近日，豆包大模型团队提出 BFS-Prover，一个基于大语言模型 (LLM) 和最优先树搜索 (BFS) 的高效自动形式化定理证明系统。
团队通过该成果发现，简单的 BFS 方法经过系统优化后，可在大规模定理证明任务中展现卓越性能与效率，无需复杂的蒙特卡洛树搜索和价值函数。
在数学定理证明基准 MiniF2F 测试集上，BFS-Prover 取得了 72.95% 准确率，超越此前所有方法。
自动形式化数学定理证明，是人工智能在数学推理领域的重要应用方向。此类任务需要将数学命题和证明步骤转化为计算机可验证的代码，这不仅能确保推理过程的绝对严谨性，还能构建可复用的数学知识库，为科学研究提供坚实基础。
早在上世纪中叶，戴维斯、明斯基、王浩等不少逻辑学家、数学家、人工智能先驱便已在探索相关问题。
近些年在 LLM 能力加持下，自动定理证明系统更多依赖于复杂的蒙特卡洛树搜索 (MCTS) 或价值函数 (Value Function) 来指导搜索过程。
然而，这些方法引入了额外计算成本，并增加系统复杂度，使模型在大规模推理任务中的可扩展性受限。
字节跳动豆包大模型团队推出的 BFS-Prover 挑战了这一传统范式。
作为一种更简单、更轻量但极具竞争力的自动定理证明系统，它引入了三项关键技术：专家迭代 (Expert Iteration) 与自适应性数据过滤、直接偏好优化 (DPO) 结合 Lean4 编译器反馈、BFS 中的长度归一化。
从结果看，BFS-Prover 在形式化数学测试集 MiniF2F 上实现了 72.95% 的准确率，创造了新的领域记录。
该结果也首次证明：在合理的优化策略下，简单的 BFS 方法能够超越蒙特卡洛树搜索和价值函数等主流的复杂搜索算法。
目前，论文成果已对外公开，模型也最新开源，期待与相关研究者做更进一步交流
。
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
论文链接：
https://arxiv.org/abs/2502.03438
HuggingFace 链接：
https://huggingface.co/bytedance-research/BFS-Prover
1. 主流方法蒙特卡洛树搜索和价值函数真的必要么？
在形式化数学证明领域，将抽象的数学概念转化为能够用计算机验证的严格形式，是一项极具挑战性的任务。
该过程要求每一步推理都符合严格的形式逻辑规则，且每个步骤都必须经过 Lean 证明助手验证。
在自动形式化定理证明过程中，计算机面临的核心挑战是——在庞大且高度结构化的证明空间中，找出有效路径。这一难点与传统搜索问题有本质区别，具体表现如下：
1）搜索空间庞大：
每一步推理可能有数十甚至上百种可能的策略选择；
2）动态变化的策略空间：
不同于棋类游戏的固定规则，数学定理证明中，每个状态下可应用的策略集合不断变化，且规模庞大，无明确界限；
3）反馈稀疏与延迟：
直到完成证明前，系统很难获得有效的中间反馈；
4）开放式推理过程：
缺乏明确的终止条件，证明尝试可能无限延续；
自动定理证明系统如 DeepSeek-Prover-V1.5、InternLM2.5-StepProver，主要依赖复杂的蒙特卡洛树搜索和价值函数解决上述问题。
这些类 AlphaZero 算法框架在游戏中表现出色，尤其在围棋领域大放异彩，推动了强化学习概念破圈。但在自动定理证明领域，由于状态空间极其复杂以及缺乏明确的过程奖励信号，上述主流方法效果并不理想。此外，复杂的搜索算法还带来了计算成本高、系统复杂度增加等问题。
2. 化繁为简，用机器证明数学定理可以更简单
人类遇到问题，往往优先采用最可能解决的方法。最优先树搜索（BFS）与之类似。
这是一种在“树”或“图”中搜索节点的算法。核心思想是根据某种启发式函数，评估每个节点优先级，按优先级访问节点，常用于解决约束满足问题和组合优化问题，特别是在需要快速找到近似最优解的情况下。
此前不少研究者认为，简单的 BFS 算法缺乏有效的探索机制，尤其是对深度路径的探索，难以胜任大规模定理证明任务，但豆包大模型团队的研究者发现了其中的突破口，并提出了 BFS-Prover 系统。
下图展示了 BFS-Prover 系统的整体架构和工作流程。
图右侧展示了训练数据生成过程，包括用于监督微调的 SFT 数据 (成功证明路径上的状态-策略对) 和用于直接偏好优化的 DPO 数据 (从同一状态出发的正确策略与错误策略的对比)。
图左侧展示了 BFS 机制，通过 LeanDojo 环境与 Lean4 交互，从根节点开始，按照优先级顺序 (1→2→3...) 探索证明路径，直到找到证明完成节点 (绿色 A 点)。
整个系统形成闭环：LLM 生成策略 → LeanDojo 执行 → 获取反馈 → 生成训练数据→优化 LLM → 再次生成策略，实现了持续改进的专家迭代机制。
团队认为，BFS-Prover 系统不仅证明了经过优化的 BFS 方法性能方面可以超越复杂的蒙特卡洛树搜索
和价值函数，并且能保持架构的简洁性和计算效率。其技术特征如下：
BFS-Prover 采用专家迭代框架，通过多轮迭代不断增强 LLM 能力。在每轮迭代中，系统会先使用确定性的束搜索 (Beam Search) 方法过滤掉容易解决的定理，将这些“简单问题”从训练数据中剔除，再着手解决“复杂问题”。
这一数据过滤机制颇具创新性，确保了训练数据逐渐向更具挑战性的定理证明任务倾斜，使 LLM 能够学习更多元化的证明策略。
如下图实验数据显示，随迭代进行，系统能够发现证明的平均长度变长，覆盖面变广，证明了这一方法的有效性。
如下图所示，经过多轮迭代，模型生成的策略长度分布发生了显著变化：非常短的策略（1-10 个 token）比例下降，而中等长度策略（11-50 个 token）比例则有所增加。
这种分布变化表明，LLM “深度思考能力”在加强，避免了常见的强化学习导致的分布坍缩问题，并逐渐掌握了更复杂、更信息丰富的证明策略。
