mlsanityData to 14 Oct 2026

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

arXiv 2512.18160 ↗First posted 20 Dec 2025cs.AIcited by 13

On the map: Synthetic data and self-improvement for LLMs → Self-play RL for reasoning

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.

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.

Builds on

30 of 38 references.

Closest ancestors · 3

Same direction, newest first

  1. 2025Language Self-Play For Data-Free Training9 Sep
  2. 2025Absolute Zero: Reinforced Self-play Reasoning with Zero Data6 May
  3. 2024Self-playing Adversarial Language Game Enhances LLM Reasoning16 Apr

Other references · 27

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 9,379
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  3. 2021Program Synthesis with Large Language Modelscited by 3,637
  4. 2023Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generationcited by 1,391
  5. 2023SGLang: Efficient Execution of Structured Language Model Programscited by 1,141
  6. 2022STaR: Bootstrapping Reasoning With Reasoningcited by 940
  7. 2017Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithmcited by 734
  8. 2023WizardCoder: Empowering Code Large Language Models with Evol-Instructcited by 733
  9. 2023Scaling Relationship on Learning Mathematical Reasoning with Large Language Modelscited by 427
  10. 2025Monitoring Reasoning Models for Misbehavior and the Risks of Promoting Obfuscationcited by 384
  11. 2025Reinforcement Learning with Verifiable Rewards Implicitly Incentivizes Correct Reasoning in Base LLMscited by 289
  12. 2025R-Zero: Self-Evolving Reasoning LLM from Zero Datacited by 228
15 more
  1. 2017Intrinsic Motivation and Automatic Curricula via Asymmetric Self-Playcited by 141
  2. 2023No More Manual Tests? Evaluating and Improving ChatGPT for Unit Test Generationcited by 82
  3. 2022Language Models Can Teach Themselves to Program Bettercited by 78
  4. 2024Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Modelscited by 73
  5. 2024SelfCodeAlign: Self-Alignment for Code Generationcited by 62
  6. 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
  7. 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 53
  8. 2025rStar-Coder: Scaling Competitive Code Reasoning with a Large-Scale Verified Datasetcited by 51
  9. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
  10. 2024AI-Assisted Generation of Difficult Math Questionscited by 37
  11. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 35
  12. 2025Shrinking the Generation-Verification Gap with Weak Verifierscited by 24
  13. 2025Can LLMs Generate High-Quality Test Cases for Algorithm Problems? TestCase-Eval: A Systematic Evaluation of Fault Coverage and Exposurecited by 10
  14. 2024Forewarned is Forearmed: Leveraging LLMs for Data Synthesis through Failure-Inducing Explorationcited by 7
  15. 2025Self-Improving Model Steeringcited by 3

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2026: 13.

13 papers.

Sort:

By area:

  1. 2026Safe and Scalable Web Agent Learning via Recreated Websitescited by 11
  2. 2026Skill Self-Play: Pushing the Frontier of LLM Capability with Co-Evolving Skillscited by 10
  3. 2026Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalizationcited by 3
  4. 2026Vocabulary Dropout for Curriculum Diversity in LLM Co-Evolutioncited by 1
  5. 2026Anchored Self-Play for Code Repaircited by 1
  6. 2026A Task-Centric Theory for Iterative Self-Improvement with Easy-to-Hard Curriculacited by 0
  7. 2026A Survey of Reinforcement Learning for Large Language Models under Data Scarcity: Challenges and Solutionscited by 0
  8. 2026ANCORA: Learning to Question via Manifold-Anchored Self-Play for Verifiable Reasoningcited by 0
  9. 2026Information-Gain Rewards over Diversity-Pruned Tests: GT-Anchored Verifier Co-Training for Reliable Code Generationcited by 0
  10. 2026Counterfactual Self-Evolving Agents for Evidence-Grounded Reasoningcited by 0
  11. 2026Learning to Optimize through Solver-Grounded Self-Playcited by 0
  12. 2026Variance-Optimal State Resampling for Reinforcement Learning with Verifiable Rewardscited by 0
1 more
  1. 2026Explorer-Zero: Improving Self-Play for Long-Horizon Tasks with Decomposable Verifiable Rewardscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation
  2. 2026Scaling Self-Play with Self-Guidance
  3. 2026SPADE: Self-Play in Adaptive Synthetic Executable Environments
  4. 2025ReVeal: Self-Evolving Code Agents via Reliable Self-Verification
  5. 2025Towards Understanding Self-play for LLM Reasoning
  6. 2026A Theoretical Framework for Self-Play Theorem Proving Algorithms
  7. 2025Trust, But Verify: A Self-Verification Approach to Reinforcement Learning with Verifiable Rewards
  8. 2025RLSR: Reinforcement Learning from Self Reward