Propose, Solve, Verify: Self-Play Through Formal Verification
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866915688203943936 |
|---|---|
| author | Wilf, Alex Aggarwal, Pranjal Parno, Bryan Fried, Daniel Morency, Louis-Philippe Liang, Paul Pu Welleck, Sean |
| author_facet | Wilf, Alex Aggarwal, Pranjal Parno, Bryan Fried, Daniel Morency, Louis-Philippe Liang, Paul Pu Welleck, Sean |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_18160 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Propose, Solve, Verify: Self-Play Through Formal Verification Wilf, Alex Aggarwal, Pranjal Parno, Bryan Fried, Daniel Morency, Louis-Philippe Liang, Paul Pu Welleck, Sean Artificial Intelligence 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. |
| title | Propose, Solve, Verify: Self-Play Through Formal Verification |
| topic | Artificial Intelligence |
| url | https://arxiv.org/abs/2512.18160 |