Propose, Solve, Verify: Self-Play Through Formal Verification — part 1/3
Cleaned-text code points [0, 15202). Bibliography omitted here; source.md includes it.
# Propose, Solve, Verify: Self-Play Through Formal Verification
###### 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.6× 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.
###### Keywords:
## 1 Introduction
A longstanding goal of AI research is to enable self-play , in which a system learns by creating its own curriculum without human supervision ( Silver et al., 2017 ; Sukhbaatar et al., 2018 ) . In the context of large language models (LLMs), an emerging family of proposer-solver algorithms holds the promise of improving LLMs through self-play ( Haluptzok et al., 2023 ; Zhao et al., 2025 ) . In this setup, a proposer model generates problems for a solver model to train on, and the solver’s capabilities inform the proposer’s curriculum. If one can reliably judge whether the solver’s outputs are correct, one can train the solver with reinforcement learning and successfully design curricula that adapt to the solver’s capabilities.
Thus a fundamental challenge in realizing proposer-solver self-play is verification . An imperfect verifier can be exploited by the solver, and hence corrupt the solver’s training and any curricula that depend on the solver’s performance. Indeed, successful early attempts have come in easy-to-verify domains such as formal theorem proving ( Dong and Ma, 2025 ) or easy-to-check synthetic tasks ( Haluptzok et al., 2023 ; Dong et al., 2025 ; Zhao et al., 2025 ) , leaving self-play’s scope of impact for LLMs unclear.
We study self-play for code generation, a domain where verification typically relies on unit tests ( Liu et al., 2023 ) . A fundamental limitation is that unit tests only cover a limited set of cases, so programs can pass them and still be incorrect ( Xin and Reiss, 2017 ; Liu et al., 2023 ; Yuan et al., 2024 ) . This can lead the solver to optimize for passing tests rather than solving the underlying task, and errors can propagate across iterations ( Lin et al., 2025 ; Baker et al., 2025 ) . Hence self-play in code generation remains an open problem.
We introduce Propose, Solve, Verify ( PSV ) , which uses formal verification to unlock a new paradigm for self-play in code generation. The core idea is for a proposer to generate problems in the form of formal specifications —statements that mathematically describe all possible permitted inputs plus the desired output behavior of a program with respect to those inputs—-and for a solver to try to generate programs that meet the specifications. The key benefit is that formal verification provides a sound reward signal: if the verifier accepts the program, then the program is guaranteed to satisfy its specification for all inputs. Thus unlike unit tests, formal verification prevents incorrect solutions from entering the self-play loop.
We apply PSV to Verus ( Lattuada et al., 2023 ) , a framework that enables formal verification of Rust programs and has attracted recent interest for LLM code generation (e.g., Yang et al. (2025a) ; Aggarwal et al. (2024) ). We design a difficulty-aware proposer that adapts the difficulty of proposed specifications based on the solver’s current pass rates. We initialize self-play from the same translated corpus used by AlphaVerus ( Aggarwal et al., 2024 ) , which originates from human-written problems. PSV then expands this corpus by alternating between proposing new specifications, training the solver on verified solutions, and using the solver’s performance to guide the next round of problem proposal. As shown in Figure 1 , the PSV self-play loop yields substantial gains: our model, PSV-Verus , improves across iterations and substantially outperforms both training on the seed corpus alone (RFT) and AlphaVerus, which relies on the same seed corpus but without self-play.
We show that PSV-Verus ’s performance scales with the number of iterations and generated questions, and empirically identify that verification of solutions and the difficulty-awareness and diversity of the proposal are key factors for self-play. Coupled with recent successes in formal theorem proving ( Dong and Ma, 2025 ) , our work points to formal verification as a promising frontier for LLM self-play. In summary, our contributions are as follows: 1. We introduce Propose, Solve, Verify ( PSV ), a self-play algorithm for code generation that leverages formal verification, and propose a difficulty-aware proposer based on in-context learning.
2. We train PSV-Verus , which outperforms the previous state-of-the art AlphaVerus ( Aggarwal et al., 2024 ) and Expert Iteration ( Singh et al., 2024 ) on verified Rust programming.
3. We show that performance scales with question budget and iterations, and identify proposal coverage and difficulty as factors driving self-play.
4. We release our code and models. 1 1 1 https://github.com/abwilf/psv
## 2 Related Work
#### Verified code generation.
Verified code generation asks solver models to generate both programs and machine-checkable proofs that verifiers can deterministically and mechanically check against a specification. For example in Figure 2 , the implementation and proof must satisfy the postconditions described in the ensures block of the spec over all possible inputs and outputs to the function . Unlike unit-tests, which are hard for LLMs to generate and vulnerable to reward hacking ( Yang et al., 2025a ; Baker et al., 2025 ) , formal verification provides a binary guarantee of correctness. This makes the setting attractive for safety-critical domains ( Klein et al., 2014 ) and for self-improving AI that requires verification of novel questions. Recently developed formal verification languages such as Verus ( Lattuada et al., 2023 ) bring SMT-backed proofs into mainstream systems languages such as Rust, making formal verification possible in real world, modern programming domains. A key obstacle to model performance on these tasks is data scarcity ( Aggarwal et al., 2024 ) , which makes synthetic corpus generation under formal verifier feedback especially promising.
#### Self-improving AI systems.
Self-play game playing algorithms such as AlphaZero have shown that AI systems can surpass human performance without human labels ( Silver et al., 2017 ) . Yet porting this paradigm to language, in particular reasoning, has been challenging: the action space is vast and verifiers are often weak instead of deterministic (e.g., the rules of the game define a win/loss). Recent work has made progress on self-improving language models with rejection-finetuning ( Singh et al., 2024 ; Zelikman et al., 2022 ) and reinforcement learning from verifiable rewards (RLVR) ( Shao et al., 2024 ; DeepSeek-AI et al., 2025 ; Wen et al., 2025 ) on fixed human-generated datasets. Yet human-generated reasoning datasets are limited and difficult to scale ( Liu et al., 2025 ) , motivating the creation of synthetic data for training reasoning capabilities.
#### Self-play reasoning systems
Self-play systems leverage an intuition that there is a “gap” between what AI can solve and verify ( Song et al., 2024 ) , meaning that systems could self-improve by proposing novel problems and verifiers and training a “solver” model on verified solutions. This has been applied to reasoning games ( Cheng et al., 2025b ) , code ( Rozière et al., 2023 ; Wei et al., 2024 ; Haluptzok et al., 2023 ) , and math ( Shah et al., 2024 ) . A recent line of work has also proposed recursively self-improving, by training the question proposer as well to output difficult problems for the current solver ( Li et al., 2024 ; Huang et al., 2025 ) . This has been applied to formal math ( Dong and Ma, 2025 ) , coding ( Zhao et al., 2025 ; Lin et al., 2025 ) , tool use ( Zhou et al., 2025 ) , alignment ( Cheng et al., 2025a ; Zhu et al., 2025 ) , and general language tasks ( Kuba et al., 2025 ) . As strong verifiers are important to self-play (yet often limited in applicability) ( Saad-Falcon et al., 2025 ) , we investigate the verified coding domain in Verus ( Lattuada et al., 2023 ) where SMT-backed verification provides a sound guarantee over a Turing-complete language (Rust).
## 3 Propose, Solve, Verify ( PSV )
Propose, Solve, Verify (PSV) leverages a formal verifier to enable a self-play loop. The core idea is to iterate between proposing specifications, attempting to solve the specifications, and using the formal verifier’s feedback to improve the solver and inform the next round of problem proposal. Over time the solver trains with an evolving pool of challenging and diverse problems, yielding improvements in the solver’s capabilities. We describe each component in detail below.
#### Problem setting.
We consider the problem of verified code generation. In this problem, the input is a formal specification x ∈ 𝒳 x\in\mathcal{X} , and the output is code y ∈ 𝒴 y\in\mathcal{Y} . A verifier v ( x , y ) → { 0 , 1 } v(x,y)\rightarrow\{0,1\} checks whether the code meets the formal specification. If so, the verifier returns 1 and otherwise it returns 0. The specification and code are written in a language that supports verification, such as Verus ( Lattuada et al., 2023 ) which supports verification for a subset of Rust code, or Dafny ( Leino, 2010 ) . The code y y contains an implementation and any additional proof code (e.g., “loop invariants”) that is necessary for the program to pass the verifier. Given a specification x x , the goal is to produce code y y that passes the verifier, v ( x , y ) = 1 v(x,y)=1 . The key property that we leverage is that the Verus verifier is sound with respect to specifications, i.e., if v ( x , y ) = 1 v(x,y)=1 then the program y y meets the specification x x . See Appendix F for additional background.
While we consider formally verified code generation here, in principle our methods apply to any problem with a sound verifier, i.e., if the verifier v ( x , y ) v(x,y) returns 1, then y y is a correct output for problem x x . Applying PSV to other such problems is left for future work.
### 3.1 Propose, Solve, Verify ( PSV )
PSV is an algorithm that runs for iterations t ∈ { 1 … T } t\in\{1\ldots T\} and consists of a proposer model P ϕ t P_{\phi_{t}} and a solver model S θ t S_{\theta_{t}} , working together to generate and solve new problems, supervised with help from the verifier.
At the first iteration ( t = 0 t=0 ), PSV receives a set of seed problem specifications X t = { x 1 , x 2 , … , x N 0 } X_{t}=\{x_{1},x_{2},\ldots,x_{N_{0}}\} , and the solver attempts to solve them. That is, given a specification x i x_{i} the solver produces candidate outputs y i , t 1 , … , y i , t k t r n y_{i,t}^{1},\ldots,y_{i,t}^{k_{trn}} , where k t r n k_{trn} is a hyperparameter governing the number of solver attempts per specification. Each output has an associated verification outcome v i , t j ∈ { 0 , 1 } v_{i,t}^{j}\in\{0,1\} obtained by running the verifier on x i , y i , t j x_{i},y_{i,t}^{j} . Over all specifications x ∈ X t x\in X_{t} , this yields a data pool D t = ( X t , Y t , V t ) D_{t}=(X_{t},Y_{t},V_{t}) .
The solver is then trained using the data pool, yielding a new solver S θ t + 1 S_{\theta_{t+1}} . Finally, the proposer P ϕ t P_{\phi_{t}} is updated using the data pool and is used to generate a new set of B B specifications that are added to the existing set, so that X t + 1 = X t ∪ { x N t + 1 , x N t + 2 , … , x N t + B } X_{t+1}=X_{t}\cup\{x_{N_{t}+1},x_{N_{t}+2},\ldots,x_{N_{t}+B}\} . The process iterates for a fixed number of iterations T T .
Next, we describe the specific design choices for the solver, learning algorithm, and proposer that we use in our experiments, including our difficulty-aware proposer. We summarize PSV in Algorithm 1 .
#### Solving.
At each iteration t t , PSV produces candidate solutions for each x i ∈ X t x_{i}\in X_{t} by sampling from the solver model S θ t S_{\theta_{t}} with temperature 0.8, yielding k t r n k_{trn} candidate solutions for each: y i , t 1 , … , y i , t k t r n y_{i,t}^{1},\ldots,y_{i,t}^{k_{trn}} , along with binary verification outcomes v i , t 1 , … , v i , t k t r n v_{i,t}^{1},\ldots,v_{i,t}^{k_{trn}} . We follow AlphaVerus’s few shot prompting setup ( Aggarwal et al., 2024 ) with a 1-shot example. We found that while increasing the number of few-shot examples improved performance, it also increased runtime substantially because solving is the most computationally intensive part of the pipeline, and the method was improving without more few-shot examples.
#### Rejection-Finetuning.
The solver is updated through rejection fine-tuning (RFT) ( Singh et al., 2024 ) , where the base model is fine-tuned only on verified solutions. Formally, we construct the training data for a single iteration of RFT as D t ∗ ← { ( x i , y i , t j ) : i ∈ D t , v i , t j = 1 } D_{t}^{*}\leftarrow\left\{(x_{i},y_{i,t}^{j}):i\in D_{t},v_{i,t}^{j}=1\right\}
We then trim D t ∗ D_{t}^{*} to keep a maximum of one solution to each problem i i if there are multiple values of j j s.t. v i , t j = 1 v_{i,t}^{j}=1 . The solver is then updated by minimizing the cross-entropy loss: ℒ ( θ ) = − 1 | D t ∗ | ∑ ( x i , y i j ) ∈ D t ∗ ∑ k = 1 | y i j | log p θ ( y i j [ k ] ∣ x i , y i j [ < k ] ) \mathcal{L}(\theta)=-\frac{1}{|D_{t}^{*}|}\sum_{(x_{i},y_{i}^{j})\in D_{t}^{*}}\sum_{k=1}^{|y_{i}^{j}|}\log p_{\theta}(y_{i}^{j}[k]\mid x_{i},y_{i}^{j}[<k]) where θ \theta is initialized from θ 0 \theta_{0} , y i j [ k ] y_{i}^{j}[k] is the k k -th token of solution y i j y_{i}^{j} , and y i j [ < k ] y_{i}^{j}[<k] denotes all preceding tokens. Iteratively training on verified solutions in this way can be seen as an offline RL algorithm based on expectation-maximization ( Singh et al., 2024 ) . Further details about SFT training can be found in Appendix E .
In principle, different reinforcement learning algorithms could have been used, such as GRPO ( Shao et al., 2024 ) . We use RFT because the Verus verifier is guaranteed to be sound but not complete, meaning that advantage-weighted algorithms could incorrectly punish models for correct solutions that were judged to be incorrect. Future work on on-policy RL algorithms for formally verified self-play may investigate more performant RL algorithms in this setting.
#### Proposing.