“`markdown
豆包发布BFS-Prover模型：自动形式化数学推理的新突破
北京 – 人工智能在数学领域的应用迎来重要进展。字节跳动豆包大模型团队近日发布了其首个形式化数学推理模型BFS-Prover，并宣布开源。该模型在自动形式化数学定理证明方面取得了显著成果，超越了此前领先的DeepSeek-ProverV1.5。
自动形式化数学定理证明旨在将数学命题和证明步骤转化为计算机可验证的代码，从而确保推理过程的绝对严谨性，并构建可复用的数学知识库。这一领域的研究可以追溯到上世纪中叶，包括戴维斯、明斯基、王浩、吴文俊等逻辑学家、数学家和人工智能先驱都曾对此进行探索。
近年来，随着大型语言模型（LLM）能力的提升，自动定理证明系统更多地依赖于蒙特卡洛树搜索（MCTS）或价值函数（Value Function）来指导搜索过程。然而，这些方法增加了计算成本和系统复杂度，限制了模型在大规模推理任务中的可扩展性。
豆包团队推出的BFS-Prover挑战了这一传统范式。作为一种更简单、更轻量但极具竞争力的自动定理证明系统，BFS-Prover引入了三项关键技术：
- 专家迭代 (Expert Iteration) 与自适应性数据过滤：通过不断迭代优化，提升模型性能。
- 直接偏好优化 (DPO) 结合 Lean4 编译器反馈：利用Lean4编译器的反馈信息，对模型进行直接偏好优化。
- BFS 中的长度归一化：优化了BFS算法，使其更适用于定理证明任务。
实验结果表明，BFS-Prover在形式化数学测试集MiniF2F上实现了72.95%的准确率，创造了新的领域记录。这一结果首次证明，在合理的优化策略下，简单的BFS方法能够超越蒙特卡洛树搜索（MCTS）和价值函数（Value Function）等主流的复杂搜索算法。
该论文成果已对外公开，模型也已开源，旨在促进相关研究者之间的交流与合作。
主流方法的局限性
现有的自动定理证明系统，如DeepSeek-Prover-V1.5、InternLM2.5-StepProver和HunyuanProver，主要依赖复杂的蒙特卡洛树搜索（MCTS）和价值函数（Value Function）来解决问题。这些方法虽然在围棋等领域取得了成功，但在自动定理证明领域，由于状态空间极其复杂以及缺乏明确的过程奖励信号，效果并不理想。此外，复杂的搜索算法还带来了计算成本高、系统复杂度增加等问题。
BFS-Prover：化繁为简
豆包团队的研究者发现，最优先树搜索（Best-First Tree Search，即 BFS）是一种更简单有效的方法。BFS算法根据某种启发式函数评估每个节点的优先级，并按优先级访问节点，常用于解决约束满足问题和组合优化问题。
BFS-Prover系统的整体架构和工作流程如下：
- LLM生成策略：利用大型语言模型生成证明策略。
- LeanDojo执行：使用LeanDojo环境执行生成的策略。
- 获取反馈：从LeanDojo获取反馈信息。
- 生成训练数据：根据反馈信息生成训练数据。
- 优化LLM：使用训练数据优化大型语言模型。
整个系统形成闭环，实现了持续改进的专家迭代机制。
结论
豆包团队的BFS-Prover模型的发布，为自动形式化数学推理领域带来了新的思路和方法。该模型不仅在准确率上取得了突破，还证明了简单的BFS算法在经过优化后，可以超越复杂的搜索算法。这一成果有望为数学研究提供更坚实的基础，并推动人工智能在科学领域的应用。
参考文献
- BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. arXiv:2502.03438 [cs.AI]
- HuggingFace: https://huggingface.co/bytedance-research/BFS-Prover
“`
Views: 0