Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving
不丢弃AI证明失败的尝试,而是重复利用它们,提升真实Lean项目定理证明的成功率
在真实的Lean 4项目中证明定理很难,因为证明往往依赖项目特有的上下文。这篇论文构建了一个搜索框架,利用编译器的报错反馈修复失败的证明,同时精细控制何时继续探索新方案、何时改进当前方案。在miniCTX-v2的七个真实Lean 4项目上,相比pass@k基线方法,平均通过率提高12.8个百分点,同时LLM调用次数减少21.9%。
METAL MEDIA 解读图
不丢弃AI证明失败的尝试,而是重复利用它们,提升真实Lean项目定理证明的成功率
- 01用两个互补的模型生成候选证明:一个通用型推理大模型(generalist)和一个Lean专用证明模型(specialist),再由一个LLM裁判判断哪个候选更有希望作为起点
- 02被选中的证明会根据编译器报错反馈不断被修改,但每次修改只有在裁判判定确实比当前最佳版本更好时才会被采纳,否则保留原版本
- 03当修复连续多轮都没有进展(触发停滞计数)时,系统会从两个模型重新采样全新的候选证明并重新开始
- 04在miniCTX-v2七个项目上,在pass@32的预算内,该方法将平均通过率提高12.8个百分点,LLM调用减少21.9%,成本也更低(1.96美元 对比 GPT-5-mini pass@32的2.43美元)
- 05分析发现,即使在成功的证明轨迹中,约一半(50.4%)的修改提案会被裁判拒绝,而39.5%的成功证明来自之前保留下来的状态而非最新提案,说明保留好的中间状态和生成新提案同样重要
他们做了什么
- 用两个互补的模型生成候选证明:一个通用型推理大模型(generalist)和一个Lean专用证明模型(specialist),再由一个LLM裁判判断哪个候选更有希望作为起点
- 被选中的证明会根据编译器报错反馈不断被修改,但每次修改只有在裁判判定确实比当前最佳版本更好时才会被采纳,否则保留原版本
- 当修复连续多轮都没有进展(触发停滞计数)时,系统会从两个模型重新采样全新的候选证明并重新开始
- 在miniCTX-v2七个项目上,在pass@32的预算内,该方法将平均通过率提高12.8个百分点,LLM调用减少21.9%,成本也更低(1.96美元 对比 GPT-5-mini pass@32的2.43美元)
- 分析发现,即使在成功的证明轨迹中,约一半(50.4%)的修改提案会被裁判拒绝,而39.5%的成功证明来自之前保留下来的状态而非最新提案,说明保留好的中间状态和生成新提案同样重要
| 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 |
| 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 |
| 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 |
| 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 |
| 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 |
| 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任务,比如代码自动修复或智能体式问题求解。
本文术语
- Lean 4 · 一种可由计算机检查数学证明是否正确的编程语言兼证明辅助工具
- pass@k · 一种评估方式,只要k次尝试中有一次验证成功就算通过
- 编译器反馈 · Lean编译器给出的报错信息,指出证明在哪一行、为什么失败
- 成对比较裁判(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).
论文原文摘要（英文）
Theorem proving in real-world Lean 4 projects is challenging because proofs often depend on project-specific context. While iterative refinement can use compiler errors to repair failed proofs, reusing failed attempts requires careful search control: some proofs provide better starting points than others, and later revisions may degrade a partially correct proof. We propose a compiler-guided proof search framework that balances exploration and exploitation. It explores diverse starting points through dual-model generation and stagnation-triggered resampling, while exploiting promising proof states through current-best refinement guided by compiler-grounded pairwise comparison. Experiments on seven real-world Lean 4 projects from miniCTX-v2 show that our method achieves a better effectiveness--efficiency tradeoff than pass@k baselines. Within the pass@32 budget, our method improves average pass rate by 12.8 percentage points while reducing LLM calls by 21.9%.
在 arXiv 阅读最新论文
- SWE-bench Science: Can Coding Agents Resolve Engineering Tasks in Science?让AI编程助手去修复真实科学软件,连最强的那个也有一半以上任务没做对
- FlashPrefill V2: Block-Sparse Prefill Attention for Long-Context LLM Serving把稀疏注意力从论文原型变成能真正上线服务的加速方案
- PolicyGuide: From Guarding One Action to Guiding the Whole Workflow for Policy-Compliant LLM Agents让客服AI坐席不只是拦住一个危险动作,而是把整个流程走对
- EXIMO: VLM Guided Exploration of VLA Policies不用人工遥控演示,让会说话的AI来教机械臂做新家务
- EnvHarness: Awakening Static Worlds for Agent Learning不重新搭建训练环境,而是给现有环境套一层可插拔组件,针对每个智能体的具体弱点重新塑形
- Bounded Sovereignty and the Control Tax: Pricing AI Oversight When the Deployer Does Not Own the Model租用AI而非拥有AI的机构,安全监管能力只剩一半
- Beyond Imitation: Filtering On-Policy Distillation by Reasoning ProgressAI模仿老师模型学习时,会误伤本来推理正确的步骤,新方法专门过滤掉这种误伤
- PersonalBench: Measuring the Authorship Gap in LLM Personalization让AI模仿某人的文风,结果发现它始终摆脱不了自己的腔调