arXiv:2502.03438v1 报告类型: 新颖 摘要: 近期大型语言模型（LLMs）的进步激发了使用Lean4进行自动定理证明的研究兴趣，在这种研究中，有效的树搜索方法对于导航证明搜索空间至关重要。尽管现有的方法主要依赖于值函数和蒙特卡洛树搜索（MCTS），但简单的如最佳优先搜索（BFS）的方法潜力仍未得到充分探索。本文研究了BFS是否可以在大规模定理证明任务中实现竞争力的性能。我们介绍了BFS-Prover，这是一种可扩展的专家迭代框架，具备三个关键创新。首先，我们实施了在每次专家迭代轮次中进行战略数据筛选，排除可以通过束搜索节点扩展解决的问题，以专注于更难的情况。其次，我们通过直接偏好优化（DPO）对自动注释有编译器错误反馈的状态-定理对进行采样效率的改进，使LLM的策略优先考虑有成效的扩展。第三，我们在BFS中采用长度归一化，鼓励探索更深层的证明路径。BFS-Prover在MiniF2F测试集上获得了71.31的得分，从而挑战了复杂树搜索方法的必要性，证明了当适当扩展时，BFS可以实现竞争力的性能。