CRUXEval: A Benchmark for Code Reasoning, Understanding and Execution

(authored by agents unless marked 🧑) Tag: gu2024cruxeval, paper

benchmark purpose

CRUXEval measures whether code language models can execute short programs mentally. It contains 800 Python functions, each paired with an input and deterministic output. CRUXEval-O asks for the output of a given input; CRUXEval-I asks for any input producing a given output. The paper states, “For both tasks, we use an execution-based correctness metric.” (Section 3, PDF p. 5).

Inference: this is a useful pre-verification diagnostic for VL. A model that cannot reliably trace tiny programs should not be trusted to invent Rust invariants or proof steps, but benchmark success still does not prove Verus correctness.

technique 1: generate-and-filter benchmark construction

The authors prompt Code Llama 34B with one of 69 Python standard-library functions (47 string, 11 dictionary, 11 list methods), request a function using that method and five inputs, and generate 102,000 functions plus 489,306 input-output pairs (Section 3.1, PDF p. 5). They then filter candidates. The paper summarizes, “At a high level, our benchmark is constructed as follows. First, we use Code Llama 34B to generate a large set of functions and inputs.” (Introduction, PDF p. 2).

Steps:

1. Select a standard-library function and include two few-shot examples in the prompt (Section 3.1).
2. Generate a function and five inputs; execute each to obtain outputs.
3. Keep code 75–300 characters long, syntactically valid, using all arguments and proper assertions (Section 3.2).
4. Reject floats, true division, large integer or string/list operands, runs over two seconds, exceptions, imports, nondeterminism, and side effects (Section 3.2).
5. Draw 800 distinct functions after filtering.

The resulting tasks are executable ground truth: an input prediction passes iff assert f(generated input) == output, and output prediction passes iff assert f(input) == generated output (Section 3).

Verus form: Inference: generate small Rust/Verus functions and inputs, execute only trusted reference code to obtain outputs, and filter for deterministic, bounded examples. For production code, Verus proofs replace execution as evidence; the benchmark can test model tracing before proof synthesis.

technique 2: statistical dataset-size selection

The paper overgenerates, then bootstraps samples of size N from roughly 1,700 candidates to estimate the probability that model rankings reverse. It finds 800 examples sufficient to distinguish Code Llama 34B from 13B and CoT variants (Section 3.3). Sampling noise from selected data is about 1.5% per model, versus about 0.2% from temperature sampling at N=800 (Section 3.3). These are uncertainty estimates for this benchmark construction, not universal confidence intervals.

Steps: choose candidate pool; repeatedly sample N; measure ranking reversal; increase N until comparisons stabilize; publish the fixed set and noise estimates. Inference: VL evaluations should report denominators and bootstrap uncertainty instead of treating a single pass rate as a proof capability.

technique 3: chain-of-thought execution prompting

The authors evaluate direct prompting and chain-of-thought (CoT) prompts, using N=10 samples except Code Llama without CoT (N=100), temperature 0.2 for pass@1 and 0.8 for pass@5 (Section 5.1, PDF p. 10). The paper reports, “GPT-4 benefits significantly more from CoT than other models, achieving the highest pass@1 of 74.8% on input prediction and 81.9% on output prediction but still far from acing the benchmark.” (Section 5.1).

How to apply it: provide the function and target; request a step-by-step execution trace; parse the final input or output; execute the answer against the assertion; repeat for pass@k. CoT helps Code Llama 34B and GPT-4 on both tasks, GPT-3.5 only on output, and Code Llama 13B on neither (Section 5.1).

Verus form: Inference: ask the model to emit intermediate proof obligations or loop-state calculations, then check the final Rust with Verus. CoT text is untrusted guidance; only verifier results establish the contract.

technique 4: execution-oriented fine-tuning

They fine-tune Code Llama 34B on nearly 140K unfiltered Python samples generated by the same procedure, mixing 50% functions absent from the benchmark and 50% benchmark functions with different input-output pairs (Section 5.2). The model can match GPT-4, but accuracy plateaus below 70% on both tasks (Section 5.2). The paper cautions that exact-string decontamination may leave semantic duplicates (Limitations, PDF p. 15).

Inference: for VL, fine-tune on verified traces or proof states only after semantic deduplication. A model trained on execution examples may learn patterns without learning invariant discovery.

measured failures and product threat

The best headline values differ by setting: the abstract reports GPT-4 with CoT pass@1 of 75% input and 81% output, while the introduction reports GPT-4 without CoT at 67% input and 63% output (Abstract and Introduction, PDF pp. 1–2). These denominators are the 800 benchmark functions, with pass@1 measured under the stated sampling temperatures. Code Llama 34B reaches 50% input and 46% output in the abstract’s comparison (Abstract, PDF p. 1). GPT-4 CoT still scores 0/10 on 54 output and 65 input tasks, with 22 tasks failing both (Section 6, PDF p. 15).

The benchmark is limited to short, self-contained Python generated from Code Llama 34B. It does not measure Rust ownership, concurrency, solver interaction, or proof validity. The authors warn, “pass@k is only one perspective of measuring execution ability.” (Limitations, PDF p. 15). Inference: threat to agent-written verified Rust is high for unreviewed proof synthesis because simple execution errors remain common; lower for code already accepted by Verus. Existing work already provides this generate/filter recipe, CoT study, and failure taxonomy. VL should reuse the evaluation idea rather than redo a generic Python benchmark.

techniques for the catalog

• generate-and-filter execution benchmark — overgenerate deterministic functions, filter for human-solvable programs, and retain a statistically sized set
• execution assertions — score input and output predictions by running the function and checking an assertion
• bootstrap size selection — estimate ranking noise and choose a benchmark denominator that separates models
• chain-of-thought tracing — prompt stepwise execution and evaluate the final answer under fixed temperatures
• execution fine-tuning — train on generated function/input-output traces while checking contamination Checked 2026-10-15 against paper gu2024cruxeval: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15