谁能想到，未来数学定理的证明竟然也能交由人工智能来完成？

字节跳动豆包团队最新推出的 BFS-Prover，不仅刷新了行业最佳纪录，还向全球开放源代码，邀请学术界与开发者共同深入探索。这一突破性成果，为AI在数学证明领域的应用开辟了全新道路。

一、BFS-Prover：数学证明领域的全新探索

数学证明一直被视为AI难以攻克的挑战。与围棋拥有固定规则不同，证明定理的每一步都必须绝对严谨，否则整个逻辑链将瞬间崩塌。当前主流技术路线大多依赖蒙特卡洛树搜索或价值函数，例如DeepSeek-Prover-V1.5、HunyuanProver和InternLM2.5-StepProver。然而，这些方法的短板也十分突出：

• 资源消耗巨大：复杂的搜索策略需要海量计算资源。
• 推理效率低下：需反复试错方能寻得正确的证明路径。
• 适用性有限：不同数学问题往往需要定制策略，通用性不足。

而BFS-Prover则另辟蹊径，以广度优先搜索（BFS）为核心框架，并融合三项关键技术，大幅提升了数学证明的效率与成功率：

• 1. 专家迭代+自适应数据过滤：通过持续迭代优化，动态修正证明路径，极大减少无效搜索。
• 2. 直接偏好优化+Lean4反馈：让AI直接学习“优质证明”的标准，而非依靠穷举猜测。
• 3. BFS与长度归一化结合：防止因证明步骤长度不一而偏离最优解，确保搜索始终聚焦于正确方向。

二、成绩亮眼：MiniF2F 权威测试刷新记录

成绩是最有力的证明。在业界公认的MiniF2F测试集上，BFS-Prover以72.95%的准确率大幅领先其他模型。具体对比如下：

• DeepSeek-Prover-V1.5：63.5%
• InternLM2.5-StepProver：65.9%
• HunyuanProver：68.4%

不仅如此，BFS-Prover还在多个国际数学奥林匹克经典难题中一展身手，成功证明了包括imo_1959_p1、imo_1962_p2在内的题目，标志着AI数学推理能力达到了全新高度。