Summary (Overview)

• Core contribution: The paper introduces VERIFIER-GROUNDED AGENTIC RL, a reinforcement learning framework for training language models to produce formally verified code, where the reward is computed from a program verifier's diagnostics (not just its verdict), augmented with an integrity audit to prevent reward hacking.
• Key innovation: The reward uses a graded obligation ratio (Ω) that measures the weighted fraction of proof obligations a candidate discharges, rather than a binary pass/fail signal, enabling dense learning signal even when most attempts fail.
• Integrity mechanism: A two-part audit (specification check and proof check) outranks the verifier, ensuring models cannot cheat by weakening specifications or inserting unchecked assumptions.
• Frozen proof specialist: A separately trained policy on annotation repair tasks is frozen and placed in the code-generation loop, where it can rewrite proof annotations to complement the main agent's implementation skills.
• Strong empirical results: Held-out verification on code generation rises from 66.1% to 93.5% on DafnyBench and from 56.3% to 100% on SWE-Proof, with gains at every scale from 1.7B to 35B parameters, and improvements transfer to unseen verification suites including a language (Rust/Verus) not in training.

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses a fundamental limitation of RL for code: test-based rewards only cover a fraction of the input domain, so a policy can pass them while remaining wrong on unobserved inputs. Meanwhile, learned reward models only approximate correctness and are susceptible to reward hacking.

Program verification offers a solution: it certifies correctness for all inputs by reducing a program and its formal specification to logical proof obligations discharged by an SMT solver. However, the verifier provides only a binary verdict (pass/fail), which creates two difficulties:

1. Density problem: When nearly every attempt fails (as with base models writing both code and proofs), the binary reward gives no learning signal — "[such rewards] are known to induce advantage and entropy collapse when successes are rare."
2. Integrity problem: A policy can cheat the verifier by changing the question — weakening postconditions, strengthening preconditions, or inserting assumptions the solver simply believes.

Theoretical Basis

The framework is built on the observation that verifiers provide explanation in addition to verdicts: "A failed attempt reports which obligations went unproved, of what kind, and where." This diagnostic information can be converted into a dense, graded reward.

The paper builds on prior work in:

• Verified code generation benchmarks (DafnyBench, SWE-Proof)
• Agentic RL environments where the model works interactively over many turns
• Group Relative Policy Optimization (GRPO) for policy optimization

Methodology

Problem Setting and Tasks

Instances consist of three parts: the specification (preconditions, postconditions, datatype invariants, lemma statements), the implementation (executable code), and proof annotations (invariants, assertions, termination measures). The specification is always given and must come back unchanged.

Two tasks are defined:

• Annotation repair: Correct implementation given, all proof annotations removed; model must write the proof.
• Code generation: Specification frozen, implementation replaced with placeholder; model writes both code and proof.

Agentic Environment

The model works against a live verifier over up to $T$ turns (20 turns in experiments), with actions including verifying, executing code, running integrity audits, submitting, and requesting proof assistance. The environment computes rewards from state the model cannot fabricate.

The Verifier-Grounded Reward

Obligation ratio: Proof obligations are sorted into five categories — postconditions, preconditions, safety, loop invariants, and termination. Before each episode, the obligation counts $N_c$ per category $c$ are fixed from the instance. The ratio is:

$$\Omega = \frac {\sum_{c : N_{c} > 0} w_{c} r_{c}}{\sum_{c : N_{c} > 0} w_{c}} \in [ 0, 1 ].$$

where $r_{c} = \max(0, N_{c} - e_{c}) / N_{c}$ and $e_c$ is the number of category-$c$ failures. Weights $w_c$ differ by task (e.g., postconditions weight 1.0 for code generation, invariants weight 1.0 for annotation repair).

Hidden probes: From the reference proof, each proof annotation is converted into a probe — inserted into the candidate at its original program point as a checked assertion. Probes already satisfied on the stripped program are dropped. These are fixed per instance, hidden from the model, and counted in $N_c$ for annotation repair. Code generation uses no probes (no reference proof available).

Final score:

$$s = \Omega - \lambda_{\text{audit}} \mathbb{1}[\text{audit failed}] - \lambda_{\text{proof}} \mathbb{1}[\text{proof check failed}] + \beta \mathbb{1}[\text{verified} \wedge \text{proof intact}]$$

with $\lambda_{\text{audit}} = 1.0$, $\lambda_{\text{proof}} = 3.0$, and $\beta = 2.0$. This induces the ordering: fully verified candidates score in $[2,3]$; honest partial attempts in $[0,1]$; verified-but-specification-altered candidates in $[-1,0]$; proof-check failures at most $-2$. Episodes that never submit receive $-1.5$.

Frozen Proof Specialist

A policy trained on annotation repair is frozen. In code generation, every submission is scored both as the agent wrote it and after the specialist rewrites its proof annotations. The episode keeps the better score:

$$s_{\text{codgen}} = \max(s_{\text{direct}}, s_{\text{assisted}})$$

This is "safe to train against": the specialist can raise the reward by completing a proof but can never lower it.

Policy Optimization

Group Relative Policy Optimization (GRPO) with $G$ complete episodes per instance ($G = 8$ at 35B, $G = 4$ below). Advantages computed from group reward statistics:

$$A_{i} = (r_{i} - \text{mean}(r)) / \text{std}(r)$$

with a clipped surrogate objective and KL penalty to the initial policy (k3 estimator).

Empirical Validation / Results

Main Results (Table 2)

• DafnyBench: Code generation verified rate rises from 66.1% (initial) to 93.5% (RL) at 35B scale, with gains at every model size (1.7B: 13.9%→27.0%; 4B: 43.4%→52.5%; 8B: 43.4%→53.3%; 14B: 41.8%→50.0%).
• SWE-Proof: Annotation repair rises from 3.1% to 68.8% and code generation from 56.3% to 100%.

Comparison with Other Training Methods (Table 3)

The binary outcome reward (controlled ablation with identical settings except reward) is competitive on annotation repair but falls far behind on code generation — 71.0% vs 93.5%.

Frozen Proof Specialist Contribution

• DafnyBench: 4.8-point improvement in code generation (93.5% vs 88.7% without)
• SWE-Proof: 12.5-point improvement (100% vs 87.5% without)
• Per-episode analysis: assistance raises verified rate from 61.9% to 72.3% on held-out episodes, changes score on 12.9% of episodes, and never lowers any score
• The specialist's advantage is negligible at 1.7B but opens from 8B onward

Transfer to Unseen Benchmarks

The 35B checkpoints improve on all three held-out suites, including:

• HumanEval-Dafny: code generation 67.9%→92.4%
• HumanEval-Nagini: 40.7%→54.4%
• HumanEval-Verus: 17.2%→36.6% (language and verifier absent from training)

Patch Generation (Table 4)

When the agent must also deliver repository patches:

• Resolve rate with specialist: 59.6% → 72.5% (+12.8)
• Without specialist: 62.4%→68.8% (trend indistinguishable from zero, $p = 0.67$)
• Full verification with specialist: 76.1%→88.1%

Theoretical and Practical Implications

1. Verifier diagnostics as dense reward: The paper demonstrates that the fine-grained diagnostic output of a program verifier — which obligations failed, of what type, and where — provides a learning signal far superior to binary pass/fail outcomes when successes are rare. This is a general principle applicable to any domain where an automated checker provides diagnostic output.

2. Integrity audits for reward robustness: The specification-check/proof-check audit that outranks the verifier's verdict provides a template for preventing reward hacking in any setting where the reward signal can be manipulated by altering the task specification.

3. Skill decomposition via frozen specialists: Training a proof specialist separately on annotation repair and freezing it into the code-generation loop shows that complex tasks requiring complementary skills can be handled by decomposing skills trained under tailored rewards, with guaranteed safety via score maximization.

4. Generalization of verifier interaction skills: The improvement on held-out benchmarks — including Verus/Rust, completely absent from training — suggests that RL against a live verifier teaches general "how to work with a verifier" skills rather than benchmark-specific idioms.

5. Practical pathway to verified code: The results on SWE-Proof patch generation (72.5% resolve rate) demonstrate a viable path toward automatically producing both code fixes and machine-checked proofs for real repository issues.

Conclusion

The paper introduces verifier-grounded agentic RL, where the reward comes from a program verifier's diagnostics rather than its verdict, combined with an integrity audit that prevents reward hacking and a frozen proof specialist that fills skill gaps in proof engineering. The approach elevates held-out code generation verification from 66.1% to 93.5% on DafnyBench and 56.3% to 100% on SWE-Proof, outperforming binary rewards, SFT, and commercial API models on code generation. The trained policies generalize to unseen verification suites — including one in an unseen language and verifier — and improve real issue resolution rates on repository patches.

Future directions suggested by the work include addressing the remaining gap in proof engineering skill (the 35B model still trails frontier models on annotation repair), extending the approach to larger model scales and additional verification languages, and further integrating verification into the full software engineering loop.