Verifier-Grounded Agentic RL for Provably Correct Code
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 ...
| Authors | George Ma, Yuhao Zhang, Bing He et al. |
|---|---|
| Primary category | cs.LG |
| Published | 13 October 2026 |
| Last updated at source | 13 October 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 15 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.