AI가 증명에 실패해도 그 실패를 버리지 않고 재활용해서 Lean 정리 증명 성공률을 높이는 방법
arXiv:2608.180842026-08-20
Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving
AI가 증명에 실패해도 그 실패를 버리지 않고 재활용해서 Lean 정리 증명 성공률을 높이는 방법
실제 프로젝트의 Lean 4 정리 증명은 그 프로젝트 고유의 정의와 규칙에 의존하기 때문에 어렵다. 이 논문은 컴파일러 오류 피드백을 이용해 실패한 증명을 고쳐 쓰되, 언제 새로 시도하고 언제 고친 결과를 받아들일지를 판단하는 탐색 프레임워크를 만들었다. miniCTX-v2의 실제 Lean 프로젝트 7개에서 기존 방식보다 평균 정답률을 12.8퍼센트포인트 올리면서 LLM 호출은 21.9% 줄였다.
METAL MEDIA 해설 도표
AI가 증명에 실패해도 그 실패를 버리지 않고 재활용해서 Lean 정리 증명 성공률을 높이는 방법
01일반 대화형 AI(제너럴리스트)와 Lean 전문 증명 AI(스페셜리스트) 두 모델이 각각 증명을 시도하게 하고, 두 결과 중 어느 쪽이 더 가능성 있는지 AI 심판이 비교해 선택한다.
02선택된 증명을 컴파일러 오류 메시지를 참고해 계속 고쳐나가되, 고친 결과가 이전보다 나은지 매번 AI 심판이 판정해서 나을 때만 교체하고 아니면 이전 상태를 유지한다.
03일정 횟수 동안 개선이 안 되고 정체되면 두 모델에서 완전히 새로운 증명 후보를 다시 뽑아 처음부터 다시 시도한다.
04miniCTX-v2 7개 프로젝트에서 pass@32 기준 평균 정답률 12.8%포인트 향상, LLM 호출 21.9% 감소를 달성했고, 비용도 GPT-5-mini 단독 방식 대비 낮았다(1.96달러 대 2.43달러).
05실제 성공 사례를 분석하니 새로 고친 증명 제안 중 약 절반(50.4%)이 심판에 의해 거부되었고, 성공한 증명의 39.5%는 최신 제안이 아니라 이전에 보존해둔 상태에서 나왔다.
METAL MEDIA이 원문을 바탕으로 재구성한 해설 도표이며, 논문 저자의 원문 figure가 아닙니다.
무엇을 했나
일반 대화형 AI(제너럴리스트)와 Lean 전문 증명 AI(스페셜리스트) 두 모델이 각각 증명을 시도하게 하고, 두 결과 중 어느 쪽이 더 가능성 있는지 AI 심판이 비교해 선택한다.
선택된 증명을 컴파일러 오류 메시지를 참고해 계속 고쳐나가되, 고친 결과가 이전보다 나은지 매번 AI 심판이 판정해서 나을 때만 교체하고 아니면 이전 상태를 유지한다.
일정 횟수 동안 개선이 안 되고 정체되면 두 모델에서 완전히 새로운 증명 후보를 다시 뽑아 처음부터 다시 시도한다.
miniCTX-v2 7개 프로젝트에서 pass@32 기준 평균 정답률 12.8%포인트 향상, LLM 호출 21.9% 감소를 달성했고, 비용도 GPT-5-mini 단독 방식 대비 낮았다(1.96달러 대 2.43달러).
실제 성공 사례를 분석하니 새로 고친 증명 제안 중 약 절반(50.4%)이 심판에 의해 거부되었고, 성공한 증명의 39.5%는 최신 제안이 아니라 이전에 보존해둔 상태에서 나왔다.
Table 1: Pass rate (%) on miniCTX-v2 across seven projects with Gemini-2.5-flash as the Generalist. Results of full proof generation are pass@16. Our method additionally reports average LLM calls per theorem (gray).
Method
Pass rate (%) per project
Avg.
Carleson
ConNF
FLT
Foundation
HepLean
Mathlib
Seymour
Gemini-2.5-Flash
44.00
28.00
35.29
52.00
38.00
40.00
72.00
44.18
DeepSeek-Prover-V2
42.00
30.00
47.06
54.00
42.00
42.00
70.00
46.72
Ours
48.00
34.00
50.00
60.00
54.00
46.00
78.00
52.86
avg calls
14.86
16.46
15.03
12.28
14.92
16.12
8.98
14.09
Table 2: Fraction of theorems proved by each component.
Component
Fraction (%)
Subtotal (%)
AutoSolve
28.36
28.36
Init (Generalist)
30.34
Init (Specialist)
9.44
39.78
Resample (Generalist)
0.49
Resample (Specialist)
1.01
1.50
Refine (Generalist)
18.91
Refine (Specialist)
11.46
30.37
Table 3: Effect of stagnation threshold N on mathlib-valid.
K/12
K/6
K/4
K/3
K/2
Pass Rate (%)
48.00
56.00
60.00
54.00
60.00
LLM Calls
30.24
27.12
24.42
27.60
27.76
Table 4: Intra-WP std (same wrong proof, multiple runs) vs. inter-WP std (different wrong proofs) for theorems in the Mathlib valid split.
Intra-WP std
Inter-WP std
T1
1.86
5.59
T2
0.80
2.58
T3
7.02
8.66
T4
0.00
0.00
T5
0.08
0.49
T6
5.42
6.54
T7
1.22
0.49
T8
4.06
4.85
T9
1.24
1.00
Avg
2.41
3.36
Table 5: Model selection rate in pairwise comparisons. Each comparison occurs when both GPT5-mini and DeepSeek-prover-v2 produce a candidate proof and the judge selects the better starting point.
Project
#Comparisons
GPT5-mini (%)
DeepSeek-prover-v2 (%)
ConNF
73
54.8
45.2
FLT
32
78.1
21.9
HepLean
45
71.1
28.9
Foundation
47
55.3
44.7
Carleson
49
53.1
46.9
Seymour
23
52.2
47.8
Mathlib
122
55.7
44.3
Total
391
58.6
41.4
Table 6: Detailed breakdown of theorems proved by each component on miniCTX-v2 test.
Component
Number of theorems proved per project
Avg.
Carleson
ConNF
FLT
Foundation
HepLean
Mathlib
Seymour
AutoSolve
0
7
11
20
4
10
5
8.14
Init (Generalist)
16
2
0
5
10
3
25
8.71
Init (Specialist)
4
1
3
1
4
3
3
2.71
Resample (Generalist)
0
0
0
0
1
0
0
0.14
Resample (Specialist)
0
0
0
0
1
0
1
0.29
Refine (Generalist)
5
5
4
3
7
8
6
5.43
Refine (Specialist)
2
7
1
1
5
3
4
3.29
Total
27
22
19
30
32
27
44
28.71
왜 중요한가
실제 소프트웨어 프로젝트 규모의 정리 증명은 그 프로젝트만의 맥락에 크게 의존해 AI가 어려움을 겪는데, 이 연구는 실패한 시도를 버리지 않고 재활용하는 탐색 전략만으로 별도의 모델 재학습 없이 성능과 비용을 동시에 개선할 수 있음을 보였다. 이는 코드 자동 수정이나 에이전트 기반 문제 해결처럼 컴파일러·실행기 피드백을 받는 다른 AI 작업에도 적용 가능한 탐색 설계 원칙을 제시한다.
이 논문의 용어
Lean 4 · 수학 정리를 컴퓨터가 검증할 수 있는 형식으로 작성하고 확인하는 프로그래밍 언어 겸 증명 보조 도구
pass@k · 모델이 k번 시도했을 때 하나라도 정답을 맞히면 성공으로 세는 평가 방식
컴파일러 피드백 · 증명이 틀렸을 때 어느 줄에서 왜 틀렸는지 알려주는 오류 메시지
AI 심판(Pairwise comparison) · 두 개의 증명 후보를 놓고 어느 쪽이 더 성공 가능성이 높은지 판단하도록 지시받은 LLM
정체 임계값(N) · 몇 번 연속으로 개선이 없으면 새로 탐색을 다시 시작할지 정하는 기준값
본문에 싣지 못한 그림
Figure 1: Overview of our framework. Exploration (left) generates two diverse candidates via a generalist and a specialist. Exploitation (right) maintains a single current-best proof s∗ and drives it toward verification: each repair produces a proposal, and an LLM judge decides whether to accept it. When refinement stagnates for N consecutive rounds, the system re-enters exploration and draws fresh candidates from both models. The Verification & Feedback layer (bottom) provides structured error feedback, tactic suggestions and verification signals.
Figure 2: Empirical refinement results of one theorem with different initial attempts. One theorem, 10 wrong proofs (WP) as starting points (rows), each iteratively refined 5 times (columns) with a 32-iteration budget. Cells show iterations to success; × marks failure. Theorem: Set_EAnnulus_oc_subset_co in carleson. More examples can be found in Figure 8 and Figure 9 in Appendix B.
Figure 3: Pass rate (%) vs. LLM calls across seven Lean 4 projects from miniCTX-v2. Gray dashed line is pass@32.
Figure 4: LLM cost breakdown under 32 average LLM calls. Specialist DeepSeek-Prover-V2-7B is self-hosted; its cost is estimated at the generalist’s per-token price (higher than the specialist) for a conservative comparison.
Figure 5: Pass rate (%) vs. LLM calls on RLMEval-FLT3 with informal proof guidance. Text labels show average calls from the generalist, specialist, and pairwise comparison (Cmp).
Figure 6: Ablation study results.
(b) Effect of pairwise comparison on call allocation and cost.
Figure 7: Pairwise comparison behavior on solved refinement trajectories. (a) Keep-current rate during successful refinement. (b) Final verification from preserved proof states.
Figure 8: Refinement heatmap for _isBigO_deriv_ofReal_cpow_const_atTop in the mathlib.
Figure 9: Refinement heatmap for eLpNorm_toReal_le in the Carleson.
Figure 10: LLM calls breakdown under 32 average LLM calls on miniCTX-v2 test.
Figure 11: Pass rate (%) vs. LLM calls on HepLean with GPT5.4-mini as the Generalist and Goedel-Prover-V2-8B as the Specialist.
Figure 12: Global refinement keep current rate on solved theorems (294 total steps).
