Propose, Solve, Verify: Self-Play Through Formal Verification

Training models through self-play alone (without any human data) has been a longstanding goal in AI, but its effectiveness for training large language models remains unclear, particularly in code generation where rewards based on unit tests are brittle and prone to error propagation. We study self-play in the verified code generation setting, where formal verification provides reliable correctness signals. We introduce Propose, Solve, Verify (PSV) a simple self-play framework where formal verification signals are used to create a proposer capable of generating challenging synthetic problems and a solver trained via expert iteration. We use PSV to train PSV-Verus, which across three benchmarks improves pass@1 by up to 9.6x over inference-only and expert-iteration baselines. We show that performance scales with the number of generated questions and training iterations, and through ablations identify formal verification and difficulty-aware proposal as essential ingredients for successful self-play.

A long-standing dream in AI is to build systems that improve themselves without humans constantly feeding them new examples. For code-writing AI, performance of these approaches has been limited because while AI can ask itself new questions, it can't always verify whether the answers it gets are correct or incorrect, which prevents it from reliably improving on those new questions. We found that a new programming language that provides a "formal verifier" enables self improvement on code generation tasks. The key is that the formal verifier provides much stronger proof that a solution satisfies the question than most programming languages. Our method proposes questions of the right difficulty (not too easy, not too hard) to optimize learning, and leads to large performance gains over baselines. This hints at a future where AI can teach itself in any domain where correctness can be mathematically checked — no human-written solutions required.