Verifier-Grounded Agentic RL for Provably Correct Code
- Published
- Source
- arXiv
- Paper number
- 1351
- Field
- Software Engineering
- arXiv ID
- 2610.19298
Key points
- The researchers built a reward that reads the verifier's diagnostics instead of its verdict, scoring a candidate by the weighted fraction of the instance's proof obligations it discharges.
- An integrity audit outranks the verifier and rejects submissions that secretly weaken the specification or replace proofs with assumptions.
- After training Qwen3 models from 1.7B to 14B and a 35B 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.
- A binary pass-or-fail reward trained under otherwise identical settings reaches only 71.0% on code generation, and a frozen proof specialist in the loop adds 4.8 points on DafnyBench.
- When the agent must also deliver the repository patch, the fraction of held-out issues resolved 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.
Paper links
External research summaries. These are not HDATF publications or measured product results.