ExecVerify: White-Box RL with Verifiable Stepwise Rewards for Code Execution Reasoning

1. Problem Statement

Large Language Models (LLMs), particularly smaller ones (e.g., 7B parameters), struggle with code execution reasoning. While they can often generate syntactically correct code, they frequently fail to understand the concrete execution process, such as control flow, variable state changes, and intermediate execution steps.

Existing approaches to improve this capability rely on Supervised Fine-Tuning (SFT) using teacher-generated explanations. These explanations typically take two forms:

1. Input-Output (I/O) chains: Predicting outputs from inputs.
2. Natural language traces: Describing execution steps in text.

Key Limitations of Current Methods:

• Lack of Verification: SFT optimizes for token-level cross-entropy loss. The model learns to imitate the teacher's text without explicitly verifying if the intermediate execution steps (e.g., variable values, next executed line) are semantically correct. This leads to "hallucinated" reasoning where the text looks plausible but the logic is flawed.
• Data Quality: Training data is often passively collected or generated without strict control over difficulty, resulting in datasets containing trivial examples or unsolvable problems, lacking a structured curriculum.

2. Methodology: ExecVerify

The authors propose ExecVerify, a framework that combines Constraint-Based Data Synthesis with White-Box Reinforcement Learning (RL). The approach consists of three main components:

A. Constraint-Based Data Synthesis

To address data quality issues, the authors construct a curriculum-style dataset with controlled difficulty:

• Structural Constraints: They iterate through Python built-in types and methods, prompting an LLM to generate code that strictly adheres to specific structural constraints (e.g., nested method calls, specific control-flow patterns like if/for/while).
• Difficulty Control: Constraints are applied in stages (simple $\to$ complex) to ensure a mix of difficulty levels.
• Input Synthesis & Filtering:
  • Input Generation: Diverse inputs are generated for each code snippet, including type-aware mutations.
  • Execution Filtering: Programs are executed; those causing runtime errors or timeouts are discarded.
  • Difficulty Filtering: Instances are evaluated against a baseline model (Qwen2.5-Coder-7B). Only "challenging but solvable" instances (where the baseline succeeds $\le$ 3 times out of 10) are retained. This ensures the training data is non-trivial.

B. White-Box Reinforcement Learning (Stage I)

Instead of relying on text imitation, ExecVerify uses verifiable white-box rewards derived directly from interpreter execution traces.

• Trace Collection: For a given program and input, an interpreter generates a trace $\tau$ containing executed statements ($l_t$) and program states ($\sigma_t$, including variable values and types).
• White-Box Questions: The trace is converted into verifiable questions:
  1. Control-Flow Questions: "Which line is executed next?"
  2. Data-Flow Questions: "What is the value and type of variable $X$ after line $Y$?"
• Reward Function: The reward $R_{white-box}$ is a weighted combination of:
  • I/O Correctness: Binary reward for the final output.
  • Step-Level Accuracy: A reward based on the model's ability to correctly answer the white-box questions about intermediate states.
  • Formula: $R = 2 \cdot ((1-\alpha)R_{I/O} + \alpha R_{white})$.
• Two-Directional Reasoning: The framework also includes reverse prediction tasks (Output $\to$ Input) to prevent over-reliance on forward pattern matching.

C. Two-Stage Post-Training Pipeline

1. Stage I (Reasoning): The model undergoes SFT warm-up followed by White-Box RL. This aligns the model's internal reasoning with semantic correctness at every execution step.
2. Stage II (Generation): The reasoning-enhanced model is further fine-tuned using Unit-Test RL (standard code generation reward based on passing test cases). This transfers the granular execution understanding into functional code generation.

3. Key Contributions

1. White-Box RL Framework: Introduces a novel training paradigm that replaces text-level imitation with verifiable, step-level rewards derived from interpreter traces. This forces the model to learn the actual mechanics of code execution.
2. Curriculum-Based Data Synthesis: Proposes a method to actively synthesize executable code with controlled structural complexity and difficulty, filtering out trivial or unsolvable examples to create a high-quality training corpus.
3. Two-Stage Transfer Strategy: Demonstrates that enhancing execution reasoning first (Stage I) significantly boosts downstream code generation performance (Stage II), bridging the gap between reasoning and generation.
4. Open Source: The authors released the code, data, and models.

4. Experimental Results

The authors evaluated the approach using Qwen2.5-Coder-7B-Instruct as the base model.

• Code Execution Reasoning:

  • The 7B model trained with ExecVerify achieved an average score of 80.8 on benchmarks (CRUXEval, LiveCodeBench-Exec, REval).
  • This performance is competitive with much larger models (e.g., Qwen2.5-Coder-32B-Instruct, which scored 77.9) and significantly outperforms other 7B baselines (e.g., +20.0 points over the base model).
  • Ablation studies confirmed that both the SFT warm-up and the White-Box RL components are essential.

• Code Generation:

  • After the two-stage training, the model achieved a 5.9% improvement in pass@1 on code generation benchmarks (EvalPlus, LiveCodeBench, BigCodeBench) compared to strong post-training baselines.
  • The results show a consistent upward trend: Base $\to$ I/O RL $\to$ SFT + I/O RL $\to$ SFT + White-Box RL + Unit-Test RL.

• Generalization:

  • Cross-Language: The reasoning improvements transferred effectively to other languages (Java, C++, etc.) in the CRUXEval-X benchmark.
  • Library-Involved Code: The model showed improved performance on tasks involving external libraries.
  • Model Sizes: The pipeline yielded consistent gains on both 3B and 8B models, indicating architecture independence.

5. Significance

• Beyond Text Imitation: ExecVerify proves that LLMs can be trained to "think" like an interpreter rather than just mimicking text descriptions of code. By verifying intermediate steps, the model learns to track control flow and variable states accurately.
• Efficiency: A small 7B model trained with this method outperforms larger 32B models on reasoning tasks, suggesting that data quality and training objectives are more critical than sheer parameter count for execution reasoning.
• Robustness: The method reduces logical errors in code generation (e.g., confusing "at least one" with "for all" conditions) by grounding the model in fine-grained runtime behavior.
• Future Direction: This work sets a precedent for using verifiable rewards in RL for code, moving away from purely human-labeled or LLM-generated text supervision toward execution-grounded learning.