Builds a benchmark of Lean-certified behavior-preserving refactorings of VERINA tasks and re-checks fixed Lean proofs against them to measure proof survival.
Abstract
Benchmarks for verifiable code generation usually test a proof against one fixed implementation. We ask whether the same proof remains valid after a program refactoring that preserves behavior. We introduce RefactorProof, which derives 458 Lean-certified variants from the 185 VERINA tasks that compile in our pinned environment while holding the specification and evaluated proof fixed byte-for-byte. VERINA supplies reference proofs for 46 tasks, all from its basic split; the primary model-versus-reference comparisons further match on 21-25 short, non-recursive tasks. Structural refactorings expose substantial brittleness across proof sources: task-normalized structural PSR is 4.3% for the supplied references and 13.3-26.8% for the specialized provers. On the matched tasks, specialized prover proofs nevertheless have higher overall unchanged-proof survival than the supplied reference artifacts: +15.6 points for DeepSeek-Prover-V2-7B, +18.8 for Goedel-Prover-V2-32B, and +20.3 for Goedel-Prover-V2-8B; all three 95% CIs exclude zero. The ordering persists after excluding universally survived T1 variants, under family-balanced aggregation, and under alternative deployable valid-proof selection rules. However, unchanged-proof failure is not the same as high repair cost: predefined one-identifier edits repair 51/54 eligible reference structural failures and 58/85 eligible prover failures. RefactorProof therefore measures unchanged-proof stability under program refactoring, not the cost of maintaining a proof after it breaks.
Problem
Benchmarks for verifiable code generation check a proof against one fixed implementation. It is unclear whether LLM-generated and reference proofs stay valid after behavior-preserving refactorings of the program.
Approach
RefactorProof applies five deterministic transformation families (let-introduction, helper extraction, commutative swap, condition inversion, branch extraction) to the implementations of VERINA tasks. Each variant is kept only if Lean proves its equivalence to the original in a separate file. The specification and proof are held byte-identical, and the unchanged proof is then re-checked against the new implementation. Proof survival rate (PSR) is compared across reference proofs and specialized provers, with sensitivity analyses and a mechanical one-identifier repair experiment.
Figure 1: RefactorProof evaluation design and a T2 helper-extraction example. (a) Each candidate refactoring C^{\prime} is kept only if Lean separately proves \forall\bar{x}.\,C(\bar{x})=C^{\prime}(\bar{x}) ; candidates for which the fixed automatic certificate search finds no proof are excluded and are not thereby shown incorrect. The specification S and proof P remain byte-identical, the certifi
Results
The benchmark contains 458 certified variants from 185 tasks. Structural refactorings break most proofs: structural PSR is 4.3% for reference proofs and 13.3–26.8% for provers. On matched tasks, DeepSeek-Prover-V2-7B and Goedel-Prover-V2 proofs survive 15.6–20.3 points more often than the references. One-identifier edits repair 51/54 eligible reference structural failures and 58/85 eligible prover failures.
Proof source
Tasks
Overall PSR (%)
D
S
E
DeepSeek-Prover-V2-7B
31
59.3
100.0
13.3
72.2
Goedel-Prover-V2-32B
26
64.5
100.0
26.0
67.6
Goedel-Prover-V2-8B
29
64.6
100.0
26.8
72.4
reference
46
47.9
100.0
4.3
44.2
Overall PSR by proof source and transformation class
