Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Building A Proof-Oriented Programmer That Is 64% Better Than GPT-4o Under Data Scarsity

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked every number in Tables 1 to 4 and Figure 4, page and section references, quotations, step lists and appendix prompts; changed the repair-versus-resampling claim (true only for the last three fine-tuned rows), the six-model count and best-in-F* claim, the 64% derivation, the seed-dataset attribution, the generator-choice wording, the Table 3 and 4 cross-reference, the two repair caps, and six unmarked inferences; could not check the Verus forms against a source.

source: Zhang, Wang and Sun, arXiv:2502.11901v2 (13 Apr 2025), 18 pages with appendices A to D. The PDF’s own title spells the last word “Scarcity”. An abstract-level entry on the same paper (PoPilot) is in the notes file c_and_systems_proofs.md; what follows is from the full text.

the paper in short

The authors fine-tune a 14B code model (Qwen2.5-Coder-14B, LoRA) to write and repair F* proofs, and call it PoPilot. F* is an SMT-backed verification language, the closest relative of Verus in this batch. The whole contribution is a way to make training data when almost none exists: have weak LLMs write many F* problems and solutions, keep what the F* checker accepts, and turn what it rejects into repair examples. Nothing is proved about the method. What is measured is the share of held-out F* problems for which some sampled answer passes the checker.

The reason this works at all is stated once, plainly: “Therefore, no extra effort such as test cases and LLM judges is required for verifying F* data.” (Section 3.1.2, p.4)

technique 1: verifier-filtered synthetic tasks at function level

what it is: an LLM is shown an existing code snippet and writes a new self-contained task plus its answer; the checker decides whether the pair enters the training set.

when to use: to teach a model the syntax and basic proof habits of a verification language that has little public code. The paper measures how little: F* has 29.6k entries in Stack-v2, under 0.002% (Section 2, p.2).

steps (Section 3.1, p.3 to 4):

  1. seed corpus: code from the F* source repository and from GitHub OCaml (Section 3.1.1)
  2. generators: five open models, chosen as “code LLMs demonstrating relatively superior capability in generating F* code” (Qwen2.5-Coder-32B and 14B, CodeLlama-13b, DeepSeek-Coder-V2-Lite, DeepSeek-R1-Distill-Qwen-32B); “All promptings are done in zero shot.” and the temperature is 0.7 (Section 5.1, p.6)
  3. task type A, natural language to code: the model writes an instruction and a response from a seed snippet. A rule that matters for step 6: “The response code generated by the model is also required to be self-contained to facilitate the verification of code correctness and the generation of other types of tasks.” (p.3)
  4. task type B, proof-oriented completion: take a verified, self-contained snippet from earlier answers and ask the model for a problem that requires proving a property of it. Outputs feed back in: “Verified response codes can also be reused as snippets for future code completion tasks.” (p.3)
  5. task type C, repair: “Code repair pairs in our dataset are generated by prompting the model to fix the given incorrect code response, supplying both the erroneous code and the execution log obtained after verification.” (p.3 to 4)
  6. filter by running F*: “Data that successfully compile and run are retained, while incorrect ones and their associated error messages are stored for inclusion in the repair dataset.” (Section 3.1.2, p.4)

Figure 2 (p.3) shows one such pair. The snippet defines list_with_length, which returns a list paired with its length. The generated task is to prove that the second component equals the length of the input. The answer is a val lemma_length_preserved with requires True and an ensures stating the equality, and a body that is one assert of the same equality.

Verus form. Inference: the unit of data is one file holding spec fn definitions, one proof fn with requires and ensures, and its body; type B hands over the spec functions and asks for a property of them, stated and proved. Figure 2 becomes a spec fn list_with_length(l: Seq<int>) -> (Seq<int>, nat) and a proof fn lemma_length_preserved(l: Seq<int>) ensures list_with_length(l).1 == l.len() with an empty body, since the solver unfolds the definition. Two things differ from F*. First, the filter must reject files that pass by an escape: assume(...), admit(), #[verifier::external_body]. The paper names no such scan for F*, where admit exists too. Second, a self-contained Verus file still needs the standard library import, so the wrapper is fixed text and only the middle is generated.

evidence (Table 1, p.6; test set of 2,000 held-out instructions drawn from the synthesized F* data itself, split evenly over the three task types; Pass@1, then accuracy after one repair attempt, generation temperature 0.1; base model Qwen2.5-Coder-7B unless marked):

  • untuned 7B: 0.25, after repair 0.30
  • 54K synthetic F* only: 0.42, 0.47
  • 93K synthetic F* only: 0.48, 0.52
  • GPT-4o: 0.60, 0.70; DeepSeek-V3: 0.66, 0.78

limits: the test set comes from the same generator pipeline as the training set, so the tuned models are tested on their own distribution and the baselines are not. Inference: Table 1 therefore shows that the model learned this task family; how far that carries to proofs people write by hand is shown only by the repository-level results below. The paper counts neither how many generated pairs the filter threw away nor how trivial the kept properties are.

technique 2: dilute the target language with other code data

what it is: mix instruction data from other languages and from Lean proofs into the F* set before fine-tuning.

when to use: when the target-language set is small and synthetic, so that the model keeps general coding and instruction-following ability.

steps (Sections 3.2 and 5.1): add CodeAlpaca, Evol-Instruct, Deepseek-Prover-V1 (Lean 4 proofs), RunBugRun (program repair) and stack-exchange-preferences. Table 1’s caption gives the sizes used: Evol 80K with the 54K F* set or 50K with the 93K set, DSP-V1 20K, CodeAlpaca 15K, RunBugRun 15K. The stated motive: “Therefore, we integrate diverse instruction-tuning data pairs in other languages besides synthetic F* data to supplement our dataset and enhance model’s capability.” (Section 3.2, p.4)

evidence (Table 1, same setting as above, 7B base):

  • 54K F* plus Evol: 0.52, 0.56 (from 0.42, 0.47)
  • 93K F* plus DSP-V1: 0.52, 0.54
  • 93K F* plus DSP-V1, Evol, CodeAlpaca, RunBugRun: 0.58, 0.62
  • the same mixture on the 14B base: 0.74, 0.77
  • the last row, “- F* NL2Code”, reads 0.48 and 0.52; the paper does not say which mixture it was removed from

Verus form. Inference: nothing changes in kind. The mixture for a Verus model would be synthetic Verus files plus Rust instruction data, plus Dafny or F* proofs as the nearest SMT-backed relatives. The paper tests Lean data as the proof-language additive and never tests another SMT-backed language, so that last choice is a guess.

limits: each row changes more than one thing (the Evol amount differs between the 54K and 93K rows), and there is one run per row with no variance, so the table supports “mixing helped here” and no ranking of the additives.

technique 3: new repository-level problems grown from real ones

what it is: for each real definition inside a verified repository, show the model its file context and a few neighbours, and ask for a different type declaration plus a definition that satisfies it, then keep the pairs F* accepts in that context.

when to use: when the proofs that matter depend on project context (opened modules, earlier lemmas) and the real projects are too few to train on.

steps (Section 4.1, p.4; prompt in Appendix C.3, p.15 to 16):

  1. start from a seed dataset whose entries have three parts: the definition (a type declaration and its proof), the context (opened modules, earlier definitions, and premises selected as likely to be used), and examples (similar pairs from the same context, found by embedding similarity of their types)
  2. build the prompt from premises, opened modules and several example definitions of varied structure. The C.3 prompt tells the model to write “a different type declaration and a corresponding definition”, to start them with val and let, to end with END, to use only the listed premises, and not to copy the examples
  3. sample: “For each unique context in the seed dataset, we apply the predefined prompt template and sample multiple candidate problem-solution pairs using two LLMs.” (p.4)
  4. filter: drop definitions too similar by sequence similarity to each other or to the reference examples, and drop any that overlap with the test set
  5. validate by running F* (the Section 3.1.2 filter again, per Section 6.2, p.7)

Prompt sizes for the solving prompt, as opposed to the problem-making prompt, are in Appendix A.2 (p.12): “For definition generation prompt, we will provide the type declaration, set the max prompt length to 4096 tokens, and use all the opened modules and premises, 15 selected premises the model may use, and 10 retrieved related examples.”

Verus form. Inference: the F* val (a type that is the statement) maps to a Verus signature with requires and ensures, and the F* let maps to the body. The context is the use lines, the spec fn definitions in scope, and candidate proof fn lemmas from the same crate. Asking for a different statement in the same context carries over directly. What does not carry over is the breadth of the seed: the paper’s seed has 30K existing definitions (Table 2 caption), and public Verus code is, I assume, much smaller (not checked), so each context would have to yield more variants and the similarity filter would bite harder.

evidence (Table 2, p.8; 1K held-out repository-level problems; Qwen2.5-Coder-14B fine-tuned; Generate@5, then problems additionally solved by repair, then the total over 10 samples, then Generate@10, all in percent of the 1K):

  • existing repositories only (30K): 30.7, 1.0, 31.7, 35.3
  • plus 30K synthetic project proofs: 32.2, 2.2, 34.4, 36.2

limits: the model invents the statement as well as the proof, and the only check is the type checker, so a statement can be true and worthless. The paper’s own caveat is about length: “Figure 3 shows that the problem-solution pair augmentation is effective for simpler definitions but struggles with longer and more complex ones, reflecting the long-tailed distribution observed in both real-world and synthesized datasets.” (Section 4.1, p.5). The gain from 30.7 to 32.2 is 15 problems of 1,000 in a single run.

technique 4: repair data from two sources, mutation and model failures

what it is: training triples of (statement, wrong proof, checker error) with a correct proof as target. One source breaks correct proofs by rule; the other collects what models get wrong.

when to use: to train the repair half of a generate-then-repair loop. The finding below says which source to prefer.

steps, source A, mutation (Section 4.2.1, p.5):

  1. take a ground-truth solution and change it at random at the syntax-tree level
  2. kinds of change: “Mutations include omitting parts, replacing arguments with underscores, and modifying control structures (e.g., removing branches or let-definitions).”
  3. keep it only if it breaks: “If a mutation causes type checking to fail, we treat it as a synthetic error and use it to train a model to recover the original solution.”
  4. one exclusion: “These errors mimic those commonly made by human F* programmers, but we avoid mutating identifiers.”

steps, source B, model failures (Sections 4.1 and 4.2.2, p.5):

  1. pool the seed problems with the new ones from technique 3 and prompt an LLM to solve each in its context
  2. run F*; keep each wrong proof with its compiler message
  3. get the target proof either by prompting LLMs to repair (weak when done zero-shot, the paper says) or by reusing the known correct proof of that problem
  4. filter: remove identical wrong proofs; cap the count per problem; remove targets that appear in the test set

The repair prompt (Appendix C.2, p.14 to 15) frames the wrong proof as an “incorrect student solution”, prints it in full with its module preamble and solver options, marks the failing lines in place with comments of the form // Error Range Start - Line 27 and // Error Range End - Line 27, and appends the error text. Per Appendix A.2 the repair prompt drops the selected premises and uses fewer examples than the generation prompt.

Verus form. Inference: source A on a verified Verus function means deleting one invariant line, one assert, one lemma call, the decreases clause, or one proof { } block, and keeping the result only if Verus now fails. The underscore mutation has no Verus counterpart. Mutating requires or ensures must be excluded, because that changes the problem instead of breaking the proof. Source B is unchanged: keep every failed attempt with Verus’s error text. The in-place error markers are easy to reproduce since Verus reports a line span per failed obligation.

evidence (Table 2, p.8, same setting as technique 3; each row adds to existing repositories plus synthetic project proofs, whose row is 32.2, 2.2, 34.4, 36.2):

  • plus 30K mutation repair data: 32.7, 0.7, 33.4, 37.5
  • plus 30K model-generated repair data: 33.1, 4.2, 37.3, 37.2
  • plus both: 34.0, 4.7, 38.7, 38.0

The paper’s reading of the first row: “(2) Rule-based synthetic repair data alone does not enhance repair performance, suggesting that rule-based errors may not accurately reflect the error situations the model would have encountered.” (Section 6.4, p.7). Repair in fact fell from 2.2 to 0.7 with mutation data alone. On what models get wrong: “We can see that the dominating model-generated errors is identifier not found and syntax error.” (Section 4.2, p.5; Figure 5). Inference: that fits the mutation result, since the mutator is forbidden to touch identifiers and so never produces the most common real error.

limits: the cap in step 4 is stated in two places with different units. Section 4.2 (p.5): “(2) Each definition generation problem contributes at most three repair problems to prevent redundancy.” Section 6.2 (p.7) adds, as a further de-duplication step, at most two instances of each unique type declaration in the repair dataset; the paper does not say how the two caps combine.

technique 5: spend half the sample budget on repairing one failure

what it is: an inference protocol. Draw 5 proofs; if none passes, pick one failed attempt at random and draw 5 repairs of it.

when to use: whenever a fixed number of model calls per problem must be split between fresh attempts and repairs.

steps (Section 6.3, p.7):

  1. sample 5 proofs from the statement and context; “If at least one proof compiles, the problem is solved.”
  2. otherwise store the failed attempts and their error messages
  3. choose one failed attempt at random and generate 5 repair attempts from it
  4. the comparison arm is 10 fresh samples with no repair

A variant was tested and rejected (Appendix D.1, p.16 to 17): repair each of the 5 failed attempts once. Table 3 (p.17) gives the points added over Generate@5 by each variant: for the authors’ best model (Generate@5 34, the 38.7 row of Table 2) 1.7 (each once) against 4.7 (one attempt five times); for Qwen2.5-Coder-32B 0.8 against 7.8; for DS-Coder-33B 4.6 against 9.8. The paper’s explanation is a hypothesis: “Allowing multiple repair attempts on the same problem increases the chances of success, leading to better overall accuracy.”

Verus form. Inference: the protocol is independent of the language. One change is needed for Verus: “compiles” has to mean that Verus reports every function verified and that the scan for assume, admit and external_body is clean.

evidence, generate-then-repair against fresh samples (Table 2, percent of 1K): PoPilot 39.4 against 38.5; GPT-4o 23.9 against 23.8; Qwen2.5-Coder-32B 26.7 against 27.1; DeepSeek-V3 22.3 against 28.6; DeepSeek-Coder-33B 26.9 against 28.8. The same table has seven fine-tuned rows (Gen+Rep against Generate@10): repair wins in the last three (37.3 against 37.2, 38.7 against 38.0, 39.4 against 38.5, so by 0.1, 0.7 and 0.9 points) and loses in the first four (for example 31.7 against 35.3 for existing repositories only). Among the ten untuned baselines it loses for seven, ties for DeepSeek-Coder-V2-Lite (25.1 both) and wins for GPT-4o, Qwen2.5-72B and Llama-3.3-70B. Section 6.3 says the setup exists to compare the two and the paper never states this mixed outcome in words.

technique 6: a small tuned model repairs a large model’s failures

what it is: the large model drafts 5 proofs; its failed outputs go to the small fine-tuned model for the 5 repair attempts.

steps (Section 6.3, “Repair Using Outputs from Other Models”, p.7): as technique 5, with the repairer swapped. The repairer is the model trained on existing repositories plus synthetic project proofs plus all repair data, which is the 38.7 row of Table 2 and not the final PoPilot.

evidence (Figure 4, p.7, percent of the 1K problems after the tuned model repairs each baseline’s failures): Qwen2.5-Coder-32B 31.3, DS-Coder-33B 32.1, GPT-4o 36.9, Qwen2.5-72B 35.0, Llama-3.3-70B 28.3. For GPT-4o that is 22.2 from its own 5 samples, 23.9 with its own repair, 36.9 with the tuned repairer.

Verus form. Inference: this is the cheapest of the six to try for VL, because it needs no change to the drafting agent. It needs a Verus repair model, which needs technique 4’s source B data first.

limits: the tuned model’s own Generate@5 on these problems is 34.0, so (inference) a share of what it “repairs” it could have solved from scratch. The paper has no arm in which the tuned model sees the statement without the failed draft, so the draft’s contribution is unmeasured.

what is measured and what stays trusted

Headline. Inference: the paper does not show its computation; 64% matches PoPilot’s 39.4 over GPT-4o’s 23.9 in the 10-sample generate-then-repair column of Table 2 only if truncated (39.4 / 23.9 = 1.648, which rounds to 65%). 54% is 36.9 over 23.9 (1.54), GPT-4o’s drafts repaired by the tuned model against GPT-4o repairing itself. Both are relative gains on 1K problems in one run; the absolute gains are 15.5 and 13.0 points, and 60.6% of the problems stay unsolved by PoPilot.

Training setup (Appendix A.3, p.12): one epoch, LoRA rank 32 and alpha 32, learning rate 1e-5, batch size 64. PoPilot’s mixture per the Table 2 caption: 30K existing definitions, 30K synthetic project proofs, both repair sets of 30K each, and 180K mixed function-level data.

Trusted: the F* checker and its solver; the seed dataset and its premise selection (the paper cites Chakraborty et al., 2024 for retrieving similar examples by type embedding and Yang et al., 2023 for the selected premises, and does not say where the seed dataset comes from); that an accepted answer contains no admit or assume (no check is described); that removing test-set overlaps by similarity is enough to stop leakage from the same repositories. The paper tests F* only: “This work focuses on the programming language of F*, but did not experiment with other languages due to their lack of well-established evaluation suite.” (Limitations, p.9)

where the text and the tables disagree

  • Section 5.3 (p.6) ends a sentence with the claim that the tuned model “achieves the best performance in both generation and repair within the F* framework”. The sentence compares with 6 open-source models and lists six (Qwen-2.5-coder 7B, 14B and 32B, Qwen-2-72B, DeepSeek-Coder-V2-Lite, LLaMa-3.1-70B), all of which the 14B tuned model beats in Table 1. DeepSeek-V3 is not in that list and scores 0.78 after repair against the tuned model’s 0.77, so the claim holds only for the six; Table 1 has ten baseline rows, GPT-4o among them.
  • Section 6.4 (p.8) says model-generated repair data improves “repair accuracy (from 32.2 to 33.1) and generation accuracy (from 2.7 to 4.2)”. In Table 2, 32.2 and 33.1 are Generate@5 values and 4.2 is a Repair@5 value, so the labels are swapped; and the row being compared has Repair@5 of 2.2, while 2.7 belongs to a different row.
  • Qwen2.5-Coder-32B has two sets of numbers: 24.2, 2.5, 26.7 in Table 2 and 23.5, 0.8, 24.3 in Table 4 (p.18). Table 3 also uses 23.5.
  • Table 3 puts 0.8 (Qwen 32B) and 4.6 (DS-Coder-33B) in the column for the rejected variant, one repair per failed attempt. The same 0.8 appears as Repair@5 for Qwen2.5-Coder-32B in Table 4 (Table 2 gives 2.5), and 4.6 for DS-Coder-33B in Tables 4 and 2. Yet for the tuned model, Table 2’s 4.7 matches the chosen variant. Inference: the baselines’ repair numbers in the main table may come from the weaker protocol, which would overstate the gap in repair. The paper does not resolve this.
  • Table 4: the 7B model fine-tuned on the full PoPilot data reaches Generate@5 of 21.9, below the untuned 7B’s 23.4 in Table 2, and the 7B tuned on existing repositories alone reaches 12.9. Appendix D.2 calls the small model “reasonably good” without remarking that fine-tuning lowered Generate@5.
  • The abstract says the gain over GPT-4o is “by 54%”; the introduction says PoPilot can boost GPT-4o’s performance “to 54%”. Figure 4’s 36.9 supports the first wording only.
  • Appendix A.3’s hardware line is garbled in the PDF (stray digits), so the GPU count cannot be read.

what is already done, and threat to VL

Done here and not worth redoing: showing that checker-filtered synthetic data lifts a small open model above untuned large ones on SMT-backed proof completion; the comparison of mutation-made against model-made repair data, which model-made data wins; the two repair-sampling variants.

Open after this paper (inference): the same recipe for Verus (the authors name “verified Rust” among low-resource proof languages in Section 2 and test only F*); any measure of whether synthetic statements are worth proving; tasks beyond one definition per problem.

Threat. Inference: low as a product, moderate as a cost trend. PoPilot fills in one F* definition given its type and context, at 39.4% with ten samples; it does not write specifications, choose what to verify, or handle Rust. The part that bears on VL is technique 6: a 14B model repaired 13 points more of GPT-4o’s failures than GPT-4o did. If that holds for Verus, proof repair inside an agent loop can move to a small specialized model, and a competitor with a Verus corpus could offer it cheaply.

techniques for the catalog

  • verifier-filtered synthetic tasks — have code LLMs write self-contained problem and answer pairs from seed snippets and keep only those the proof checker accepts, routing rejects with their errors to a repair set
  • snippet recycling for proof tasks — reuse each verified answer as the seed snippet for a new task that asks to prove a property of it
  • cross-language data mixing — add general code instruction data and proofs from another prover to the small target-language set before fine-tuning
  • in-context statement synthesis — given a real definition’s opened modules, premises and similar examples, ask for a different statement plus proof in that context and validate it with the checker there
  • similarity and test-overlap filter — remove generated definitions that are near-copies of each other, of the prompt examples, or of test items
  • mutation-made repair data — break correct proofs by syntax-tree edits that leave identifiers alone and keep the ones that fail checking; measured here as no help on its own
  • model-made repair data — collect a model’s own failed proofs with compiler errors and pair them with the known correct proof as target; measured here as the repair data that helps
  • error-range markers in the repair prompt — print the failed proof with comment lines bracketing the failing span, followed by the error text
  • sample 5 then repair one failure 5 times — split a 10-call budget into fresh samples and repeated repairs of one randomly chosen failed attempt, which beat repairing five failures once each
  • small tuned repairer for a large drafter — send a large general model’s failed proofs to a small fine-tuned model for repair

Last edited: