Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving

Jack Li; Sophia Li

cs.AIOct 15, 2026

Repair, Retry, and the Cost of Hindsight: Verifier Feedback in Formal Theorem Proving

Authors: Jack Li, Sophia Li

Organizations: Department of Computer Science, Stanford University

Abstract

Verifier-guided self-repair conditions a model on feedback from failed attempts before it tries again, without weight updates. Yet two findings in prior work are in tension: verifier feedback can improve repair of failures, but self-repair itself can provide little-to-no advantage over independent resampling. We reconcile these findings in Lean theorem proving through controlled one-step experiments that hold the preceding failure fixed while varying whether the failed proof is shown, whether the compiler error corresponds to that failure, and the retry instruction. We test frozen Qwen3.6-27B, a general-purpose model, and DeepSeek-Prover-V2-7B, a specialized prover, on difficult MiniF2F problems. We find two opposing effects. Showing the model its failed predecessor reduces success and sharply increases copying of it, while on Qwen adding that attempt's compiler error recovers the loss, to the level of the diagnostic alone. Replacing the predecessor with another theorem's failed proof largely removes the degradation on both models; on Qwen, replacing the diagnostic with another problem's error substantially reduces the recovery. Without the failed proof, correct diagnostics show no resolved advantage over wrong-diagnostic controls on either model. The failed-proof penalty persists with and without the retry instruction, whereas Qwen's diagnostic recovery is weaker without it. In 11-problem sequential experiments through 64 attempts, Qwen retains a correct-diagnostic benefit within failed-proof histories, while DeepSeek-Prover shows no resolved recovery. However, no tested one-step feedback condition establishes an advantage over instruction-only resampling, nor does 64-attempt sequential repair with failed proofs and correct diagnostics at equal token budgets. Verifier feedback can thus improve repair without overcoming the performance loss from conditioning on a failed attempt.

Figures & tables

Study	Repair context	Feedback control	Additional separation
Verma (2026)	Failed code under matched-budget retries	Placebo feedback; successful cross-task examples in a separate experiment	Failed-code exposure versus omission; cross-task examples supplement rather than replace the failed code
Iscan (2026a)	Failed code in one repair step	Generic fact bullets matched to the executed-feedback format	Blind resampling with matched generation count
This work	Fixed failed Lean proof and evolving histories	Cross-problem diagnostics, ordinary or class/length matched	Own-proof omission or replacement and retry-instruction crossings

Table 1: Operational comparison of controls in closely related test-time repair studies. “Matched” refers to each study’s stated control variables, not exact token identity across studies.

Condition	Instruction	Failure notice	Failed proof	Added feedback
Bare	–	–	–	–
$I$	Yes	–	–	–
$F$	Yes	Yes	–	–
$F_{C}$	Yes	Yes	Yes	–
$F_{E}$	Yes	Yes	–	Diagnostic
$F_{CE}$	Yes	Yes	Yes	Diagnostic

Table 2: Central one-step prompt components. Every condition includes the theorem-completion task.

Figure 1: Controlled one-step pass@4. Dashed lines mark instruction-only performance. $s$ : shuffled wrong diagnostic; $m$ : class/length-matched wrong diagnostic; $o$ : another theorem’s failed proof. Whiskers are marginal 95% problem-bootstrap intervals; paired contrast intervals are reported in text.

Figure 2: Sequential repair and diagnostic-content effects on both models. Qwen (top) and DeepSeek-Prover (bottom) each use their own 11-problem bank. Left: success by attempt $k$ for memoryless instruction-only resampling ( $I$ ), failed-proof history alone ( $C$ ), failed-proof histories with correct ( $CE$ ), ordinary-shuffled ( $CE_{s}$ ), or matched-wrong ( $CE_{m}$ ) diagnostics, and code-free diagnostic histories ( $E,E_{m}$ ). Adaptive curves are fractions of 110 trajectories solved; $I$ is mean pooled pass@ $k$ from 640 draws per problem. Right: matched corresponding-minus-wrong diagnostic effects with failed proofs ( $CE-CE_{m}$ , orange) and without them ( $E-E_{m}$ , green). Their difference defines the registered matched interaction reported in the text and Appendix D.5 . Shading shows pointwise 95% problem-bootstrap intervals: marginal for left-panel curves and paired for right-panel contrasts.

Appendix figures & tables25 assets

Supplementary material from the paper’s appendix.

Appendix

Model	Contrast	$\Delta$ (pp)	95% CI	Status	Adjustment
Repair does not beat retrying
Qwen	$F_{CE}-I$	$-3.0$	$[-8.4,+2.4]$	Expl.	—
DS	$F_{CE}-I$	$-16.1$	$[-22.6,-10.2]$	Expl.	Holm, BH
Qwen	$CE-I$	$-18.3$	$[-41.8,+5.3]$	Prim.	—
DS	$CE-I$	$-50.7$	$[-66.4,-34.5]$	Prim.	Holm, BH
Own failed proof harms

Appendix

Table 3: Main-text claims, the contrasts that carry them, and their status. Intervals are the paper’s 95% paired problem-bootstrap intervals. Status: Prim. = registered primary endpoint; Reg. = registered secondary or family member; Expl. = exploratory. The last column gives the adjustments a contrast survives, applying Holm and Benjamini–Hochberg (BH) within model as described above (one-step: bootstrap

p

over each model’s 15 comparisons; sequential: exact randomization

p

over each model’s table); “—” marks contrasts for which no difference is claimed; primary endpoints are shown as if adjusted, although they need no adjustment. Qwen’s preregistered

F_{C}-F

has Holm-adjusted

p=0.055

; DeepSeek-Prover’s

E-E_{m}

and matched interaction have exact

p=0.063

and

0.109

before adjustment. DS = DeepSeek-Prover.

Figure 3: One-step pass@4 for the central arms, and prompt anatomy. Dashed lines mark instruction-only performance; hatching denotes shuffled wrong diagnostics, and the bracket gives the $F_{CE}-F_{C}$ difference in problems solved. Whiskers are marginal 95% problem-bootstrap intervals, not paired contrasts. The predecessor-replacement and matched-diagnostic controls are summarized in Fig. 1 and Table 9 ; detailed copying and diversity appear in Fig. 5 .

arm	prompt	pass@4 count	passes	vs. $I$ (sign, $p$ )
bare	task only	15	18	9/42, $3.4\times 10^{-6}$
$I^{\dagger}$	instruction line + task	45	110	—
N †	random words + instruction	49	105	19/23, 0.64
N2–N5 †	four more random-word sentences	48/43/42/44	130/87/117/116	0.16/0.20/1/0.50
$F$	failure sentence + instruction	33	81	11/26, 0.020
S †	“did fully verify” variant	30	77	8/27, 0.0019

Appendix

Table 4: Qwen3.6-27B, all one-step arms (167 problems; 4 samples per problem). “Problems passed” = problems with

\geq 1

passing sample (pass@4 count); “passes” = passing samples of 668. † post-hoc.

scaffold	without line	with line	line’s worth (sign, $p$ )	without, vs. bare
nothing	15 (bare)	45 ( $I$ )	$+30$ (42/9, $3.4\times 10^{-6}$ )	—
random words	30	49	$+19$ (33/12, 0.002)	$+15$ (26/8, 0.003)
failure sentence	46 (repl. 45)	33	$-13$ (14/29, 0.03)	$+31$ (42/7, $4\times 10^{-7}$ )
+ compiler error	32	41	$+9$ (22/11, 0.08; McNemar 0.049)	$+17$ (28/8, 0.001)
+ wrong error	29	39	$+10$ (25/13, 0.07)	$+14$ (28/11, 0.009)
+ reflection	41	42	$+1$ (18/18, 1)	$+26$ (39/10, $4\times 10^{-5}$ )

Appendix

Table 5: Qwen3.6-27B, the no-instruction ladder (167 problems). Each scaffold with and without the instruction line; prompts differ only by the removed line, on frozen banks and seeds.

scaffold	with line	without line
nothing	29 (65; bare) $\cdot$ 34 (85; $I$ )	—
random words	32 (83)	—
failure sentence	35 (92)	32 (88)
+ compiler error	30 (79)	32 (81)
+ another problem’s error	32 (83)	32 (86)
+ failed code	14 (25)	8 (12)

Appendix

Table 6: DeepSeek-Prover-V2-7B, all arms (137 problems, its own frozen failures; four samples per problem). Entries are problems with a passing sample (pass@4 count), with passing samples out of 548 in parentheses.

Figure 4: Instruction ablations. Outlined/filled bars omit/include the instruction line; $F$ without that line is the failure notice alone. Bars show pass@4 counts with marginal problem-bootstrap intervals.

Contrast	Counts	Wins/losses	Raw $p$	Holm $p$
$F$ vs. bare	33/15	32/9	0.000215	0.00108
$F_{E}$ vs. $F$	41/33	25/19	0.226	0.462
$F_{E}$ vs. bare	41/15	37/9	0.0000203	0.000122
$F_{R}$ vs. $F$	42/33	25/15	0.154	0.462
$F_{C}$ vs. $F$	18/33	11/27	0.0139	0.0554
$F_{CE}$ vs. $F_{E}$	40/41	25/22	0.771	0.771

Appendix

Table 7: Preregistered Qwen comparison family. Counts are problems with a pass among four; wins/losses compare per-problem numbers of passing samples. The first three tests are one-sided and the last three two-sided; Holm adjustment covers all six.

Model	Contrast	All problems	Parseable problems
Qwen	$F_{CE}-I$	$-3.0$ $[-8.4,+2.4]$	$-3.6$ $[-10.2,+2.9]$
	$F_{C}-F$	$-9.0$ $[-15.6,-2.4]$	$-10.9$ $[-19.0,-2.9]$
	$F_{CE}-F_{C}$	$+13.2$ $[+7.2,+19.8]$	$+16.1$ $[+8.8,+23.4]$
	$F_{CE}-F_{CE_{m}}$	$+7.8$ $[+1.8,+13.8]$	$+9.5$ $[+2.2,+16.8]$
	$F_{E}-F_{E_{m}}$	$-3.6$ $[-9.0,+1.8]$	$-4.4$ $[-10.9,+2.2]$
	$F_{C_{o}}-F_{C}$	$+14.4$ $[+7.8,+21.6]$	$+17.5$ $[+9.5,+25.5]$

Appendix

Table 8: One-step contrasts (pass@4, pp) on all problems and on the problems whose statements parse. Both columns use the same paired problem bootstrap (10,000 resamples), so an all-problem interval can differ by one resampling step from the main-text value for the same contrast.

	Qwen (167)		DeepSeek-Prover (137)
arm	problems	passes	problems	passes
$F_{C_{o}}$	42	93	33	88
$F_{E_{m}}$	47	90	32	87
$F_{CE_{m}}$	27	66	12	26

Appendix

Table 9: Replacement and matched-diagnostic one-step controls. “Problems” is the number solved at least once among four samples; “passes” is the number of verified passing samples.

C_{o}

replaces the model’s own failed predecessor with another theorem’s failed proof;

E_{m}

uses a wrong diagnostic matched by coarse error class and length.

Figure 5: Detailed copying and diversity across one-step conditions. Top: fraction of samples matching the normalized predecessor. Bottom: mean distinct normalized proof bodies among four samples. Hatching marks shuffled wrong diagnostics, except on the gray bare bars, whose prompt shows no predecessor. DeepSeek’s bare copying rate excludes its selected predecessor draw, so it is not directly comparable with the four-draw instruction-only rate. Whiskers are marginal problem-bootstrap intervals.

Contrast	Identifier subset ( $n=68$ )	Other problems ( $n=99$ )	Subset difference
$F_{C}-F$	$-14.7$ $[-26.5,-2.9]$ ( $21\to 11$ )	$-5.1$ $[-12.1,+2.0]$ ( $12\to 7$ )	$-9.7$ $[-23.7,+4.6]$
$F_{CE}-F_{C}$	$+26.5$ $[+16.2,+38.2]$ ( $11\to 29$ )	$+4.0$ $[-2.0,+10.1]$ ( $7\to 11$ )	$+22.4$ $[+9.7,+35.3]$
$F_{CE}-F_{CE_{m}}$	$+17.6$ $[+7.4,+27.9]$ ( $17\to 29$ )	$+1.0$ $[-5.1,+7.1]$ ( $10\to 11$ )	$+16.6$ $[+4.3,+29.5]$
$F_{CE}-I$	$-8.8$ $[-19.1,+1.5]$ ( $35\to 29$ )	$+1.0$ $[-5.1,+7.1]$ ( $10\to 11$ )	—

Appendix

Table 10: Qwen one-step contrasts split by whether the fixed predecessor’s diagnostic names an unknown identifier absent from the theorem statement (exploratory). Entries are paired differences in percentage points with 95% paired problem-bootstrap intervals (10,000 resamples); the last column resamples the two subsets independently. Parentheses give problems solved (pass@4) under the subtracted condition and then the first condition.

Figure 6: Identifier retention. Top: Qwen and DeepSeek-Prover unknown-identifier subsets. Bottom: Qwen without the instruction; the first three bars use the 62 problems whose replacement diagnostic omits the identifier, and the last uses the six whose replacement includes it. Whiskers are 95% problem-bootstrap intervals (2,000 resamples, seed 0). The panel heading is descriptive, not a causal interpretation. Copying and proof diversity appear in Fig. 5 .

Figure 7: Qwen unknown-identifier subgroup (68 problems). Correct diagnostics recover performance relative to code alone, but do not surpass instruction-only retrying. Outlined bars omit the instruction. The no-instruction code-plus-error comparison is unresolved; this subgroup accounts for 18 of the 22 problems recovered in the full bank (Table 10 ).

	Predecessors		Failed one-step samples
Category	Qwen	DeepSeek	Qwen	DeepSeek
Lean 3 keyword ( begin )	48	0	2,376	0
Valid in 2024 Mathlib, renamed since	7	18	1,269	1,089
Needs an unopened namespace	1	0	49	0
Never in either library	11	0	1,135	20
Local hypothesis or variable	1	0	271	61

Appendix

Table 11: Unknown identifiers named by diagnostics, classified against the verifier’s library and DeepSeek-Prover-V2’s evaluation-era library. Predecessor columns count problems; sample columns count failed one-step samples on the one-step banks, excluding the runner’s no-proof-body marker. Each diagnostic’s first unknown identifier is resolved as Lean would under the proof’s open declarations; single-letter names such as I and X that resolve under an opened namespace count as needing that namespace.

Contrast	Lean 3 predecessors ( $n=50$ )	Other problems ( $n=117$ )
$F_{C}-F$	$-26.0$ $[-40.0,-12.0]$ ( $21\to 8$ )	$-1.7$ $[-8.5,+5.1]$ ( $12\to 10$ )
$F_{CE}-F_{C}$	$+34.0$ $[+20.0,+48.0]$ ( $8\to 25$ )	$+4.3$ $[-0.9,+9.4]$ ( $10\to 15$ )
$F_{CE}-F_{CE_{m}}$	$+20.0$ $[+6.0,+34.0]$ ( $15\to 25$ )	$+2.6$ $[-3.4,+8.5]$ ( $12\to 15$ )
$F_{C_{o}}-F_{C}$	$+42.0$ $[+26.0,+58.0]$ ( $8\to 29$ )	$+2.6$ $[-3.4,+8.5]$ ( $10\to 13$ )
$F_{CE}-I$	$-12.0$ $[-26.0,0.0]$ ( $31\to 25$ )	$+0.9$ $[-4.3,+6.0]$ ( $14\to 15$ )

Appendix

Table 12: Qwen one-step contrasts (pp) split by whether the frozen predecessor is written in Lean 3 syntax (exploratory; 10,000 problem-bootstrap resamples). Parentheses give problems solved under the subtracted and then the first condition.

Status	Contrast	$\Delta$ (pp)	95% CI
Ordinary-shuffle registration (2026-09-07, 2026-09-08)
Primary	$CE-I$	$-18.3$	$[-41.8,+5.3]$
Primary	$(CE-CE_{s})-(E-E_{m})$	$+11.8$	$[-8.2,+29.1]$
Reg.	$C-I$	$-40.1$	$[-62.2,-17.0]$
Reg.	$CE-C$	$+21.8$	$[+10.9,+32.7]$
Reg.	$CE-CE_{s}$	$+18.2$	$[+8.2,+28.2]$

Appendix

Table 13: Qwen sequential contrasts at

k=64

on 11 problems, grouped by registration status. Primary and registered secondary (Reg.) contrasts were specified in a timestamped document before the corresponding arm was generated (Appendix A.4 ); exploratory (Expl.) contrasts were not. Intervals are unadjusted 95% percentile intervals from 10,000 paired problem-bootstrap resamples that carry all trajectories and memoryless draws for each resampled problem. An interval spanning zero resolves neither a difference nor equivalence. The content-free filler arm (noise) exists only for Qwen, so

E_{m}-\text{noise}

has no DeepSeek-Prover counterpart.

arm	1	2	4	8	16	32	64
$C$	3	8	12	15	17	20	25
$CE$	4	11	28	35	40	44	49
$CE_{m}$	2	9	13	15	17	20	23
$CE_{s}$	2	9	17	18	22	24	29
$E$	1	4	14	24	40	60	70
$E_{m}$	5	10	20	27	37	51	63

Appendix

Table 14: Qwen sequential success by horizon. The

E

, noise, and assert rows come from the earlier August launch (Appendix A.4 ); assert shows only a failure marker per prior attempt. Adaptive entries are trajectories of 110 with a first verified pass by

k

; memoryless

I

is the mean pooled pass@

k

estimate from 640 independent draws per problem.

Status	Contrast	$\Delta$ (pp)	95% CI
Ordinary-shuffle registration (2026-09-11)
Primary	$CE-I$	$-50.7$	$[-66.4,-34.5]$
Reg.	$C-I$	$-50.7$	$[-67.6,-33.6]$
Reg.	$CE-C$	$0.0$	$[-3.6,+3.6]$
Reg.	$CE-CE_{s}$	$+1.8$	$[-10.0,+13.6]$
Reg.	$CE-E$	$-42.7$	$[-61.8,-23.6]$

Appendix

Table 15: DeepSeek-Prover sequential contrasts at

k=64

on its own 11-problem bank, grouped by registration status. The prover’s sequential arms, including its ordinary-shuffle contrasts, were registered on 2026-09-11 before any prover depth attempt was generated. Entries are percentage-point differences with unadjusted 95% percentile intervals from 200,000 paired problem-bootstrap resamples; the

CE_{m}

family uses the registered 10,000 resamples. Memoryless

I

uses pooled pass@

k

CE-E

and

C-E

coincide to the reported precision; their per-problem difference vectors differ, but with 11 problem clusters the bootstrap percentiles land on the same endpoints.

arm	1	2	4	8	16	32	64
$C$	7	10	11	14	16	20	27
$CE$	9	9	12	14	16	20	27
$CE_{m}$	11	11	13	14	15	17	25
$CE_{s}$	9	9	9	11	14	21	25
$E$	9	12	26	35	52	61	74
$E_{m}$	9	17	24	35	53	72	90

Appendix

Table 16: DeepSeek-Prover sequential success by horizon. Adaptive entries are trajectories of 110 with a first verified pass by

k

; memoryless

I

is mean pooled pass@

k

from 640 draws per problem.

Figure 8: Per-problem sequential success for Qwen (top) and DeepSeek-Prover (bottom). Adaptive curves are the fraction of ten trajectories solved by attempt

k

; memoryless

I

is the pooled pass@

k

from 640 draws on that problem.

Model	Contrast	Full $\Delta$ (pp)	Range	Excl.
Qwen	$CE-I$	$-18.3$	$[-25.1,-12.1]$	1
	$C-I$	$-40.1$	$[-45.1,-34.4]$	0
	$CE-C$	$+21.8$	$[+20.0,+25.0]$	0
	$CE-CE_{s}$	$+18.2$	$[+16.0,+21.0]$	0
	$CE-CE_{m}$	$+23.6$	$[+20.0,+26.0]$	0
	$CE_{m}-I$	$-41.9$	$[-47.1,-36.4]$	0

Appendix

Table 17: Leave-one-problem-out sensitivity at

k=64

. “Range” is the smallest and largest point estimate over the 11 banks that each drop one problem. “Sign” counts banks whose estimate lies strictly on the other side of zero from the full-bank estimate, a zero full-bank estimate counting as nonnegative; “Excl.” counts banks on which the 95% interval’s exclusion of zero differs from the full bank’s. Reduced-bank intervals use Python random.Random(1) with 10,000 resamples; full-bank intervals use random.Random(0) with 10,000 resamples on Qwen and the registered NumPy procedure on DeepSeek-Prover. The Qwen stream differs from the registered analysis, so its full-bank bounds can differ slightly from Table 13 (for

CE-I

[-42.1,+5.5]

versus

[-41.8,+5.3]

Figure 9: Qwen all-sample similarity and visible output length. Similarity averages over parseable normalized proof bodies, comparing the first 3,000 characters with the predecessor. Output length is the median number of characters in retained response text. Whiskers use a 2,000-resample problem bootstrap (seed 0); they are not token-cost intervals. Daggers mark the figure’s instruction-only and random-word post-hoc arms.

Model	Accounting	Budget	$I$ (%)	$CE-I$	$p$	$E-I$	$p$
Qwen	total	200k	63.1	$-25.9$ $[-50.4,-2.4]$	0.066	$-6.8$ $[-26.1,+10.9]$	0.50
Qwen	input	20k	69.3	$-40.2$ $[-64.4,-15.2]$	0.018	$-26.6$ $[-44.5,-9.0]$	0.025
Qwen	output	20k	35.9	$-0.4$ $[-19.2,+17.7]$	0.98	$-13.1$ $[-29.8,+2.7]$	0.16
DeepSeek	total	200k	89.9	$-73.5$ $[-89.8,-53.5]$	0.002	$-26.3$ $[-46.3,-8.2]$	0.062
DeepSeek	input	50k	90.3	$-76.7$ $[-92.4,-56.7]$	0.002	$-37.6$ $[-60.3,-16.1]$	0.016
DeepSeek	output	5k	41.0	$-28.2$ $[-43.0,-15.2]$	0.002	$-1.0$ $[-9.3,+8.2]$	0.84

Appendix

Table 18: Sequential success at equal per-trajectory token budgets. Adaptive arms stop at their first verified proof and are capped at 64 attempts; memoryless

I

draws until the budget is spent, so its number of draws depends on the budget (about 71 at Qwen’s 200k total-token budget). Entries are arm minus memoryless

I

in percentage points, with 95% paired problem-bootstrap intervals and exact randomization

p

-values; the

I

column is memoryless success at the same budget. Total and input accounting charge the retained history; output-only accounting is the most favorable to repair. Qwen’s

E

outputs are predicted (see text).

Category	GPU-hours
Depth experiments	124.8
Qwen one-step	33.4
No-instruction ladder	10.7
Code plus shuffled diagnostic	1.7
DeepSeek-Prover one-step	1.2
Probes	0.1

Appendix

Table 19: Reported productive GPU-hours from the available campaign accounting. Categories follow that accounting and are not a complete inventory of the paper.

One-step		Sequential
Manuscript	Artifact	Manuscript	Artifact
bare, $I$ , $F$	bare , I , F	$I$ (memoryless)	memI
$F_{C}$ , $F_{E}$ , $F_{CE}$ , $F_{R}$	F_C , F_E , F_CE , F_R	$C$ , $CE$	C , CE
$F_{E_{s}}$ , $F_{CE_{s}}$	F_E_shuf , F_CE_shuf	$CE_{s}$ , $CE_{m}$	CE_s , CE_m
$F_{E_{m}}$ , $F_{CE_{m}}$	F_E_match , F_CE_match	$E$	f
$F_{C_{o}}$	F_C_other	$E_{m}$	E_s

Appendix

Table 20: Manuscript arm names and artifact labels. One-step labels are the arm field of the verified records; sequential labels name the files depth_<label>.jsonl . The _noI suffix marks a one-step arm without the retry instruction.

LLM Self-Correction

Large language model self-correction studies how language models detect and repair errors in their own answers, reasoning, and actions.

See all 159 papers

Oct 18, 2026

Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples

K

candidate tactics at each step and repairs a failed tactic at most

R

times. Instead of discarding failed tactics, we feed the compiler's error message to a pretrained repair model to fix individual rejected steps in place. This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets (

K \in \{1,3,5,8\}

), achieving up to a

32\%

relative gain and solving

82

additional theorems on a

1{,}990

-theorem subset of the LeanDojo benchmark. Repair is not free: it trades extra runtime for reachable proofs. But the trade is predictable: repair pays most when sampling is constrained; its return is front-loaded, with the first repair attempt capturing

84\text{--}96\%

of the total gain; and the gain comes almost entirely from shallow tactic-execution failures rather than structural errors such as type mismatches. This targeted repair successfully replicates on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions.

Haotian Deng, Chris Farber, Sonal Narasimha +2

Purdue University

Automated Theorem Proving Large Language Model-Guided Theorem Proving Lean Theorem Proving LLM Self-Correction Automated Program Repair

Ask PDF

Jul 30, 2026

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

LLM-based Lean proving systems increasingly organize a proof as a blueprint: a dependency graph of formal statements. We introduce BlueprintRepair, a repair interface that lets a model change this graph through ten schema-checked local operations. An operation names the node it edits, so the target theorem cannot be changed. Lean checks every applied change, and an accepted repair must declare every blueprint lemma its proof uses. We also construct BlueprintTrace, a benchmark of 142 controlled failures with complete accepted and rejected repair trajectories. We compare typed edits, exact source patches, and complete module rewrites under matched source, feedback, model, and budget, one episode per state and interface. With DeepSeek-V4-Flash, the three interfaces solve almost the same number of the benchmark's localized failures. Typed repair is the cheapest per solved state (patching is 1.30x as expensive, rewriting 2.06x), and within 10,000 completion tokens per task it reaches almost all of its final coverage, while both free-form interfaces are well behind. A second model, Qwen3.6-Flash, solves fewer states but keeps typed repair cheapest, puts it ahead on the proof-authoring states, and repeats the localized pattern.

Ruslan Khrulev

Lomonosov Moscow State University

Automated Theorem Proving Interactive Theorem Proving Lean Theorem Proving

Ask PDF

Oct 6, 2026

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner

In proof assistants such as Lean, a generated proof must pass machine compilation checks, so evaluation needs no human scoring. Direct generation fails on multi-step numeric propositions: a proof is valid only if every content integer is correct, so the pass rate is bounded by the k-th power of the per-integer accuracy. Controlled corruption across 2,617 reference proofs confirms this power law. SCOPE (State-Conditioned Operator Planning and Execution) enforces the natural division of labor: the model plans over an operator vocabulary, a symbolic engine executes the numerics, and a compiler renders the proof. On a 218-problem suite it certifies 191/218 (87.6%) with a 135M backbone; the 7B DeepSeek-Prover-V1.5-RL certifies 18/218 at 27.5 times the tokens and 37.5 times the wall-clock, and DeepSeek-Prover-V2-7B certifies zero on a bidirectional dual suite. Multi-step thinking costs 6.12 discrete decision actions per problem and produces no natural-language thinking text. Replacing the lagged engine state in the decision frame with the current one lifts the pass rate from 117/218 to 191/218, while up-weighting the chain-end loss hurts. On the public Lean-Workbook library, 2,132 of 3,536 gradeable admissible problems certify (60.29%) with zero regression on the main suite. All readings come from a version-frozen review with independent rechecks and reverse verification. Restricting free generation and keeping decision-time information visible is a more direct route than enlarging the model.

Hanchao Zhou, Jialei Li

Large Language Model-Guided Theorem Proving Automated Theorem Proving Lean Theorem Proving Efficient Language Model Reasoning

Ask PDF

Abstract

LLM Self-Correction

Explore similar work

Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

BlueprintRepair: Typed Local Edits for Failed Lean Proof Blueprints

SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner