Benchmarks for verifiable code generation usually evaluate a proof against a single fixed implementation. We introduce RefactorProof, which creates 458 Lean‑certified variants from 185 VERINA tasks that compile in a pinned environment while keeping the specification and the evaluated proof byte‑for‑byte unchanged. VERINA supplies reference proofs for 46 basic tasks, of which 21‑25 short non‑recursive tasks are used for model‑versus‑reference comparisons. Structural refactorings expose substantial brittleness: task‑normalized structural PSR is 4.3% for the supplied references and 13.3%‑26.8% for specialized provers. On the matched tasks, specialized prover proofs still show higher overall unchanged‑proof survival than the reference artifacts, with gains of +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% confidence intervals exclude zero. The ordering persists after removing universally survived T1 variants, using family‑balanced aggregation, and applying alternative deployable valid‑proof selection rules. However, unchanged‑proof failure does not imply high repair cost: predefined single‑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.
Review