BFS-Prover：面向基于大语言模型的自动定理证明的可扩展最佳优先树搜索
人工智能
2025-10-10 v3
摘要
大语言模型 (LLM) 的最新进展激发了人们对使用 Lean4 进行自动定理证明的日益浓厚的兴趣，其中有效的树搜索方法对于导航底层庞大的证明搜索空间至关重要。虽然现有方法主要依赖价值函数和/或蒙特卡洛树搜索 (MCTS)，但像最佳优先树搜索 (BFS) 这样更简单方法的潜力仍未得到充分探索。本文研究 BFS 能否在大规模定理证明任务中取得有竞争力的性能。我们提出了 BFS-Prover，一个可扩展的专家迭代框架，具有三项关键创新。首先，我们在每一轮专家迭代中实施策略性数据过滤，排除可通过束搜索节点扩展解决的问题，以专注于更困难的案例。其次，我们通过将直接偏好优化 (DPO) 应用于自动标注了编译器错误反馈的状态-策略对，提高了 BFS 的样本效率，从而优化 LLM 的策略，使其优先考虑富有成效的扩展。第三，我们在 BFS 中采用长度归一化，以鼓励探索更深的证明路径。BFS-Prover 在 MiniF2F 测试集上取得了 的当前最优分数，因此挑战了复杂树搜索方法被认为的必要性，证明了 BFS 在适当扩展时能够取得有竞争力的性能。为促进该领域的进一步研究和发展，我们已在 https://huggingface.co/ByteDance-Seed/BFS-Prover-V1-7B 开源了我们的模型。
引用
@article{arxiv.2502.03438,
title = {BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving},
author = {Ran Xin and Chenguang Xi and Jie Yang and Feng Chen and Hang Wu and Xia Xiao and Yifan Sun and Shen Zheng and Kai Shen},
journal= {arXiv preprint arXiv:2502.03438},
year = {2025}
}