字节跳动整活了！正式发布 BFS-Prover，并全程开源！

谁能想到，未来证明数学定理也能交给 AI 来完成？

字节跳动豆包团队最新推出的 BFS-Prover，不仅刷新了行业记录，还向全世界开放源码，邀请学术界和开发者共同探索。

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

数学证明一直是AI攻克的高难挑战。不同于围棋的固定规则，证明定理要求每一步都严谨无误，否则整个逻辑便会崩盘。

目前，主流自动定理证明技术大多依赖蒙特卡洛树搜索或价值函数，如DeepSeek-Prover-V1.5、HunyuanProver和InternLM2.5-StepProver，但它们普遍面临：

资源消耗巨大

复杂搜索策略耗费大量计算资源；

推理效率低下

需要反复试错才能找到正确路径；

适用性有限

不同数学问题往往需不同策略。

而 BFS-Prover则另辟蹊径，采用最优先树搜索（BFS），结合三大核心技术：

1. 专家迭代+自适应数据过滤

持续优化证明路径，降低无效搜索；

2. 直接偏好优化+Lean4反馈

让 AI 直接学会“好证明”的标准；

3. BFS与长度归一化结合

避免因证明步骤长短不一而偏离最优解。

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

成绩是最有力的证明。BFS-Prover 在 MiniF2F 测试集上以72.95%的准确率轻松超越对手。

其它模型如 DeepSeek-Prover-V1.5、InternLM2.5-StepProver 和 HunyuanProver 分别为 63.5%、65.9% 和 68.4%。

它还成功解决了多个国际数学奥赛难题，如imo_1959_p1、imo_1962_p2，显示出AI在数学推理上的全新高度。

证明系统	搜索方法	Critic 模型	策略预算	准确率
BFS-Prover	BFS	否	Accumulative	72.95%
BFS-Prover	BFS	否	2048×2×600	70.83% ± 0.89%
HunyuanProver	BFS	是	600×8×400	68.4%
InternLM2.5-StepProver	BFS	是	256×32×600	65.9%
DeepSeek-Prover-V1.5	MCTS	否	32×16×400	63.5%