BFS-Prover

“BFS-Prover是字节豆包团队推出的一款自动定理证明系统，采用了基于大型语言模型（LLM）的先进技术。通过创新的广度优先搜索（BFS）算法优化，同时结合专家迭代和直接偏好优化等先进技术，实现了高效的证明搜索能力。该系统的核心在于采用了长度归一化的评分启发式方法，通过对数概率的累积评估证明路径的优先级，从而显著提升了搜索效率。

BFS-Prover主要功能包括：

• 高效的证明搜索：系统利用改进后的广度优先搜索算法，通过长度归一化的评分机制，显著提升了对深度推理路径的探索能力。
• 持续改进与数据积累：系统形成闭环，不断优化LLM生成的策略，通过LeanDojo执行并收集反馈，生成训练数据，不断优化LLM。

BFS-Prover的技术原理包括：

• 长度归一化的评分机制：通过引入长度归一化的评分函数，优化了传统BFS对深度路径的探索效率。
• 专家迭代与自过滤：采用专家迭代框架，逐轮筛选出更复杂的定理进行证明。
• 直接偏好优化（DPO）：通过比较成功与失败的策略，避免无效的推理路径，优化搜索效率。
• 分布式证明架构：采用分布式系统设计，实现并行证明，提高硬件利用率。
• 与Lean4的深度集成：与LeanDojo深度交互，确保证明过程的逻辑正确性。

BFS-Prover的应用场景包括形式化数学问题的自动证明、解决数学竞赛题目、本科和研究生级数学研究以及推动自动定理证明技术的发展。用户可以访问HuggingFace模型库获取更多信息。”