摘要
arXiv:2608.18084v1 公告类型：新论文
在真实世界的 Lean 4 项目中进行定理证明具有挑战性，因为证明通常依赖于项目特定的上下文。虽然迭代细化可以利用编译器错误来修复失败的证明，但重用失败的尝试需要仔细的搜索控制：某些证明比其他证明提供更好的起点，而后来的修订可能会降低部分正确证明的质量。
方法
我们提出了一种编译器引导的证明搜索框架，该框架平衡了探索与利用。它通过双模型生成和停滞触发的重采样来探索多样化的起点，同时通过编译器接地成对比较引导的当前最佳细化来利用有前景的证明状态。
实验与结果
在来自 miniCTX-v2 的七个真实世界 Lean 4 项目上的实验表明，我们的方法在有效性-效率权衡方面优于 pass@k 基线。在 pass@32 预算内，我们的方法将平均通过率提高了 12.8 个百分点，同时将 LLM 调用次数减少了 21.9%。