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

arXiv: https://arxiv.org/abs/2512.18160 · HTML: https://mlsanity.com/paper/2512.18160/

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Placed in Self-play RL for reasoning, one of 13 directions in Synthetic data and self-improvement for LLMs.
- Builds on 30 of its 38 references that are in the map.
- First posted on arXiv 20 Dec 2025.

## Placed in

- Synthetic data and self-improvement for LLMs / [Self-play RL for reasoning](https://mlsanity.com/synth/self-play-rl-for-reasoning/)

## Builds on (most cited first, 30 of 30)

- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generation](https://mlsanity.com/paper/2305.01210/) (2023)
- [SGLang: Efficient Execution of Structured Language Model Programs](https://mlsanity.com/paper/2312.07104/) (2023)
- [STaR: Bootstrapping Reasoning With Reasoning](https://mlsanity.com/paper/2203.14465/) (2022)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [WizardCoder: Empowering Code Large Language Models with Evol-Instruct](https://mlsanity.com/paper/2306.08568/) (2023)
- [Scaling Relationship on Learning Mathematical Reasoning with Large Language Models](https://mlsanity.com/paper/2308.01825/) (2023)
- [Monitoring Reasoning Models for Misbehavior and the Risks of Promoting Obfuscation](https://mlsanity.com/paper/2503.11926/) (2025)
- [Absolute Zero: Reinforced Self-play Reasoning with Zero Data](https://mlsanity.com/paper/2505.03335/) (2025)
- [Reinforcement Learning with Verifiable Rewards Implicitly Incentivizes Correct Reasoning in Base LLMs](https://mlsanity.com/paper/2506.14245/) (2025)
- [R-Zero: Self-Evolving Reasoning LLM from Zero Data](https://mlsanity.com/paper/2508.05004/) (2025)
- [Intrinsic Motivation and Automatic Curricula via Asymmetric Self-Play](https://mlsanity.com/paper/1703.05407/) (2017)
- [Self-playing Adversarial Language Game Enhances LLM Reasoning](https://mlsanity.com/paper/2404.10642/) (2024)
- [No More Manual Tests? Evaluating and Improving ChatGPT for Unit Test Generation](https://mlsanity.com/paper/2305.04207/) (2023)
- [Language Models Can Teach Themselves to Program Better](https://mlsanity.com/paper/2207.14502/) (2022)
- [Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models](https://mlsanity.com/paper/2406.13542/) (2024)
- [SelfCodeAlign: Self-Alignment for Code Generation](https://mlsanity.com/paper/2410.24198/) (2024)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [rStar-Coder: Scaling Competitive Code Reasoning with a Large-Scale Verified Dataset](https://mlsanity.com/paper/2505.21297/) (2025)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Language Self-Play For Data-Free Training](https://mlsanity.com/paper/2509.07414/) (2025)
- [AI-Assisted Generation of Difficult Math Questions](https://mlsanity.com/paper/2407.21009/) (2024)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [Shrinking the Generation-Verification Gap with Weak Verifiers](https://mlsanity.com/paper/2506.18203/) (2025)
- [Can LLMs Generate High-Quality Test Cases for Algorithm Problems? TestCase-Eval: A Systematic Evaluation of Fault Coverage and Exposure](https://mlsanity.com/paper/2506.12278/) (2025)
- [Forewarned is Forearmed: Leveraging LLMs for Data Synthesis through Failure-Inducing Exploration](https://mlsanity.com/paper/2410.16736/) (2024)
- [Self-Improving Model Steering](https://mlsanity.com/paper/2507.08967/) (2025)

## Built on by (most cited first, 13 of 13)

- [Safe and Scalable Web Agent Learning via Recreated Websites](https://mlsanity.com/paper/2603.10505/) (2026)
- [Skill Self-Play: Pushing the Frontier of LLM Capability with Co-Evolving Skills](https://mlsanity.com/paper/2607.22529/) (2026)
- [Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization](https://mlsanity.com/paper/2605.26457/) (2026)
- [Vocabulary Dropout for Curriculum Diversity in LLM Co-Evolution](https://mlsanity.com/paper/2604.03472/) (2026)
- [Anchored Self-Play for Code Repair](https://mlsanity.com/paper/2607.03523/) (2026)
- [A Task-Centric Theory for Iterative Self-Improvement with Easy-to-Hard Curricula](https://mlsanity.com/paper/2602.10014/) (2026)
- [A Survey of Reinforcement Learning for Large Language Models under Data Scarcity: Challenges and Solutions](https://mlsanity.com/paper/2604.17312/) (2026)
- [ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoning](https://mlsanity.com/paper/2604.27644/) (2026)
- [Information-Gain Rewards over Diversity-Pruned Tests: GT-Anchored Verifier Co-Training for Reliable Code Generation](https://mlsanity.com/paper/2609.21208/) (2026)
- [Counterfactual Self-Evolving Agents for Evidence-Grounded Reasoning](https://mlsanity.com/paper/2609.32870/) (2026)
- [Learning to Optimize through Solver-Grounded Self-Play](https://mlsanity.com/paper/2609.34205/) (2026)
- [Variance-Optimal State Resampling for Reinforcement Learning with Verifiable Rewards](https://mlsanity.com/paper/2610.15888/) (2026)
- [Explorer-Zero: Improving Self-Play for Long-Horizon Tasks with Decomposable Verifiable Rewards](https://mlsanity.com/paper/2610.19868/) (2026)

## Abstract (arXiv)

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.