编译器引导的自适应证明搜索与上下文相关定理证明的跨模型协同

在现实世界的精益 4 项目中进行定理证明具有挑战性，因为证明通常取决于项目特定的环境。虽然迭代细化可以使用编译器错误来修复失败的证明，但重用失败的尝试需要仔细的搜索控制：某些证明提供了比其他证明更好的起点，而以后的修订可能会降低部分正确的证明的质量。我们提出了一个编译器引导的证明搜索框架，可以平衡探索和利用。它通过双模型生成和停滞触发的重采样探索不同的起点，同时通过基于编译器的成对比较指导的当前最佳细化来利用有希望的证明状态。对 miniCTX-v2 的七个真实 Lean 4 项目进行的实验表明，我们的方法比 pass@k 基线实现了更好的有效性和效率权衡。在 pass@32 预算内，我们的方法将平均通过率提高了 12.8 个百分点，同时将 LLM 调用减少了 21.9%。