PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Aravind Mandiga, Guoming Li

arXiv:2610.36328v1cs.AIcs.LOcs.SE

TL;DR

Benchmarks for verifiable code generation usually test proofs against one fixed implementation, leaving their stability under behavior-preserving refactoring unmeasured. RefactorProof creates Lean-certified variants while keeping specifications and evaluated proofs fixed. On matched tasks, specialized prover proofs have higher overall unchanged-proof survival than supplied reference artifacts, while many eligible structural failures can be repaired with a one-identifier edit.

  • Problem

    Verifiable-code benchmarks usually test whether a proof verifies against one fixed implementation, not whether it survives a behavior-preserving refactoring.

    Source: §1 · p. 1

  • Method

    RefactorProof constructs Lean-certified, behavior-preserving implementation variants and rechecks the unchanged proof against the unchanged specification.

    Source: §1 · pp. 1–2

  • Results

    On matched tasks, specialized provers’ overall PSR exceeds supplied-reference PSR by +15.6 to +20.3 percentage points, with all three 95% bootstrap intervals excluding zero.

    Source: §4.2 · p. 6, §6 · p. 9

  • Takeaways & Limitations

    Predefined one-identifier edits repair 51/54 eligible reference-proof failures and 58/85 eligible prover failures, so unchanged-proof failure need not mean high repair cost.

    Source: §4.4 · p. 8

    The reference arm covers 46 basic-split tasks, while primary matched comparisons narrow to 21–25 short, non-recursive tasks and do not establish checkpoint-wide robustness.

    Source: §5 · p. 8

Abstract

from arXiv · show

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.

1 Introduction

RefactorProof tests whether unchanged proofs survive behavior-preserving implementation refactorings, extending one-time verification benchmarks to proof stability. Its certified variants and matched comparisons examine proof artifacts within a limited VERINA reference subset.

1 Introduction

  • RefactorProof certifies that each refactored implementation is equivalent to the original, then rechecks the unchanged proof against the same specification; PSR measures survival across certified refactorings.The equivalence certificate is checked in a separate file.Source: §1 · p. 1
  • Five deterministic transformation families are grouped into definitional, structural, and theorem-certified semantic classes according to their source-level changes.T2 and T5 are structural even though Lean can reduce the transformed implementation to the original behavior definitionally.Source: §1 · pp. 1–2
  • The benchmark constructs 458 certified variants while keeping the specification and evaluated proof fixed, enabling matched proof-survival comparisons and analyses of proof strategies and repair.The reference proofs cover 46 basic-split tasks; primary model-versus-reference comparisons match on 21–25 short, non-recursive tasks.Source: §1 · p. 2
  • VERINA supplies reference proofs for only 46 basic-split tasks, and primary model-versus-reference comparisons cover 21–25 short, non-recursive tasks.The authors frame these as comparisons of proof artifacts on this subset, not checkpoint-wide robustness rankings over VERINA.Source: §1 · p. 2

2 Related work

Related work evaluates verified code on original implementations, proof generation and repair, or semantics-preserving perturbations. RefactorProof instead changes the implementation while holding the proof and specification fixed.

2 Related work

  • VERINA [Ye et al., 2026] and other verifiable-code benchmarks assess verification on the original task or implementation; RefactorProof rechecks the proof after implementation refactoring.The cited alternatives include CLEVER [Thakur et al., 2025], miniCodeProps [Lohn and Welleck, 2024], and FVAPPS [Dougherty and Mehta, 2025].Source: §2 · p. 2
  • Proof-maintenance and repair systems generate, search, or repair proofs, whereas RefactorProof freezes the proof and changes only the implementation to measure survival before repair.Examples include PUMPKIN PATCH, PUMPKIN Pi [Ringer et al., 2021], and Baldur [First et al., 2023].Source: §2 · p. 2
  • ReCode [Wang et al., 2023] and Mariposa study semantics-preserving perturbations, but RefactorProof changes the implementation while fixing the proof and specification.Each retained program change also receives a separate Lean equivalence certificate.Source: §2 · p. 2

3 Method

RefactorProof changes only implementations, preserving specifications and evaluated proofs byte-for-byte while separately certifying behavior equivalence. It measures whether unchanged proofs survive deterministic refactorings across a pinned Lean environment and defined proof-source populations.

3.1 Setting and invariants

  • RefactorProof keeps task specifications and evaluated proofs byte-identical, certifies each retained implementation change separately, and checks the unchanged proof against the refactored program.The separate equivalence certificate is not imported into the survival file; the pipeline also checks hashes, unchanged public signatures, and absence of sorry, admit, or new axioms.Source: §3.1 · pp. 2–3

3.2 Transformation classes

  • Five deterministic transformations test definitional, structural, and theorem-certified semantic source changes without inspecting specifications or proof artifacts.T1 introduces a let; T2 extracts a helper; T3 swaps commutative operands; T4 inverts a conditional; and T5 extracts one branch of a conditional.Source: §3.2 · p. 3

3.3 Certification

  • Each variant is retained when any tactic in a fixed Lean certificate search proves pointwise equivalence between the original and transformed implementations.The search tries definitional tactics first, then simplification and family-specific tactics; wrapped bodies that Lean’s code generator refuses are retried as noncomputable definitions.Source: §3.3 · p. 3

3.4 Survival evaluation and metrics

  • Survival evaluation rebuilds each task with only its implementation changed, then compiles the unchanged proof in the pinned VERINA environment.PSR is averaged within task and then across tasks with a valid proof; matched sources are compared on the same variants, with task-cluster bootstrap intervals.Source: §3.4 · pp. 3–4

3.5 Evaluation populations and reference-proof availability

  • The benchmark is built from 185 VERINA task files that compile in the pinned environment, while supplied reference proofs cover only 46 basic-split tasks.The reference tasks are simpler than the other 139 construction tasks: their median implementation is one line and 6.5% are recursive, versus eight lines and 54.0% recursive for the others.Source: §3.5 · p. 4

3.6 LLM proofs

  • Models generate five ordered samples per task on original implementations; the first Lean-valid sample is the primary proof artifact.Sensitivity analyses also evaluate shortest, fixed-seed random, and all valid proofs, and recompute PSR excluding T1 and with alternative task-family weighting and common support.Source: §3.6 · p. 5

4 Results

On matched tasks, specialized-prover proofs have higher overall unchanged-proof survival than supplied references, though survival depends on the refactoring mechanism. Many eligible structural failures are repaired by predefined one-identifier edits.

4.1 RefactorProof construction

  • Only 50/122 T3 candidates certify, and 98.6% of rejected cases are recursive versus 14.0% of certified candidates.The fixed certificate search does not synthesize induction often needed for recursive swaps, so T3 results cover a selected, mostly non-recursive subset.Source: §4.1 · p. 6, Table 2 · p. 6

4.2 Proof stability by source

  • On matched tasks, specialized provers exceed supplied references in overall PSR by +15.6 to +20.3 points, with all three 95% CIs excluding zero.The overall ordering persists under sensitivity checks; family-specific comparisons remain exploratory.Source: §4.2 · pp. 6–7, Table 4 · p. 7

4.3 Why proof strategies respond differently to refactoring

  • Under structural helper extraction, bridge proofs survive in 6/6 tasks versus 6/31 for other strategies, and 9/9 versus 2/9 on the same variants.Reference proofs usually begin with unfold, while specialized provers more often use simp or dsimp with automation; the stylistic difference is not itself causal.Source: §4.3 · p. 7, Table 6 · p. 8
  • Under semantic refactoring, rfl-bridge proofs survive 0/3 tasks versus 17/19 for simp [f]-style proofs; the mechanism findings are descriptive associations.Semantic changes alter the literal body, which can break an rfl equation tied to the original body.Source: §4.3 · p. 8

4.4 Mechanical repair of structural failures

  • Predefined one-identifier edits repair 109/139 eligible failures, including 51/54 reference failures and 58/85 prover failures.The median edit is two tokens on one line; unchanged-proof failure therefore does not imply high repair cost under this narrow template.Source: §4.4 · p. 8

5 Limitations

The findings are bounded by the benchmark slice, certification and proof-selection procedures, and a narrow set of transformations and repair edits. Several analyses are exploratory, and the source comparisons do not establish causal effects.

5 Limitations

  • Several analyses were specified after survival outcomes were known, including mechanism categories, alternative weightings, and selection-rule sensitivity analyses.The three repair templates were fixed before repair outcomes were evaluated.Source: §5 · p. 8
  • T3 results apply to certified, mostly non-recursive swaps because the automatic sequence does not synthesize induction for many recursive swaps.Only 14.0% of certified candidates are recursive, compared with 98.6% of rejected candidates.Source: §5 · p. 8
  • The reference arm covers 46 basic-split tasks, while matched comparisons narrow to 21–25 short, non-recursive tasks; results do not characterize checkpoint-wide robustness over VERINA.Model PSR is conditional on solving the original task, with Coverage@5 of 13.8–16.4% for the three specialized provers.Source: §5 · p. 8
  • Because VERINA predates the evaluated checkpoints, pretraining exposure cannot be ruled out and could inflate original-task coverage.Its effect on survival is less direct because the refactored implementations and certificates were generated for this work and were not previously public.Source: §5 · p. 9
  • The between-source tactic profile is descriptive, not causal; templates, decoding defaults, and 32B quantization differ across sources.Class- and family-specific comparisons are exploratory and not multiplicity-corrected; mechanism categories were developed post hoc from observed artifacts.Source: §5 · p. 9
  • RefactorProof covers five local mechanical transformation families in one pinned Lean/Mathlib environment, not the full range of software refactorings; repair tests only three predefined edits on eligible failures.The T2 and T5 results also depend on Lean transparency settings; the helper remains definitionally reducible, and this setting was not varied.Source: §5 · p. 9

6 Conclusion

RefactorProof evaluates whether an already valid Lean proof survives a certified, behavior-preserving implementation change. Specialized provers show higher overall unchanged-proof survival on the matched tasks, but PSR measures artifact stability rather than maintenance cost.

6 Conclusion

  • On short, non-recursive matched VERINA tasks, the three specialized provers have higher overall unchanged-proof survival than supplied reference proofs.Family-specific evidence is strongest for conditional inversion and helper extraction.Source: §6 · p. 9
  • Inspected proof artifacts remain coupled to implementation details through syntax-specific rewrites, definitional-equality bridges, and normalization, which fail under different changes.Source: §6 · p. 9
  • Many eligible structural failures are repaired by a one-identifier edit, so PSR measures proof-artifact stability rather than the cost of maintaining a proof after it breaks.One-time verification does not establish that the same proof remains reusable unchanged after refactoring.Source: §6 · p. 9

A Additional sensitivity analyses

The appendix uses existing generation outputs and Lean re-checks to test the main comparisons and their scope.

A Additional sensitivity analyses

A.1 Valid-proof selection

The overall matched comparison remains positive across deployable valid-proof selection rules, while a post hoc least-robust-valid bound shows that structural differences can depend on proof choice.

A.1 Valid-proof selection

  • Every deployable valid-proof selection rule yields an overall matched 95% task-cluster bootstrap interval excluding zero.The first-valid re-evaluation reproduces 301/301 frozen primary survival outcomes after all 334 Lean-valid samples are re-checked on every certified variant.Source: §A.1 · p. 12, Table 7 · p. 12
  • Under the post hoc least-robust-valid bound, structural ∆PSR is +6.5 [-4.3, 19.6] for Goedel-8B, +2.4 [-7.1, 14.3] for Goedel-32B, and -2.0 [-6.0, 0.0] for DeepSeek-7B.This bound is not treated as a deployable selection rule.Source: §A.1 · p. 12
  • The least-robust-valid bound indicates that structural robustness can depend on which valid proof a model emits.Source: §A.1 · p. 12

A.2 Within-task variability across valid proofs

Valid proofs from the same model–task pair can behave differently under refactoring, so survival depends materially on the proof artifact selected. The first-valid proof is close to the within-task mean, and tested deployable selection rules preserve the direction of the overall matched differences.

A.2 Within-task variability across valid proofs

  • Table 8 summarizes identical survival vectors and mean within-task max–min PSR ranges across valid proofs, with separate structural and semantic ranges.The analysis focuses on the three specialized provers because Qwen controls have only two tasks each with multiple valid proofs.Source: Table 8 · p. 12, §A.2 · p. 12
  • 54%, 56%, and 71% of multi-proof tasks show disagreement among valid proofs for DeepSeek-7B, Goedel-8B, and Goedel-32B, respectively.Disagreement means at least one certified variant has a different survival outcome across valid proofs.Source: §A.2 · p. 12
  • Mean within-task PSR ranges are 15.1–22.4 points, with within-task variance accounting for 29–54% of combined within- and between-task variance.Structural survival is especially sample-dependent, with mean within-task ranges of 36–54 points.Source: §A.2 · p. 12
  • The first-valid artifact differs from the within-task mean by 4.7–8.6 points on average, and every tested deployable selection rule preserves all three overall matched-difference directions.The analysis re-checks every Lean-valid sample on every certified variant; proof choice contributes variation but does not reverse the primary ordering under tested rules.Source: §A.2 · p. 12

A.3 Aggregation and common support

The analysis tests whether matched model–reference comparisons depend on aggregation, common support, or universally survived variants. The reference source remains lowest under tested weightings, while the positive point estimates persist on the T1-and-T2-excluded remainder, with weaker uncertainty for some models.

A.3 Aggregation and common support

  • The end-to-end rate combines proof-artifact availability with survival on a uniformly sampled certified variant, with Table 9 reporting estimates and uncertainty.Availability means a supplied VERINA proof for the reference source and a model-produced Lean-valid proof for a model.Source: §A.3 · p. 13, Table 9 · p. 13
  • Excluding T1, source-level PSR is 11.5% for reference proofs, 32.0% for DeepSeek-7B, 43.8% for Goedel-8B, and 43.7% for Goedel-32B.Family-balanced and one-per-task-family weighting move any source’s PSR by at most 3.8 points, and reference proofs remain lowest under every tested weighting.Source: §A.3 · p. 13
  • Table 10 reports matched model-minus-reference ∆PSR values under alternative aggregation and common-support choices, including 65 shared task-family cells across 21 tasks.T1 and T2 contribute 358/458 certified variants, motivating the sensitivity analyses.Source: Table 10 · p. 13, §A.3 · p. 13
  • On the T1-and-T2-excluded remainder of 14–15 matched tasks, point estimates remain positive for all three sources, but the Goedel-32B interval crosses zero.Sign-flip p-values are 0.017, 0.066, and 0.216 for DeepSeek-7B, Goedel-8B, and Goedel-32B, respectively.Source: §A.3 · p. 13
  • No task favors the reference proof in overall matched comparisons, while reference proofs lead on at most one task in class-specific comparisons.Table 11 counts taskwise directions of matched PSR differences; remaining tasks tie.Source: §A.3 · p. 13, Table 11 · p. 13

A.4 Matched-subset characterization

The matched comparisons cover a particularly simple subset of VERINA, and analyses across transformation families and proof strategies qualify how broadly their results apply. Mechanism findings are descriptive, and predefined helper-name edits repair many eligible structural failures without measuring general repair cost.

A.4 Matched-subset characterization

  • The matched subsets are all basic-split, non-recursive tasks with median one-line implementations and postconditions, unlike a construction population that is 42.2% recursive with six-line median implementations.Matched tasks have higher T3–T5 availability; the source ordering therefore does not establish the same result for recursive or longer tasks.Source: §A.4 · p. 14

A.5 Matched effects by transformation family

  • Table 13 reports matched model-minus-reference ∆PSR by transformation family and omits T1 because both sources survive it universally.Family task counts differ because a family must be present on a task for both sources.Source: Table 13 · p. 14

A.6 Mechanism sensitivity

  • For structural refactorings, rfl-bridge proofs survive in 6/6 tasks versus 6/31 for other strategies; for semantic refactorings, rfl survives in 0/3 versus 17/19 for simp.Record-level contrasts are +89.8 points for structural rfl versus other and −83.6 points for semantic rfl versus simp; small group sizes make these descriptive, not population-level tactic effects.Source: §A.6 · p. 14
  • Among prover structural records, all 12 explicit rfl bridges survive versus 10/98 without one, while semantic simp [f]-style bridges survive 56/67 and explicit rfl-equation bridges 0/4.Syntax-specific T3 failures include rewrite-pattern mismatches and residual commuted goals; prompt intervention did not isolate a common causal tactic effect.Source: §A.6 · pp. 14–15

A.7 Mechanical repair

  • The predefined edit repairs 109/139 eligible failures, or 76.8% of all 142 structural failures, with a median two-token, one-line change.The rate is conditional on template eligibility and does not measure general proof repair or re-proving.Source: §A.7 · p. 15, Table 14 · p. 15

A.8 Other sensitivity checks

  • T3 certification selects against recursive candidates: 14.0% of certified candidates are recursive versus 98.6% of rejected candidates.Across 50 bootstrap seeds, two class-specific lower bounds vary across zero; the other seven matched rows exclude zero under every tested seed.Source: §A.8 · p. 15
  • Adding log proof length changes the prover coefficient from 1.404 to 1.370 (p = 0.0013), while proof length itself is not associated with survival (coefficient 0.030, p = 0.88).This remains observational because prompt templates, decoding settings, and FP8 quantization also differ by source.Source: §A.8 · p. 15
Loading 2610.36328v1…