How Stable Are LLM-Generated Proofs Under Program Refactoring? A Stress Test for Verifiable Code Generation

AI summary

Overview

Research area: Formal verification and AI for code — specifically verifiable code generation, where language models produce Lean 4 proofs alongside implementations and specifications.

Technical level: Advanced. The core question is stated plainly, but following the results requires familiarity with Lean, definitional equality, tactics such as unfold/simp/rfl, and the VERINA benchmark.

Scope: The paper introduces RefactorProof, a benchmark of 458 Lean-certified behavior-preserving program variants, and uses it to measure whether an already-valid Lean proof still verifies when only the implementation is refactored while the specification and proof stay byte-identical.

What This Paper Is About

Benchmarks for verifiable code generation typically score a proof on one fixed implementation, but real programs get refactored, and a proof can break even when the refactored program behaves identically. The authors build a benchmark that mechanically rewrites implementations in behavior-preserving ways — with each rewrite separately certified in Lean — and then re-check the unchanged proof against the rewritten program. The goal is to measure proof-artifact stability across proof sources (supplied references versus specialized provers and general models) and to identify which proof styles survive which kinds of change.

Key Contributions

1. A semantics-preserving evaluation protocol. Only the implementation changes; the specification regions and the evaluated proof are held fixed byte-for-byte (SHA-256 asserted). Every retained transformation carries a separate Lean certificate of pointwise equality that is never imported into, or textually present in, the survival file.

2. The RefactorProof benchmark. 458 certified variants derived from the 185 VERINA tasks that compile in the pinned environment, organized into five deterministic transformation families grouped into definitional (D), structural (S), and theorem-certified semantic (E) classes, plus matched proof-survival comparisons and sensitivity analyses for proof selection, aggregation, common support, and certification artifacts.

3. Artifact-level mechanism analysis. An analysis of how proof strategies fail under different refactorings, identifying definitional-equality "bridges" of the form have h : f args = body := rfl as associated with survival under structural refactoring and with failure under semantic refactoring.

4. A controlled mechanical-repair experiment. Three predefined one-identifier edits that separate unchanged-proof stability from simple repair effort.

Main Findings

• Structural refactoring is the weak point for every proof source. Task-normalized structural PSR is 4.3% for the supplied VERINA reference proofs and 13.3–26.8% for the specialized provers (DeepSeek-Prover-V2-7B 13.3%, Goedel-Prover-V2-32B 26.0%, Goedel-Prover-V2-8B 26.8%).

• Specialized provers survive better overall than the references. On the 21–25 matched short, non-recursive tasks, overall unchanged-proof survival advantages are +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. Overall PSR is 59.3% (DeepSeek-7B), 64.5% (Goedel-32B), 64.6% (Goedel-8B), versus 47.9% for the reference proofs.

• The ordering is robust to analysis choices. It persists after excluding T1 variants (+24.3, +32.9, +31.3 points), under family-balanced aggregation (+13.7, +18.6, +17.3), under common task-family support (+17.4, +21.1, +18.8), and under four deployable valid-proof selection rules (first valid, shortest, random, all-valid average).

• But higher conditional survival does not mean better end-to-end utility. Coverage@5 is only 13.8–16.4% for the three specialized provers. The joint rate that a proof artifact is available and survives a uniformly sampled certified variant is 12.2% for the supplied references versus 9.3–10.4% for the provers.

• Class- and family-level results are fragile. The Goedel-32B semantic interval reaches zero, and the DeepSeek structural lower bound varies from 0.0 to 2.0 across bootstrap seeds. T3 and T5 have only 7–9 matched tasks. T4 (conditional inversion) is the clearest family-level case, with +50.0, +50.0, and +42.9 points for the three provers.

• Proof style predicts which refactorings are survived. Reference proofs open by unfold in 97.8% of cases and use simp[target] in 2.2%; the provers do the reverse (0.0–9.7% unfold, 77.4–84.6% simp[target]).

• Definitional bridges help structurally and hurt semantically. Under structural refactoring, rfl-bridge proofs survive in 6/6 tasks versus 6/31 for other strategies (Fisher p = 0.0004); on identical variants, 9/9 versus 2/9. Under semantic refactoring, rfl-bridge proofs survive 0/3 tasks versus 17/19 for simp[f]-style proofs (Fisher p = 0.0065); on identical variants, 0/4 versus 3/5. The authors describe these as descriptive associations, not causal tactic effects.

• Unchanged-proof failure is cheap to fix in many cases. Predefined one-identifier edits repair 109/139 eligible failures — 51/54 eligible reference structural failures and 58/85 eligible prover failures — with a median edit of two tokens on one line.

• T3 certification is strongly selected. Only 50/122 commutative-swap candidates certify (41.0%), and rejected candidates are 98.6% recursive versus 14.0% among certified ones, because the fixed certificate search does not synthesize the required induction.

• Valid proofs from the same model disagree materially. Different valid proofs disagree on at least one variant for 54%, 56%, and 71% of multi-proof tasks (DeepSeek-7B, Goedel-8B, Goedel-32B); mean within-task PSR ranges are 15.1–22.4 points, and within-task variance accounts for 29–54% of combined variance. The first-valid artifact differs from the within-task mean by only 4.7–8.6 points on average.

Methodology in Plain English

Each VERINA task is a Lean file with marker-delimited regions: imports, helpers, a precondition, the implementation body, a postcondition, and a proof. The authors wrote five deterministic text-rewrite "refactorings" that touch only the implementation region — wrap the body in a let, extract the body into a private helper function, swap the operands of a commutative operator, invert an if conditional, or extract just the else branch of a tail if. No model is involved in constructing candidates.

A candidate rewrite is kept only if Lean can separately prove that the original and refactored implementations agree pointwise on all inputs. That certificate lives in its own file and is never imported into the file where survival is tested, so the proof under evaluation cannot cheat by consulting it. Six invariants are enforced mechanically, including byte-identical specifications and proofs, no sorry/admit/new axioms, and an unchanged public function name and signature. The authors additionally ran #print axioms over all 458 certificate files and all 423 surviving proof files; none depends on sorryAx or any axiom beyond propext, Classical.choice, and Quot.sound, and 223 depend on no axioms.

For each surviving variant, they rebuild the task file with only the implementation regions changed and recompile in a pinned environment (Lean v4.18.0 with VERINA's Mathlib, 300-second timeout per file). The proof survival rate (PSR) for a task is the fraction of its certified variants on which the same unchanged proof still verifies; the headline number is the average of per-task PSRs over tasks with a valid proof, with 95% intervals from a task-cluster bootstrap over 10,000 replicates. Model-versus-reference comparisons are paired on the matched task set where both sources have a valid proof.

Model proofs come from five checkpoints — Qwen3-14B, Qwen3-32B, Goedel-Prover-V2-8B, Goedel-Prover-V2-32B, and DeepSeek-Prover-V2-7B — with K = 5 samples per task at temperature 1.0 and a 16,000-token output limit, using VERINA's prompting code. The first Lean-valid sample is the primary artifact. Total project cost was 35.3 GPU-hours including failed and exploratory runs.

Why This Matters

Impact on research. Verifiable-code benchmarks currently score a proof once, on one implementation. This paper shows that score is not a proxy for stability: specialized provers can beat the supplied reference proofs on unchanged-proof survival by 15–20 points while simultaneously losing on end-to-end availability-and-survival (9.3–10.4% versus 12.2%), because they solve the original task far less often. The measured PSR-versus-repair gap — 139 failures, 109 repaired by a two-token edit — argues that proof-stability metrics and proof-maintenance-cost metrics must be reported separately.

Real-world applications:

• Proof-maintenance tooling for large formal developments. Knowing that helper extraction (T2) is the dominant structural break, and that a single added identifier in an unfold/simp/dsimp call fixes most of those breaks, gives maintainers a concrete repair template.
• Evaluating and selecting code-generation models for verified software. Coverage@1/Coverage@5 and PSR together give a procurement-relevant picture that either metric alone would distort.
• CI for proof-carrying code. Refactoring-aware regression tests could flag proofs that will break at the next refactor rather than at the next commit.
• Compiler and language-design feedback. The finding that T2/T5 breakage depends on whether the extracted helper is a definitionally reducible private def suggests transparency settings and attributes such as @[irreducible] are levers on proof robustness.

Industry relevance. Any organization generating machine-checked proofs at scale — verified cryptography, smart contracts, safety-critical control code, verified compilers — faces proof maintenance as an ongoing cost. This paper quantifies how much of that cost is intrinsic to the proof artifact versus recoverable by trivial repair, and it shows that a model's original-task success rate and its proof stability are largely independent axes.

Future Directions

• Broaden beyond the matched slice. The primary comparisons rest on 21–25 basic-split, non-recursive, one-line-implementation tasks. Whether the source ordering holds for the 42.2% of the construction population that is recursive, or for longer implementations (median six lines in the construction population versus one line in the matched subset), is untested.

• Make T3 certification complete. Only 50/122 commutative swaps certify because the fixed certificate search cannot synthesize induction for recursive swaps. An induction-capable certificate search would let T3 results cover the recursive cases that currently get filtered out.

• Move from descriptive to causal claims about proof style. The mechanism categories were developed post hoc from observed artifacts and span only six structural and three semantic tasks; the within-prover prompt-time intervention did not produce a consistent causal effect. A properly controlled intervention on proof style is the obvious next experiment.

• Extend the transformation set and the repair model. The five families do not cover algorithm changes, data-representation changes, argument reordering, inlining, or @[irreducible] and set_option variations of unfolding behavior. The repair experiment covers only three predefined unfold/simp/dsimp edits and is explicitly not a re-proving experiment, so general maintenance cost after arbitrary refactorings remains unmeasured.

Target Audience

Researchers in AI for formal mathematics and verified code generation; maintainers of Lean/Mathlib developments and proof-engineering tooling; benchmark designers who need to know that one-shot verification scores conflate proof production with proof stability; and machine-learning engineers selecting or evaluating code models for settings where outputs must be machine-checked. Readers without Lean background can follow the framing and headline numbers but will need the tactics material to interpret the mechanism section.

Authors’ 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.