编译器引导搜索：Lean 4 定理证明成功率提升12.8%，调用成本降21.9%！
Compiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem Proving
👨💼 主理人解读 · 为什么值得关注
利用编译器错误引导自适应证明搜索，结合跨模型协同，提升Lean 4项目上下文相关证明效率。
📖 AI 总结
这篇论文提出了一种编译器引导的自适应证明搜索框架，用于解决真实Lean 4项目中定理证明依赖项目特定上下文的问题。研究指出，迭代修复虽可利用编译器错误，但失败尝试的复用需精细控制，因为不同起点的质量差异大，且后续修改可能破坏部分正确的证明。该框架通过双模型生成和停滞触发重采样来探索多样化起点，同时利用编译器基础的成对比较指导当前最优精化，平衡探索与利用。在miniCTX-v2的七个真实Lean 4项目实验中，该方法在pass@32预算内，平均通过率提升12.8个百分点，同时减少21.9%的LLM调用，展现出优于pass@k基线的效果-效率权衡。这一成果为依赖上下文的定理证明提供了更实用的自动化策略。
🔑 关键词速览
| Compiler-Guided Proof Search | 一种利用编译器反馈（如错误信息）来指导定理证明搜索过程的策略。 |
| Cross-Model Synergy | 通过结合多个模型（如不同的大语言模型）的生成结果来增强证明搜索的多样性和鲁棒性。 |
| Context-Dependent Theorem Proving | 在依赖项目特定上下文的定理证明场景中，证明过程需要考虑局部定义和已有代码。 |
| Pass@k | 一种评估指标，表示在 k 次尝试中至少有一次成功生成正确证明的概率。 |
| Stagnation-Triggered Resampling | 当搜索进展停滞时，触发重新采样以生成新的起点，从而避免陷入局部最优。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅