Propose, Solve, Verify: Self-Play Through Formal Verification — part 3/3
Cleaned-text code points [31147, 40744). Bibliography omitted here; source.md includes it.
We believe this work could help usher in a future of self-improving models through self-play. This comes with ethical concerns, but so too does it have the potential to enable a more equitable future where reasoning can emerge in many domains—more dependent on the properties of the generation-verification gap in that domain than on the capability to collect costly human reasoning traces (a capability usually only the highly resourced possess).
## Appendix A Full Proposer Prompt
## Appendix B Input & Target Proposal Settings
We investigated different input and target proposal settings – e.g., using all problem types as the input to the proposer, asking for Uniform problem types as output target, or perhaps asking for only one class of problems as output (e.g., Easy, Hard). We tested three alternatives to our method: All → \rightarrow Hard, Easy → \rightarrow Hard (motivated by Luo et al. (2023) ), and All → \rightarrow Easy. We found that our model’s setting worked the best (All input problem types → \rightarrow Uniform output targets). This may be partially explained by the ablation in § 6.3 , where we found that removing sampling of the inputs in the proposer hurt performance. Our results suggest that taking in as much of the seed dataset as possible (not limiting input problems to a specific difficulty type) and using that to generate as diverse a sampling of problems as possible is the best approach.
## Appendix C Transfer Learning Scaling Results
We also evaluate how PSV-Verus scales in the transfer learning setting, where we train on Dafny2Verus and evaluate on MBPP and HumanEval. On MBPP, scaling from 4k to 32k questions per iteration yields consistent improvements: pass@1 increases from 21.8% to 32.0% ( +47% ), pass@5 from 34.4% to 42.6% ( +24% ), and pass@10 from 37.3% to 44.5% ( +19% ). In contrast, HumanEval shows minimal scaling effects: pass@1 remains essentially flat (14.4% to 14.3%, -1% ), while pass@5 and pass@10 show marginal gains (+4% and +3%, respectively). This is supported by prior work ( Aggarwal et al., 2024 ) which found limited transfer between Dafny2Verus and HumanEval-Verified.
## Appendix D Spec Compilation
In Verus, specifications define the contract a function must satisfy—preconditions ( requires ) and postconditions ( ensures ). To test whether a specification is well-formed without requiring a correct implementation, we use the #[verifier::external_body] attribute. This tells Verus to trust the function signature and specification without verifying the implementation body.
### Example: Finding the Maximum Element
The external_body stub uses assume(false); arbitrary() to satisfy Verus’s type checker without a real implementation. This allows us to verify that the specification itself is syntactically valid and logically consistent, independent of any implementation.
The verified implementation includes loop invariants that mirror the postconditions, allowing Verus to prove the implementation satisfies the specification. The invariants maintain that: 1. All elements seen so far are ≤ \leq max
2. The current max value exists somewhere in the portion of the array already traversed
## Appendix E Supervised Fine-Tuning (SFT) Training Details
We perform all supervised fine-tuning (SFT) using the SFTTrainer implementation from the Hugging Face trl library. 2 2 2 https://huggingface.co/docs/trl/en/sft_trainer The training setup mirrors standard LoRA-based fine-tuning for decoder-only models, with lightweight adaptation for efficiency on a single GPU. All experiments are conducted using accelerate to scale to distributed configurations, though all runs reported in the main results with the Qwen2.5-3B-Coder model use a single NVIDIA A6000 GPU (no DDP).
Each run takes approximately 20 minutes at the final iteration of the main experiments (with the most sft data). Checkpoints are saved every 5 steps, retaining only the latest one to minimize storage.
#### Reproducibility.
All code for SFT training, including configuration files and launcher scripts, is available in the project repository for full reproducibility, and is run automatically as a subprocess during the main entrypoint script.
## Appendix F Verification Background
Denote a problem as x ∈ 𝒳 x\in\mathcal{X} , and its associated set of acceptable programs as Y x ⊆ 𝒴 Y_{x}\subseteq\mathcal{Y} . Here 𝒳 \mathcal{X} is a problem domain and 𝒴 \mathcal{Y} is the set of possible programs. Intuitively, the term acceptable corresponds to the notion of a “correct solution”.
Let Z x v ⊆ 𝒴 Z_{x}^{v}\subseteq\mathcal{Y} be the set of programs for which a binary verifier v v returns 1 for problem x x , i.e. Z x v = { y ∈ 𝒴 | v ( x , y ) = 1 } . \displaystyle Z_{x}^{v}=\{y\in\mathcal{Y}\ |\ v(x,y)=1\}. (1) We say that program y y is verified according to v v when y ∈ Z x v y\in Z_{x}^{v} .
We refer to Z x v Z_{x}^{v} as an accepted set (for verifier v v , on problem x x ; we occasionally do not state these distinctions for brevity).
By soundness we mean that every program verified according to v v is an acceptable program: Z x v ⊆ Y x . \displaystyle Z_{x}^{v}\subseteq Y_{x}. (2) Namely, we say that verifier v v is sound for problem x x if the relationship above holds, and unsound for problem x x if the relationship above does not hold. We say that the verifier is sound if it is sound for all problems x ∈ 𝒳 x\in\mathcal{X} . We say that the verifier is unsound if it is unsound for at least one problem x ∈ 𝒳 x\in\mathcal{X} .
By completeness we mean that every acceptable program is verified according to v v : Y x ⊆ Z x v . \displaystyle Y_{x}\subseteq Z_{x}^{v}. (3)
We say that verifier v v is complete for problem x x if the relationship above holds, and incomplete if the relationship does not hold. We say that the verifier is complete if it is complete for all problems x ∈ 𝒳 x\in\mathcal{X} . We say that the verifier is incomplete if it is incomplete for at least one problem x ∈ 𝒳 x\in\mathcal{X} .
#### Test-case verification is unsound.
A test suite can be seen as a verifier v T v_{T} that returns 1 when a program passes all tests in the suite T T , and 0 otherwise. It induces a subset of programs that pass all tests in T T , Z x v T = { y ∈ 𝒴 | y passes T } Z_{x}^{v_{T}}=\{y\in\mathcal{Y}\ |\ y\text{ passes T}\} .
When we say that test case verification is unsound, we mean that for some problem x x , there exists a program y y that passes the test cases but is not actually correct: ∃ x ∈ 𝒳 s.t. Z x v T ⊈ Y x . \displaystyle\exists x\in\mathcal{X}\text{ s.t. }Z_{x}^{v_{T}}\not\subseteq Y_{x}. (4)
It is easy to construct such an example. For instance, consider the problem of writing a program to check whether an input integer is prime, and a single test that checks if the program returns True for input 3. Then a program return n == 3 would pass the tests, but it is clearly not an acceptable program for the problem. In practice, unsoundness of test-case verification is widely observed in the context of LLM code generation and evaluation (e.g., ( Liu et al., 2023 ) ).
#### Formal verification is sound with respect to the specification.
In this setting, we take 𝒳 \mathcal{X} to be the set of specifications in a formal verification language such as Verus or Dafny. In our setting, x x is a specification (e.g., preconditions and postconditions), Y x Y_{x} is the set of programs that satisfy x x , and v F v_{F} is the Verus verification procedure. Verus is an SMT-based verifier: it translates a program and specification into verification conditions and discharges them with an SMT solver. When Verus verifies a program, the result is sound with respect to the specification, up to the trusted computing base ( Lattuada et al., 2023 ) : y ∈ Z x v F ⟹ y ∈ Y x . \displaystyle y\in Z_{x}^{v_{F}}\implies y\in Y_{x}. (5) That is, if v F ( x , y ) = 1 v_{F}(x,y)=1 then y y satisfies the specification x x .
However, formal verification tools like Verus or Dafny are incomplete. This is fundamental: no (general-purpose) program analysis for Turing-complete languages can be both sound and complete ( Rice, 1953 ) . Hence, for a problem x x , it may be the case that Z x v F ⊂ Y x Z_{x}^{v_{F}}\subset Y_{x} (note the strict subset), meaning that there are acceptable programs that the verifier rejects. This fundamental incompleteness explains why proof annotations are needed; we can think of adding such annotations as converting a program p ∈ Y x ∖ Z x v F p\in Y_{x}\setminus Z_{x}^{v_{F}} into a program p ′ ∈ Z x v F p^{\prime}\in Z_{x}^{v_{F}} .
## Appendix G Difficulty Unaware Ablation
## Instructions for reporting errors
We are continuing to improve HTML versions of papers, and your feedback helps enhance accessibility and mobile support. To report errors in the HTML that will help us improve conversion and rendering, choose any of the methods listed below:
Click the "Report Issue" ( ) button, located in the page header.
Tip: You can select the relevant text first, to include it in your report.
Our team has already identified the following issues . We appreciate your time reviewing and reporting rendering errors we may not have found yet. Your efforts will help us improve the HTML versions for all readers, because disability should not be a barrier to accessing research. Thank you for your continued support in championing open access for all.
Have a free development cycle? Help support accessibility at arXiv! Our collaborators at LaTeXML maintain a list of packages that need conversion , and welcome developer contributions .