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

TL;DR

This paper introduces PSV, a self-play framework using formal verification signals to improve code generation models, achieving significant performance gains over inference-only methods.

Contribution

The paper presents PSV, a novel self-play approach leveraging formal verification to generate challenging problems and train models, advancing code generation capabilities.

Findings

PSV improves pass@1 by up to 9.6x over baselines.

Performance scales with generated questions and training iterations.

Formal verification and difficulty-aware proposals are key to success.

Abstract

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.