发表机构
University of Rochester（罗切斯特大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究针对Lean 4项目定理证明的上下文依赖难题，提出结合双模型生成等策略的编译器引导证明搜索框架，在7个项目实验中实现了通过率提升且LLM调用量减少的更优权衡。
AI 中文摘要
现实世界中Lean 4项目的定理证明颇具挑战性，因为证明常依赖项目特定上下文。尽管迭代精化可利用编译器错误修复失败的证明，但复用失败尝试需谨慎的搜索控制：部分证明能提供更优起点，后续修订可能降低部分正确证明的质量。我们提出编译器引导的证明搜索框架，平衡探索与利用：通过双模型生成探索多样起点，经停滞触发重采样；基于编译器支撑的成对比较，通过当前最优精化利用有前景的证明状态。在miniCTX-v2的7个真实Lean 4项目上实验显示，该方法相比pass@k基线实现了更优的有效性-效率权衡：在pass@32预算内，平均通过率提升12.8个百分点，同时减少21.9%的LLM调用量。
英文摘要
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%.
Comments18 pages; accepted to Findings of EMNLP 2026
