arXiv提出基于编译器指导的修复方法，显著提升Lean 4定理证明效率

摘要：arXiv发布了一项关于自动化定理证明的研究，提出了一种基于编译器指导的修复方法，通过在线采样候选策略并利用预训练修复模型对失败步骤进行修复，显著提升了Lean 4定理证明的解决率。与仅依赖采样的基线方法相比，该方法在LeanDojo基准测试中实现了高达32%的相对提升，并额外解决了82个定理。该方法在保持较低计算开销的同时，展示了其在复杂推理任务中的潜力。

---

研究背景与动机

在自动化定理证明领域，传统的基于采样的方法依赖于语言模型生成候选策略，但当证明步骤失败时，这些方法会丢弃错误信息，导致效率低下。Lean 4等证明助手会提供精确的错误消息，但这些信息未被充分利用。为此，研究人员提出了一种基于编译器指导的修复方法，旨在通过修复失败步骤来提升证明效率。

技术机制剖析

该方法的核心在于一个在线的、有限步数的修复模块。具体来说，在每一步中，搜索过程会采样$K$个候选策略（$K \in {1,3,5,8}$），并在最多$R$次修复尝试中利用预训练的修复模型对失败的策略进行修复。修复模型通过接收编译器的错误消息来定位并修正错误，而不是简单丢弃失败的策略。

工程权衡与实测表现

1. 性能提升：与仅依赖采样的基线方法相比，该方法在LeanDojo基准测试中实现了高达32%的相对提升，并额外解决了82个定理。
2. 计算开销：修复过程并非免费，它以额外的运行时间为代价换取更高的解决率。然而，这种开销是可控的，尤其是在采样受限的情况下，修复的收益更为显著。
3. 收益分布：修复的收益主要集中在首次尝试中，捕获了总收益的84%-96%。此外，收益主要来自浅层的策略执行失败，而非结构性错误（如类型不匹配）。

开发者落地与部署建议

1. 适用场景：该方法适用于需要高解决率的复杂推理任务，尤其是在资源受限的环境中。
2. 优化建议：开发者可以根据具体任务调整$K$和$R$的值，以在解决率和计算开销之间找到最佳平衡。
3. 未来方向：未来可以探索将修复模型与更复杂的推理策略结合，进一步提升解决率和效率。

结论

这项研究展示了基于编译器指导的修复方法在提升自动化定理证明效率方面的巨大潜力，为未来的推理系统设计提供了新的思路。

---

消息来源：ArXiv AI (cs.AI) (2026-10-21)

—— 完 ——

主题标签： #Lean 4 关注 #定理证明 关注 #编译器指导 关注 #修复模型 关注 #自动化推理 关注