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

Aravind Mandiga; Guoming Li

cs.AIOct 26, 2026

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

Authors: Aravind Mandiga, Guoming Li

Organizations: University of Georgia, Athens, USA

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.

Figures & tables

Population / proof source	Tasks	Coverage@1 (%)	Coverage@5 (%)	Valid artifacts
VERINA source benchmark	189	–	–	–
RefactorProof construction	185	–	–	–
VERINA reference proofs	46	–	–	46 supplied
DeepSeek-Prover-V2-7B	31/189	12.7	16.4	111
Goedel-Prover-V2-32B	26/189	11.6	13.8	108
Goedel-Prover-V2-8B	29/189	9.5	15.3	100

Table 1: Task populations and original-proof coverage. Reference proofs are supplied upstream. Model Coverage@

k

is the fraction of all 189 tasks with a Lean-valid proof within the first

k

samples; “valid artifacts” counts all valid samples among

K=5

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 certificate is never imported into the survival file, and $\mathrm{PSR}_{\mathrm{task}}$ is averaged over tasks with a valid proof for that source. (b) VERINA task lastDigit . The supplied reference proof fails after T2 helper extraction with simp made no progress ; the two model lines shown are verbatim from the DeepSeek-Prover-V2-7B primary proof and survive via definitional equality.

Transformation	Class	Applicable tasks	Candidates	Certified	Cert. rate (%)	rfl (%)	Tasks w/ variant
T1_let_intro	D	181/185	181	180	99.4	100.0	180
T2_helper_extract	S	179/185	179	178	99.4	100.0	178
T3_comm_swap	E	77/185	122	50	41.0	4.0	34
T4_cond_invert	E	32/185	32	32	100.0	0.0	32
T5_branch_extract	S	18/185	18	18	100.0	100.0	18

Table 2: RefactorProof construction over the 185 VERINA tasks whose originals compile in the pinned environment. Certification rate is over generated candidates; “rfl” is the share of certified variants closed at a definitional level.

Panel A: Overall and transformation class
Proof source	C@1	C@5	Tasks	Overall PSR (%) [95% CI]	D	S	E
DeepSeek-Prover-V2-7B	12.7	16.4	31	59.3 [52.4, 66.4]	100.0	13.3	72.2
Goedel-Prover-V2-32B	11.6	13.8	26	64.5 [56.5, 72.8]	100.0	26.0	67.6
Goedel-Prover-V2-8B	9.5	15.3	29	64.6 [57.8, 72.1]	100.0	26.8	72.4
reference	–	–	46	47.9 [44.0, 52.0]	100.0	4.3	44.2

Table 3: Task-normalized PSR for the reference proofs and specialized provers. Coverage columns report Coverage@1 and Coverage@5 over all 189 attempted tasks; reference proofs are supplied rather than generated. T3 can contribute more than one variant per task, so each reported group is first averaged within task.

Model	Class	Matched tasks	Ref. PSR	Model PSR	$\Delta$ PSR	95% CI
deepseek-prover-v2-7b	all	25	43.6	59.2	+15.6	[8.0, 24.3]
deepseek-prover-v2-7b	structural	25	2.0	16.0	+14.0	[2.0, 30.0]
deepseek-prover-v2-7b	semantic	15	35.6	73.3	+37.8	[13.3, 62.2]
goedel-prover-v2-32b	all	21	43.5	62.4	+18.8	[10.1, 28.1]
goedel-prover-v2-32b	structural	21	2.4	26.2	+23.8	[4.8, 45.2]
goedel-prover-v2-32b	semantic	14	38.1	67.9	+29.8	[0.0, 58.3]

Table 4: Matched model versus supplied-reference comparison on identical certified variants. Values are paired PSR differences with task-cluster bootstrap 95% CIs. Overall sensitivity checks remain positive: excluding T1 gives +24.3, +32.9, and +31.3 points for DeepSeek-7B, Goedel-8B, and Goedel-32B; family-balanced aggregation gives +13.7, +18.6, and +17.3 points. PSR columns are rounded independently;

\Delta

PSR is computed from the unrounded task-level values. Appendix A reports full sensitivity results.

Proof source	$n$	unfold target (%)	simp[target] (%)	med. LoC	med. tactics
deepseek-prover-v2-7b	31	9.7	77.4	25	23
goedel-prover-v2-32b	26	0.0	84.6	36	33
goedel-prover-v2-8b	29	0.0	79.3	32	30
reference	46	97.8	2.2	11	12

Table 5: Tactic profile of the fixed reference and specialized-prover proof artifacts.

Setting	Comparison level	Group A	Group B	Evidence
Structural	task	rfl bridge: 6/6	other: 6/31	Fisher $p=0.0004$
Structural	same variant	rfl bridge: 9/9	other: 2/9	6 variants, 5 tasks
Semantic	task	rfl bridge: 0/3	simp[f]: 17/19	Fisher $p=0.0065$
Semantic	same variant	rfl bridge: 0/4	simp[f]: 3/5	3 variants

Table 6: Mechanism checks that reduce dependence among repeated records. Task-level rows count tasks with at least one survival in the indicated category. Same-variant rows compare proof categories on the same refactored variants.

Appendix figures & tables8 assets

Supplementary material from the paper’s appendix.

Appendix

Model	First valid	Shortest valid	Random valid	All valid
DeepSeek-Prover-V2-7B	+15.6	+11.3	+15.6	+15.5
Goedel-Prover-V2-8B	+20.3	+22.4	+20.7	+20.7
Goedel-Prover-V2-32B	+18.8	+24.5	+20.9	+20.9

Appendix

Table 7: Overall matched

\Delta

PSR (percentage points) under valid-proof selection rules. “All valid” averages each task across all valid samples.

Model	Tasks ( $\geq 2$ valid)	Identical (%)	PSR range	$S$ range	$E$ range	Within-var. share (%)	$\|$ first–mean $\|$
DeepSeek-7B	26	46	17.4	48.0	35.3	41	6.7
Goedel-8B	25	44	15.1	36.0	45.4	29	4.7
Goedel-32B	24	29	22.4	54.2	55.9	54	8.6

Appendix

Table 8: Within-task variability across independently sampled Lean-valid proofs. “Identical” is the share of tasks on which all valid samples have the same survive/fail vector over certified variants. Ranges are mean within-task max–min PSR differences in percentage points;

S

and

E

restrict to structural and semantic variants.

Proof source	Rate (%)	95% CI
VERINA supplied reference	12.2	[9.0, 15.5]
DeepSeek-Prover-V2-7B	10.2	[6.8, 13.8]
Goedel-Prover-V2-8B	10.4	[6.9, 14.2]
Goedel-Prover-V2-32B	9.3	[5.9, 13.0]

Appendix

Table 9: Artifact-availability-and-survival rate over the 180 tasks with at least one certified variant.

Analysis	DeepSeek-7B	Goedel-8B	Goedel-32B
Exclude T1	+24.3 [11.5, 38.9]	+32.9 [18.4, 48.6]	+31.3 [15.7, 48.7]
Family-balanced within task	+13.7 [6.8, 21.5]	+18.6 [10.9, 26.6]	+17.3 [9.2, 26.2]
Exclude T1 and T2	+28.7 [13.3, 46.0]	+30.7 [4.0, 54.7]	+20.7 [-4.3, 45.7]
Common task-family support	+17.4 [8.3, 26.8]	+21.1 [12.3, 30.2]	+18.8 [9.9, 27.8]

Appendix

Table 10: Matched

\Delta

PSR sensitivity to aggregation and common support. Values are percentage points with 95% task-cluster bootstrap intervals. The final row uses the 65 task-family cells shared by all four sources (21 tasks).

Model	Class	Tasks	Model higher	Reference higher	Tie	$\Delta$ PSR
DeepSeek-7B	all	25	10	0	15	+15.6
DeepSeek-7B	structural	25	5	1	19	+14.0
DeepSeek-7B	semantic	15	6	0	9	+37.8
Goedel-8B	all	23	12	0	11	+20.3
Goedel-8B	structural	23	6	1	16	+21.7
Goedel-8B	semantic	15	8	1	6	+42.8

Appendix

Table 11: Taskwise direction of matched PSR differences. “Model higher” and “Reference higher” compare the per-task PSR of the two proof artifacts; the remaining tasks tie.

Population	Tasks	Basic (%)	Recursive (%)	Med. impl. LoC	Med. postcond. LoC	T3 (%)	T4 (%)	T5 (%)
Construction population	185	58	42.2	6	3	18	17	10
Supplied-reference subset	46	100	6.5	1	2	24	26	24
Matched, DeepSeek-7B	25	100	0.0	1	1	36	32	32
Matched, Goedel-8B	23	100	0.0	1	1	39	35	35
Matched, Goedel-32B	21	100	0.0	1	1	43	33	33

Appendix

Table 12: Characteristics of the task populations entering the matched comparisons. T3–T5 columns give the share of tasks with at least one certified variant of that family. T1 and T2 are available for every matched task.

Model	Family	Matched tasks	$\Delta$ PSR	95% CI
DeepSeek-Prover-V2-7B	T2	25	+12.0	[0.0, 24.0]
Goedel-Prover-V2-8B	T2	23	+21.7	[4.3, 39.1]
Goedel-Prover-V2-32B	T2	21	+23.8	[9.5, 42.9]
DeepSeek-Prover-V2-7B	T3	9	+33.3	[0.0, 66.7]
Goedel-Prover-V2-8B	T3	9	+40.7	[-3.7, 81.5]
Goedel-Prover-V2-32B	T3	9	+25.9	[-14.8, 66.7]

Appendix

Table 13: Matched model-minus-reference

\Delta

PSR by transformation family. Task counts differ because a family must be present on a task for both sources. T1 is omitted because both sources survive it universally.

Source / template	Repaired	Attempted
Reference	51	54
DeepSeek-Prover-V2-7B	21	32
Goedel-Prover-V2-8B	19	28
Goedel-Prover-V2-32B	18	25
dsimp add helper	40	45
simp add helper	16	37

Appendix

Table 14: Predefined one-identifier repair of eligible structural failures. The unedited control reproduces all 139 attempted failures.

Code Generation Evaluation

Code generation evaluation measures whether AI-produced programs are correct, reliable, secure, efficient, and faithful to their specifications.

See all 215 papers

Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts
Jun 2, 2026Yiming Fu, Peixuan Liu, Zichen Wang +1Interactive Theorem Proving Lean Theorem Proving
Department of Mathematics Southern University of Science and Technology · School of Mathematical Sciences Peking University · Center for Machine Learning Research Peking University
Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search
May 18, 2026Jialin Lu, Soonho Kong, Rodrigo Stehling +4Large Language Model-Guided Optimization Lean Theorem Proving
Simon Fraser University · Amazon Web Services · MiroMind +1
P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation
Aug 10, 2026Zenan Li, Ziran Yang, Peiyang Song +2Code Generation Formal Verification
1Apodex · 2Princeton University · 3Caltech +1

Jun 2, 2026J/K move · Enter open · S save

Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

Yiming Fu, Peixuan Liu, Zichen Wang, Kun yuan

Department of Mathematics Southern University of Science and Technology · School of Mathematical Sciences Peking University · Center for Machine Learning Research Peking University

Interactive Theorem Proving Lean Theorem Proving

Open paper AskPDF arXiv

While Large Language Models (LLMs) have shown strong performance in generating formal proofs, their outputs often remain less readable, modular, maintainable, and reusable than proofs in mature formal mathematics libraries. We argue that this gap stems in part from the compile-first objective implicit in most proof-generation pipelines, which encourages monolithic or ad hoc proof scripts rather than library-quality artifacts. Existing approaches to proof-quality improvement often rely on explicit, computable optimization objectives. In practice, however, the most tractable and experimentally validated objectives are largely length-based, while higher-level qualities such as readability, modularity, maintainability, and reusability are difficult to reduce to reliable automatic metrics. Instead of optimizing proof improvement against a single proxy metric, we take a process-guided approach inspired by human proof-refactoring workflows. We propose an agentic framework

\textbf{Proof-Refactor}

that decomposes proof refactoring into four phases: extracting candidate proof fragments, designing helper declarations, formally proving the extracted and designed components, and repairing the original proof using the verified components. On generated Lean proofs from PutnamBench and Putnam2025, Proof-Refactor improves rubric-based refactoring scores over a strong Claude Code refactoring baseline, with the largest gains in signature quality and human readability. These results suggest that process-guided refactoring can improve proof structure without treating proof length as the primary objective.

Abstract

Code Generation Evaluation

Explore similar work

Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts

Lean Refactor: Multi-Objective Controllable Proof Optimization via Agentic Strategy Search

P3^{3}3: Joint Program-and-Proof Planning for Verified Code Generation

P $^{3}$ : Joint Program-and-Proof Planning for Verified Code Generation