Reinforcement learning for code usually rewards passing tests, which a model can do while remaining wrong on the inputs the tests do not cover. A program verifier instead decides whether a program satisfies a formal specification for all inputs. Language models are almost always paired with verifiers at inference time only, and turning a verifier into a reward raises two difficulties. It reports only acceptance or rejection, which gives no gradient when every attempt fails, and a policy can cheat it, most simply by telling it to assume what the proof was supposed to establish. We build an agentic environment and reward that address both. The reward reads the verifier's diagnostics rather than its verdict, scoring a candidate by the weighted fraction of proof obligations it discharges, extended with hidden probes from a reference proof's annotations. An integrity audit outranks the verifier, rejecting any candidate that alters the specification or assumes what it was meant to prove. The model works as an agent against a live verifier over many turns, with a separately trained proof specialist as a frozen collaborator. Across Qwen3 models from 1.7B to 14B and a 35B Qwen3.6 mixture-of-experts model, held-out verification on code generation rises from 66.1% to 93.5% on DafnyBench and from 56.3% to 100% on SWE-Proof. This reward leads every other training signal we compare, including a binary pass-or-fail reward trained under otherwise identical settings, with the widest margin on code generation. When the agent must also deliver the repository patch, graded by each project's withheld tests, the fraction of held-out issues it resolves rises from 59.6% to 72.5%. Evaluated unchanged on three verification suites withheld from training, the checkpoints improve on all of them, including one whose language and verifier are absent from training.
Figures & tables
Figure 1: The method. (a) In an episode, the policy takes one action per turn against a live verifier and revises based on its diagnostics. (b) Scoring a submission: the failed obligations and the hidden probes give the obligation ratio Ω (Equation 1 ), while the integrity audit checks that the specification is intact and that no obligation was assumed instead of proved. (c) The ordering the score (Equation 2 ) induces: a verified candidate with an intact specification ranks highest, one that verifies only by weakening the specification ranks below an honest partial proof, and one that fails the proof check ranks below not submitting at all.
Figure 2: An instance and the two tasks built from it. Each task removes a different part of a verified program and asks the model to restore it, leaving the specification given and unchanged.
DafnyBench
SWE-Proof
Specification lines
16
117
Preconditions
1
4
Postconditions
2
8
Table 1: Median size of a specification in each benchmark.
Figure 3: The frozen proof specialist. (a) A policy is trained on annotation repair and then frozen. (b) In code generation, every submission is scored as the agent wrote it and again after the specialist rewrites its proof annotations, keeping the implementation. The episode takes the better score, and the specialist’s version is returned to the agent as feedback.
Figure 4: Held-out verified rate over training, per model size and task. Faint traces are per-step values and bold traces exponentially weighted moving averages; open and filled markers show the initial policy and the best checkpoint, with values above each panel. More curves are in Appendix F .
Annotation repair
Code generation
Benchmark
Model
Init
RL
Δ
Init
RL
Δ
DafnyBench
Qwen3-1.7B
10.5
22.6
(+12.1)
13.9
27.0
(+13.1)
Qwen3-4B
26.6
51.6
(+25.0)
43.4
52.5
( 0 +9.1)
Qwen3-8B
38.7
53.2
(+14.5)
43.4
53.3
( 0 +9.9)
Qwen3-14B
36.3
51.6
(+15.3)
41.8
50.0
( 0 +8.2)
Qwen3.6-35B-A3B
67.4
76.7
( 0 +9.3)
66.1
93.5
(+27.4)
Table 2: Held-out verified rate (%) before and after verifier-grounded RL. Init is the initial policy and RL the best held-out checkpoint. The lower block evaluates the 35 B checkpoints trained on DafnyBench (Dafny, Verus) and SWE-Proof (Nagini) on benchmarks never used in training.
Figure 5: Code generation with and without the frozen proof specialist. Left and center: held-out verified rate at 35 B-A 3 B, with per-step values (faint) and moving averages (solid). Right: difference in best held-out rate at each DafnyBench scale.
Method
Annotation repair
Code generation
Untrained policy
67.4
66.1
Supervised fine-tuning
60.9
53.2
Binary outcome reward
75.2
71.0
Verifier-grounded reward
76.7
93.5
Table 3: Held-out verified rate (%) at 35 B on DafnyBench under different training signals. The binary outcome reward matches our run in every setting except the reward.
Figure 9
Appendix figures & tables18 assets
Supplementary material from the paper’s appendix.
Appendix
Task
Postcondition
Precondition
Safety
Invariant
Termination
Code generation
1.00
0.50
0.50
0.25
0.25
Annotation repair
0.50
0.25
0.25
1.00
0.25
Appendix
Table 5: Obligation category weights wc used in Equation 1 .
Qwen3-1.7B
Qwen3-4B
Qwen3-8B
Qwen3-14B
Qwen3.6-35B-A3B
Instances per step
8
8
8
8
16–32
Episodes per instance G
4
4
4
4
8
Learning rate
1×10−6
1×10−6
1×10−6
1×10−6
2×10−6
KL coefficient
0.02
0.02
0.02
0.02
0.02
Update epochs per step
1
1
1
1
1–2
Max response tokens
4096
4096
4096
4096
8192–12288
Appendix
Table 6: Training hyperparameters. G is episodes sampled per instance. All runs are full-parameter; no adapters are used.
Code generation
Annotation repair
Repository
Total
Train
Held-out
Total
Train
Held-out
Web framework (split)
231
184
0 47
111
88
23
Symbolic mathematics
0 75
0 75
00 0
0 43
43
0 0
Documentation generator
0 44
0 44
00 0
0 27
27
0 0
Plotting library
0 34
0 34
00 0
0 14
14
0 0
Machine learning toolkit
0 32
0 32
00 0
0 14
14
0 0
Appendix
Table 7: Per-repository composition of the SWE-Proof split. The largest repository is divided across both sides; every other repository lies entirely on one side.
Figure 7: DafnyBench over training, one column per model size. Rows one and two are annotation repair, held-out verified rate and mean training reward; rows three and four are code generation. Faint traces are per-step values, solid traces exponentially weighted moving averages.
Figure 8: SWE-Proof at 35 B: held-out verified rate (left column) and mean training reward (right column), annotation repair on top and code generation below. Annotation repair starts near zero, so essentially all of its final performance is acquired during training.
Figure 9: SWE-Proof held-out verified rate at every model size. Top row: annotation repair, which stays at or near zero below 35 B; note the compressed vertical scale on the first four panels. Bottom row: code generation with and without the frozen proof specialist, which are indistinguishable wherever the specialist itself is at the floor.
Figure 10: DafnyBench episode diagnostics over training at all five model sizes: turns per episode, submissions per episode, mean response length, the fraction of submissions failing the integrity audit, and policy entropy.
Figure 11: The same diagnostics on SWE-Proof at 35 B. Episodes are longer than on DafnyBench throughout, which is what a repository-scale instance with several routines to prove requires.
Run
Window
Submits/ep.
First-try
Retries
Revises
Recovers
DafnyBench codegen
early
2.28
52.8
87.6
96.8
38.2
late
1.98
66.9
99.4
98.9
53.7
DafnyBench repair
early
2.40
46.8
91.4
95.3
42.9
late
2.72
42.9
97.9
98.6
47.2
SWE-Proof codegen
early
1.84
58.7
83.0
85.2
27.6
late
1.24
82.5
100.0
89.7
89.3
Appendix
Table 8: Held-out episode behavior, early versus late in training. All columns but the first are percentages. First-try is the fraction of episodes whose first submission verifies. The last three condition on the first submission failing: whether the policy submits again, whether the resubmission changes the program, and whether the episode ends verified anyway.
Episodes
n
Direct (%)
Assisted (%)
Verify only with help
Verify only without
Held-out
1589
61.9
72.3
165
0
Training
16250
59.8
71.3
1874
0
Appendix
Table 9: Per-episode effect of the frozen proof specialist on DafnyBench code generation. Direct is the agent’s own candidate; Assisted is the score the reward used. The last two columns count episodes where assistance changed the verification outcome in each direction.
Qwen3-1.7B
Qwen3-4B
Qwen3-8B
Qwen3-14B
Qwen3.6-35B-A3B
With specialist
27.0
52.5
53.3
50.0
93.5
Without specialist
27.9
51.6
48.4
48.4
88.7
Appendix
Table 10: Held-out verified rate (%) on DafnyBench code generation with and without the frozen proof specialist, at every model size.
Figure 12: DafnyBench code generation episode diagnostics with and without the frozen proof specialist. The two runs behave alike.
Figure 13: The same diagnostics on SWE-Proof code generation.
With frozen specialist
Without specialist
Step
Resolve
Verify
Step
Resolve
Verify
0
59.6
76.1
0
62.4
84.4
5
65.1
78.9
5
60.6
88.1
10
66.1
83.5
10
68.8
85.3
15
65.1
80.7
15
67.9
89.0
20
67.9
88.1
20
68.8
87.2
Appendix
Table 11: Every held-out pass of the two SWE-Proof patch generation runs, on the complete held-out split ( 109 instances, one greedy sample each). Resolve is the fraction of issues whose patch passes the project’s withheld tests and verify the fraction of the same episodes whose Nagini program verifies with an intact specification.
Held out
Training
Measure
Run
Slope
p
Slope
p
Resolve
With specialist
+0.29
7.6×10−4
+0.44
2.9×10−4
Without specialist
+0.05
6.7×10−1
−0.15
3.2×10−1
Full verification
With specialist
+0.30
5.5×10−3
+0.59
1.1×10−5
Without specialist
+0.09
1.5×10−1
+0.25
1.9×10−1
Appendix
Table 12: Fitted trends over the eight held-out passes and over the training steps of the same runs. Slope is in points of rate per training step, with the p -value of a two-sided test against zero slope.
Suite
Task
n
Init (%)
RL (%)
z
p
HumanEval-Dafny
repair
110
54.5
70.0
2.36
1.8×10−2
HumanEval-Dafny
codegen
131
67.9
92.4
4.96
7.1×10−7
HumanEval-Nagini
repair
0 77
23.1
36.4
1.81
7.0×10−2
HumanEval-Nagini
codegen
0 90
40.7
54.4
1.86
6.3×10−2
HumanEval-Verus
repair
0 84
0 9.5
13.1
0.73
4.6×10−1
HumanEval-Verus
codegen
0 93
17.2
36.6
2.98
2.9×10−3
Appendix
Table 13: Transfer significance, two-proportion z -tests on the instances where both the initial policy and the trained checkpoint were evaluated.
No submission (%)
Unparseable turns (%)
Suite
Task
Init
RL
Init
RL
HumanEval-Dafny
repair
0 8.2
0.0
31.4
15.5
HumanEval-Dafny
codegen
0 8.4
0.0
18.6
13.2
HumanEval-Nagini
repair
0 5.1
0.0
34.6
25.3
HumanEval-Nagini
codegen
11.0
0.0
27.6
0 7.8
HumanEval-Verus
repair
13.1
0.0
56.3
32.8
Appendix
Table 14: Interaction quality on the transfer suites. No submission is the fraction of episodes that never produce a candidate; unparseable turns is the share of turns whose output contains no action the environment can execute.
Multi-submit (%)
Submissions
Suite
Task
Init
RL
Init
RL
HumanEval-Dafny
repair
46.3
63.6
1.96
3.52
HumanEval-Dafny
codegen
41.8
32.8
2.73
1.64
HumanEval-Nagini
repair
93.8
60.7
6.00
3.11
HumanEval-Nagini
codegen
48.5
30.6
4.09
3.18
HumanEval-Verus
repair
83.3
63.6
2.33
3.64
Appendix
Table 15: Iteration among successful transfer episodes. Multi-submit is the fraction of successes that required more than one submission; submissions is the mean number among successes.
Reinforcement learning for code generation trains models to write, repair, and optimize programs using execution-based and other task-specific feedback.
A classical intuition holds that verifying a solution is easier than producing one. For today's coding agents, this intuition is being inverted: as foundation models develop stronger reasoning capabilities and engineering harnesses grow more sophisticated, generating complex candidate solutions is no longer difficult -- reliably verifying them has become the harder problem. Every verifier we can build is only a proxy for human intent, never the intent itself. This makes verification subject to a twofold difficulty: first, intent is underspecified by nature, making it inherently hard to faithfully check whether it has been fulfilled; second, during model training, optimization widens the gap between proxy and intent -- manifesting as reward hacking or signal saturation. To address this, we characterize the quality of verification signals along three dimensions -- scalability, faithfulness, and robustness -- and argue that achieving all three simultaneously is the central challenge. We further study four reward constructions: a test verifier for general coding tasks, a rubric verifier for frontend tasks, the user as verifier for real-world agent tasks, and an automated agent verifier for long-horizon tasks. Across different task types and policy capability levels, we conduct in-depth analysis and experiments on the core challenges of reward design and how to more effectively leverage reward signals. Experiments show that targeted verification design can effectively suppress reward hacking, improve task completion quality, and achieve significant gains across multiple internal and public benchmarks. These experiences collectively point to a core observation: no fixed reward function can remain effective as policy capability continues to grow; and verification must co-evolve with the generator.
Test-time scaling for large language models (LLMs) can involve generating multiple candidate solutions for selection or revising an earlier attempt. To guide selection and revision, we need a verifier that can estimate candidate correctness and provide evidence of failure. In competitive programming, however, official judging systems provide authoritative verdicts under finite submission budgets, without revealing failure explanations or failing inputs. To provide informative feedback without consuming official submissions, we formulate a task in which a model judges and diagnoses a candidate program using only the problem statement and source code, with generated counterexamples serving as checkable evidence. To evaluate this task, we build USACO-JUDGE from the USACO 2026 contests, using accepted and unaccepted programs written by human experts and multiple LLMs. We then train ARBITER, a 35B mixture-of-experts (MoE) agentic verifier, with reinforcement learning in a generic execution sandbox. Training raises counterexample success on incorrect programs from 40.61% to 62.67% and mean binary verdict accuracy on USACO-JUDGE from 71.41% to 87.41%, approaching frontier verification performance. Beyond verification, ARBITER outperforms baselines in both code selection and refinement. In an IOI 2026 case study, ARBITER-guided refinement raises GPT-OSS-120B's expected score above the gold-medal threshold under the official submission limit.
Automated formal verification remains challenging for large language models because data for proof assistants and verification-aware languages is scarce, and correctness depends on satisfying precise machine-checkable specifications rather than producing plausible code. This thesis studies how verifier environments can improve LLM generation of verified programs and proofs through reinforcement learning from verifiable rewards (RLVR) and verifier-guided inference-time search. First, we train open-source models in Dafny with RLVR using Group Relative Policy Optimization (GRPO) and related variants, assembling generated candidates into complete programs and scoring them with compiler and verifier outcomes. Initial experiments on an APPS-derived Dafny dataset increased verified reward from 2.2% to 58.1%, but revealed specification hacking, where models exploit weak formal specifications instead of implementing the intended solutions. After filtering underspecified and vulnerable tasks, multi-turn RLVR on the refined benchmark improves the verified pass rate from 9.7% to 31.1%. Second, we develop a verifier-guided inference scaffold in Lean that treats proof generation as structured search over decomposed subgoals, verifier feedback, diagnostics, and repair. With a fixed base model, the full scaffold with proof reviser improves pass rate on an initial VeriCoding pilot set from 46.2% under direct repair to 69.2%. On the larger VERINA dataset, whole-task decomposition plus proof reviser solves 7 of 42 previously unsolved tasks. We also introduce Dalek-Bench, a repository-scale Lean benchmark derived from the Rust curve25519-dalek verification project; preliminary results remain weak, indicating that stronger progress evaluation and task-specific tool-use policies are still needed.
Max Tan
Department of Electrical Engineering and Computer Science · Massachusetts Institute of Technology