BFS

BFS-Prover 是由字节跳动豆包大模型团队研发的一种基于大语言模型（LLM）的自动定理证明系统。该系统通过优化传统的广度优先搜索（BFS）算法，结合专家迭代与直接偏好优化等技术，提升了证明搜索的效率和准确性。其核心在于采用长度归一化的评分机制，通过累积对数概率评估路径优先级，从而更有效地探索复杂证明路径。此外，系统还支持分布式架构，实现大规模并行计算，提升处理能力。BFS-Prover 通过闭环机制不断积累数据并优化策略模型，逐步掌握更复杂的证明方法，并与 Lean4 深度集成，确保形式化数学问题的逻辑正确性。