The authors built a multi-turn reinforcement learning environment in which an agent writes code and proof annotations, runs a verifier, reads its diagnostics and revises its solution.
Verifier-based rewards train coding agents toward formally correct programs
A dense reward derived from proof diagnostics improved verified code generation while an integrity audit blocked specification tampering and unsupported assumptions.
Big Tech
George Ma · Yuhao Zhang · Bing He · Zeren Shui · Ferhat Erata · Murali Krishna Ramanathan · +2 more
UC Berkeley · AWS AI Labs
Research Digest··3 min read
Ma et al.
Why this paper
From AWS AI Labs and UC Berkeley
In one line
A reward from verifier diagnostics, plus integrity auditing, raises verified code generation from 66.1% to 93.5% on DafnyBench and from 56.3% to 100% on SWE-Proof.
What we could check
- ·No code link found
- ·No weights link found
- ·No dataset link found
- ·No compute details found
- ·No stated limitations found
- ✓Reports numbers on named benchmarks (3 benchmarks)
Observed from the paper text and links we have. Absence here means we did not find it, not that it does not exist.
§