BFS-Prover是由字节跳动豆包大模型团队推出的一款基于大语言模型（LLM）的自动定理证明系统。它通过改进传统的广度优先搜索（BFS）算法，结合专家迭代、直接偏好优化等技术，实现了高效的证明搜索。

BFS-Prover功能特点：

1、高效的证明搜索：

BFS-Prover 采用改进的广度优先搜索（BFS）算法，通过长度归一化的评分机制，优化了对深度推理路径的探索能力。

2、专家迭代与自过滤：

系统通过专家迭代框架，逐轮筛选出更复杂的定理进行证明。在每轮迭代中，使用束搜索（Beam Search）过滤掉容易解决的定理，专注于解决更具挑战性的定理。

3、直接偏好优化（DPO）：

BFS-Prover 基于 DPO 从编译器反馈中优化策略模型。通过对比同一状态下成功和失败的策略，模型能避免无效的推理路径，提高搜索效率。

4、长度归一化评分函数：

采用长度归一化的评分函数，通过将路径的累积对数概率除以路径长度的α次方（α∈[0,1]），缓解了传统 BFS 对深度路径的惩罚，能更有效地探索复杂证明。

5、分布式证明架构：

BFS-Prover 采用分布式系统设计，使用 Ray 框架在多台机器上运行，每台机器配备多个 GPU 和 CPU 核心，实现了近线性的扩展效率。

6、与 Lean4 的深度集成：

BFS-Prover 通过 LeanDojo 与 Lean4 交互，将数学问题编码为形式化系统，生成可验证的机器证明。

BFS-Prover应用场景：

1、形式化数学问题的自动证明：BFS-Prover 可以将数学问题编码为形式化语言（如 Lean4），生成可验证的机器证明。

2、数学竞赛题目的解决：能证明复杂的国际数学奥林匹克竞赛（IMO）题目。

3、本科和研究生级别的数学研究：帮助解决本科和研究生阶段的数学定理证明问题。

4、推动自动定理证明技术的发展：BFS-Prover 在 MiniF2F 测试集上刷新了准确率记录，为自动定理证明领域提供了新的方法和技术思路。