Propose, Solve, Verify: Self-Play Through Formal Verification — part 2/3

Cleaned-text code points [15202, 31147). Bibliography omitted here; source.md includes it.

At iteration t t , proposer P ϕ , t P_{\phi,t} generates B B new problem specs at target difficulty levels by conditioning on problems and associated difficulty labels. We estimate the difficulty of question x i x_{i} at iteration t t by the current solver’s pass rate on that problem: r i , t = 1 k t ​ r ​ n ​ ∑ j = 1 k t ​ r ​ n v i , t j r_{i,t}=\frac{1}{k_{trn}}\sum_{j=1}^{k_{trn}}v_{i,t}^{j} We categorize problems into one of four classes based on r i , t r_{i,t} : Easy , Medium , Hard , and Impossible : difficulty ​ ( x i , t ) = { Easy if ​ r i , t ≥ τ E Medium if ​ τ M ≤ r i , t < τ E Hard if ​ 0 < r i , t < τ M Impossible if ​ r i , t = 0 , \text{difficulty}(x_{i},t)=\begin{cases}\textsc{Easy}&\text{if }r_{i,t}\geq\tau_{E}\\ \textsc{Medium}&\text{if }\tau_{M}\leq r_{i,t}<\tau_{E}\\ \textsc{Hard}&\text{if }0<r_{i,t}<\tau_{M}\\ \textsc{Impossible}&\text{if }r_{i,t}=0,\end{cases} where the thresholds τ E \tau_{E} and τ M \tau_{M} are hyperparameters for our method.

We then sample k p ​ r ​ o ​ p k_{prop} problems from D t D_{t} to use as examples and ask the proposer to output a question at a target difficulty level. A simplified version of our prompt is below, and the complete prompt is in Appendix A . This mechanism continually refreshes the prompt distribution, updating the proposer to P ϕ , t + 1 P_{\phi,t+1} through in-context learning and expanding the problem frontier in a difficulty-controlled manner.

After inference, specifications are parsed, deduplicated, and filtered through a spec verifier which ensures that the spec defines a valid set of mathematical pre- and post-conditions. This uses a form of Verus that ignores the implementation body – details are in Appendix D .

## 4 Experiments

We study self-play verified code generation in the Verus language ( Lattuada et al., 2023 ) .

#### Datasets and evaluation.

We evaluate our approach using three Verus datasets. Dafny2Verus (274 problems) is a translation-derived corpus adapted from the AlphaVerus ( Aggarwal et al., 2024 ) pipeline, providing a diverse set of formally verified Dafny problems translated into Verus. MBPP -Verified (78 problems) is based on the MBPP dataset ( Austin et al., 2021 ) , following the verified adaptation process described in ( Yang et al., 2025a ; Misu et al., 2024 ) , where each task includes executable Rust+Verus specifications and proofs. HumanEval -Verified (85 functions across 49 original programs) is drawn from an open-source HumanEval-Verus effort ( Contributors, 2024 ) , which translates Python HumanEval tasks ( Chen et al., 2021 ) into Verus. Each multi-function program is decomposed into independently verifiable functions, ensuring all necessary dependencies are preserved. All datasets require generating Rust+Verus code that passes the Verus verifier ( Lattuada et al., 2023 ) . We will omit the *-Verified from the names for brevity throughout the rest of the paper. We adopt the widely used Pass@ k k metric ( Chen et al., 2021 ) : for n n samples and c c verified successes, pass@ k = 1 − ( n − c k ) / ( n k ) k=1-\binom{n-c}{k}/\binom{n}{k} . We measure Pass@1, 5, and 10, and run our final evaluation with n = 100 n=100 to provide a strong unbiased estimate of the evaluation metrics.

#### Settings.

We study our method’s performance in two settings. In a setting we refer to as transfer learning we set X 0 X_{0} to the set of questions in Dafny2Verus and report performance on MBPP and HumanEval as a held out test set. In a setting that we refer to as test-time training (TTT) ( Sun et al., 2020 ) , we set X 0 X_{0} to the set of questions in each dataset, and run our method on that dataset alone. It is worth noting that human-written solutions are never trained on .

#### Baselines.

We compare to AlphaVerus ( Aggarwal et al., 2024 ) (no treefinement version), which is the previous SOTA method for verified code generation based on prompting with 50 in-domain exemplars. We also compare to iterative RFT ( Yuan et al., 2023 ; Singh et al., 2024 ) , which performs expert iteration without proposing new problems. We train and evaluate RFT with the same parameters as our method, excluding any parameters related to question proposal.

#### Hyperparameters and design choices.

Our hyperparameters and design choices were selected to provide a proof of concept of our idea at minimal compute scale. In the current setting, the main experiment (Table 1 ) takes around 24 hours on a single machine with 8xL40s GPUs. We use the Qwen2.5-Coder-3B-Instruct model as our base because it was the strongest open-weight code model at the 3B size. We use SGLang ( Zheng et al., 2024 ) with dp-size=8 and temperature 0.8 for all inference sampling because SGLang has large efficiency gains for inference time sampling and can parallelize over multiple GPUs on the same machine easily. We set τ M \tau_{M} to 0.2, similar to Dong and Ma (2025) (who used 0.25), and set τ E \tau_{E} to 0.8. We set k t ​ r ​ n k_{trn} to 10 to balance having enough breadth in our search to enable performance improvements and not so much that the computational requirements would become unreasonable to reproduce. We use k p ​ r ​ o ​ p = 12 k_{prop}=12 and use uniform input and output targets, meaning that we populate the proposer prompt with 3 problems for each difficulty class, and ask for B / 4 B/4 problems of each difficulty class as the output. We justify the choice of uniform input/targets in Appendix B , and vary the number of iterations T T and proposer budget B B in our analysis (§ 6 ).

## 5 Results

We investigate PSV-Verus ’s performance on our two experimental settings: transfer learning and test-time training . Table 1 presents our main results on three benchmarks: Dafny2Verus, MBPP-Verified, and HumanEval-Verified. PSV-Verus consistently outperforms both the AlphaVerus and the RFT baselines across all metrics.

#### Transfer learning

PSV-Verus achieves strong cross-domain generalization, scoring 25.25% pass@1 on MBPP and 16.18% on HumanEval, outperforming AlphaVerus (6.48%, 7.24%) and RFT (10.99%, 10.99%) by 3.90 × \times and 2.30 × \times on MBPP and 2.24 × \times and 1.47 × \times on HumanEval, respectively. These results demonstrate that training on Dafny2Verus generalizes robustly across domains, yielding substantial gains on realistic natural-language programming benchmarks.

#### Test-time training

On Dafny2Verus pass@1, PSV-Verus achieves 65.63%, compared to AlphaVerus’s 24.06% (a 2.73 × \times improvement) and RFT’s 34.46% (a 1.90 × \times improvement). On MBPP pass@1, PSV-Verus reaches 36.78%, outperforming AlphaVerus’s 6.48% (5.68 × \times ) and RFT’s 3.83% (9.61 × \times ), and on HumanEval pass@1, PSV-Verus achieves 19.07%, compared to AlphaVerus’s 7.24% (2.63 × \times ) and RFT’s 5.56% (3.43 × \times ). On Dafny2Verus pass@10, PSV-Verus outperforms RFT by 1.26 × \times and AlphaVerus by 1.26 × \times . Averaged across all benchmarks and metrics, PSV-Verus obtains 48.12%, compared to 25.43% for RFT and 25.55% for AlphaVerus, representing mean improvements of 1.89 × \times and 1.88 × \times , respectively. Performance graphs for each task are in Figure 4 , where the trends of improving over iterations become clear.

## 6 Analyses and Ablations

In the sections that follow, we investigate how our method scales with the number of generated questions (§ 6.1 ) and iterations of the algorithm when the number of proposed questions is held constant (§ 6.2 ) – experiments that articulate the scaling properties of our method with respect to increasing compute. We also analyze the importance of formal verification and factors impacting the effectiveness of the question proposal through ablation experiments in § 6.3 to better understand their impact on self-play performance.

### 6.1 Scaling with Questions Per Iteration

The first scaling factor we consider is the number of questions per iteration B B , because it can be scaled in parallel across many machines simultaneously without any blocking factors. Results for the test-time training setting are shown in Figure 5 .

On Dafny2Verus, scaling from 4k to 32k questions per iteration yields consistent improvements: pass@1 increases from 59.5% to 74.3% ( +25% relative ), pass@5 from 73.8% to 82.6% ( +12% ), and pass@10 from 75.8% to 83.6% ( +10% ). On MBPP, scaling from 1k to 32k questions yields pass@1 improvements from 22.3% to 44.3% ( +98% ), pass@5 from 39.7% to 57.8% ( +46% ), and pass@10 from 44.8% to 61.1% ( +36% ). HumanEval shows similar gains: pass@1 from 13.9% to 26.3% ( +89% ), pass@5 from 16.4% to 32.6% ( +99% ), and pass@10 from 17.9% to 34.5% ( +93% ). We also observe positive scaling behavior for transferring from Dafny2Verus to MBPP, though more modest gains for transferring to HumanEval; see Appendix C .

### 6.2 Iterative Training

Next, we are interested in whether the proposer’s budget of generated specifications (i.e., the question budget) should be allocated towards increasing the number of iterations of the method or increasing the number of generated specifications per iteration. We fix the question budget and vary the number of iterations. Figure 6 illustrates a smooth, monotonic improvement as the number of iterations increase. That is, distributing a fixed question budget across multiple of iterations proposing, solving, and updating yields better results than a single large iteration. For example, in the test-time-training setting on Dafny2Verus at a 1k budget, increasing iterations from 1 to 5 boosts pass@1 from 21.0% to 42.3% ( +102% ). The pattern holds at higher budgets: at 2k, pass@1 rises from 26.3% to 44.3% ( +68% ); at 4k, from 28.0% to 46.9% ( +68% ). This effect extends beyond pass@1: at the 4k budget level, pass@5 improves from 50.6% to 62.9% ( +24% ), and pass@10 improves from 60.0% to 66.7% ( +11% ). In summary, holding the number of proposed specifications constant, increasing the number of iterations boosts success rates, showing that iterative training drives performance improvements in our method.

### 6.3 Ablations

Our self-play algorithm PSV-Verus has three key components worth examining through ablation analyses – a verifier that determines whether specs and solutions are correct, and a proposer that outputs diverse solutions by sampling questions to put in the proposer prompt from the ever-growing dataset and that outputs questions of target difficulty by computing and including labels of how difficult questions included in the prompt were for the most recent solver. We decided to ablate each of these components and observe their effect on performance in the transfer learning setting. Our results are in Table 2 and described below in detail.

#### Verification

The Verus verifier is used primarily in our algorithm to check whether solutions are valid for a given spec before training on them. We analyze the impact of this by ablating this step and training on all generated solutions, ignoring the verification signal. Our results are shown in Table 2 under (-Verification). We find that removing solution verification hurts performance significantly, leading to relative drops in performance of 51.5% pass@1 and 29.3% pass@5 for Dafny2Verus, 55.2% and 35.7% for MBPP, and 52.1% and 33.5% for HumanEval.

In addition to performance gains, we also find that verification can be useful for efficiency. We also use verification to filter out candidate specs to make sure they are syntactically compilable before attempting inference on them. This impacts efficiency only, not performance, because the syntactically invalid specs are 100% not solvable, therefore no solution can impact training. We ablated this step and found that the efficiency hit from removing spec verification is substantial: only 47.7% of unique specs were valid on average, so removing spec verification meant that we had to perform pass@10 inference on the remaining 52.3% of specs that were not solvable, a 2.1x increase in inference compute with no resulting performance improvement.

#### Difficulty-awareness

We experiment with removing the difficulty awareness of our proposer by removing the labels for the sampled questions in the proposer prompt. The prompt form is detailed in Appendix G . We found that this -Difficulty ablation causes an average drop of 5.6% across all metrics. Table 2 shows per-dataset comparisons: the drop is statistically significant for 6 of 9 dataset/metric combinations (paired t-test, p < 0.05 p<0.05 ). Notably, all three Dafny2Verus metrics show significant drops, while some HumanEval and MBPP comparisons do not reach significance (MBPP pass@1, HumanEval pass@5,10).

To understand why, we analyze whether the proposer successfully generates questions at the target difficulty. For PSV-Verus , easy-targeted questions have mean pass rate 0.55 0.55 (std 0.47 0.47 ), medium-targeted questions have mean 0.45 0.45 (std 0.42 0.42 ), and hard-targeted questions have mean 0.36 0.36 (std 0.39 0.39 ). The different means but substantial overlap between distributions indicates that difficulty prompting provides partial but incomplete control over generated question difficulty. It seems that difficulty-aware prompting provides a modest benefit despite its imperfect control over generated question difficulty – an area that future work may find fruitful to improve upon.

#### Diversity

We experiment with limiting the diversity of the generated questions by ablating the constantly refreshing proposer prompt with a fixed proposer prompt. We construct this by sampling only once from the seed dataset to get our in-context examples, similar to the fixed prompt in self-instruct pipelines such as Rozière et al. (2023) . This ablation causes an average drop of 10.6% across all metrics. Table 2 show the full results: all Dafny2Verus and MBPP metrics show significant drops (pass@1 drops of 16.3% and 19.7% respectively), while HumanEval pass@5 and pass@10 are lower but do not reach significance.

The mechanism behind this improvement is increased sample diversity: PSV-Verus achieves a higher uniqueness rate on average (45.3% vs 29.3%), which leads to 2.48 × \times more unique questions, and 2.26 × \times more solvable questions used for training the solver, enabling the model to learn from a broader distribution of verified solutions.

## 7 Conclusion

This work set out to investigate a central obstacle to proposer-solver self-play algorithms for language models: obtaining a reliable reward signal that prevents error propagation and reward hacking. While prior self-play successes have largely been confined to domains with trivial or limited-applicability verifiers, we showed that formal verification in a Turing-complete coding language enables self-play in a realistic code-generation setting by providing a sound, non-exploitable training signal. By introducing PSV and applying it successfully to verified Rust programming, we demonstrated that a model can autonomously expand its training curriculum beyond human-written data and steadily improve its capabilities without human supervision. We show that our algorithm displays smooth scaling behavior with respect to the number of generated questions (§ 6.1 ) and iterations (§ 6.2 ), making it an exciting first step in understanding the limits of scaling for self-play reasoning training. In analyzing key components of our algorithm’s design, we observe the importance of formal verification and difficulty-aware and diverse question proposal (§ 6.3 ) in making self-play performant.

## Acknowledgments

This work was also supported in part by the National Science Foundation under Grant Nos. DMS-2434614 and DMS2502281, the Future Enterprise Security initiative at Carnegie Mellon CyLab (FutureEnterprise@CyLab), and AFRL and DARPA under Agreement FA8750-24-9-1000, and by gifts from Amazon, Convergent Research, Microsoft, VMware, and the Beneficial AI Foundation.

## Impact Statement