BFS-Prover：面向大语言模型自动定理证明的可扩展最佳优先树搜索

BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

https://arxiv.org/pdf/2502.03438

打开网易新闻 查看精彩图片

摘要：

近期大语言模型（LLMs）的进展激发了利用 Lean4 进行自动定理证明的广泛兴趣，其中高效的树搜索方法对于应对底层庞大的证明搜索空间至关重要。尽管现有方法主要依赖价值函数和/或蒙特卡洛树搜索（MCTS），但更简单的方法（如最佳优先树搜索，BFS）的潜力尚未得到充分探索。本文研究了 BFS 是否能在大规模定理证明任务中实现具有竞争力的性能。

我们提出了 BFS-Prover，一个可扩展的专家迭代框架，包含三项关键创新：
第一，在每轮专家迭代中实施策略性数据过滤，排除那些通过束搜索节点扩展即可解决的问题，从而聚焦于更具挑战性的案例；
第二，通过对状态-策略对（state-tactic pairs）应用直接偏好优化（DPO），提升 BFS 的样本效率——这些状态-策略对利用编译器错误反馈自动标注，从而优化 LLM 的策略，使其优先选择更有成效的扩展；
第三，在 BFS 中引入长度归一化，以鼓励探索更深的证明路径。

BFS-Prover 在 MiniF2F 测试集上取得了 72.95% 的当前最优成绩，挑战了复杂树搜索方法必不可少的普遍认知，表明在适当扩展下，BFS 同样能实现具有竞争力的性能。为促进该领域的进一步研究与发展，我们已在 https://huggingface.co/ByteDance-Seed/BFS-Prover-V1-7B 开源我们的模型。

1 引言

形式化语言中的自动定理证明（ATP）近期已成为评估大语言模型（LLMs）推理能力的关键基准。通过将数学问题编码到如 Lean4 等形式系统中，ATP 能够为复杂的数学命题生成机器可验证的证明，从而确保逻辑正确性（Moura 和 Ullrich，2021；Polu 与 Sutskever，2020）。尽管 LLMs 在自然语言数学和推理任务中取得了显著成功（Lewkowycz 等，2022；OpenAI，2023），但在形式化语言中的定理证明仍面临独特挑战（Yang 等，2024b；Wu 等，2022；He 等，2024；Wang 等，2023，2024；Lin 等，2024；Xin 等，2024a）。与非形式化推理不同，形式系统要求严格遵守语法和语义，并且必须在高度受限的形式框架内生成有效步骤。此外，ATP 中的动作（策略，tactic）空间极为庞大——每个证明状态都可能引出大量潜在策略，使得有效证明的搜索过程在计算上非常昂贵（Polu 等，2022）。

树搜索算法是 ATP 的基础，使策略模型能够高效地在庞大而复杂的证明空间中导航（Polu 与 Sutskever，2020）。在这些方法中，蒙特卡洛树搜索（MCTS）（Coulom，2006）因其能利用价值函数（评判模型）或内在奖励在探索与利用之间取得平衡而广受欢迎（Browne 等，2012；Silver 等，2016）。MCTS 在 AlphaZero 类框架中已展现出卓越成效，例如在国际象棋和围棋等游戏中（Silver 等，2017），这些游戏的状态空间虽大，但终止状态定义明确。然而，将 MCTS 和/或价值函数应用于 ATP 时会遇到特殊困难。与游戏具有清晰的胜负条件不同，证明搜索缺乏此类明确的终止状态：一次证明尝试理论上可以无限进行下去，直到找到证明或反例为止，这使得评估中间进展变得极具挑战性（Han 等，2021；Lample 等，2022）。此外，ATP 涉及更大且更动态的分支因子、稀疏且延迟的反馈，以及开放式推理过程。这些差异凸显了 ATP 的独特需求，也表明有必要对搜索方法进行专门适配，以应对其中的复杂性。

最佳优先树搜索（BFS）（Pearl，1984）提供了一种比 MCTS 更简单、更轻量的替代方案，其通过当前节点到根节点路径上累积的对数概率来优先扩展节点。尽管其简洁性和计算效率颇具吸引力，但现有文献通常认为 BFS 在定理证明中表现欠佳（Wu 等，2024a；Li 等，2024b；Xin 等，2024b），主要基于以下假设：

  • 缺乏高效探索能力：BFS 优先选择高概率路径，容易忽略那些概率较低但有效的解。由于缺乏诸如置信上限（UCB）或价值函数等探索机制，它难以在利用有希望的节点与探索多样化路径之间取得平衡。
  • 对深度推理路径存在偏见：BFS 依赖累积对数概率，本质上会惩罚较长路径，因为更深的扩展往往累积更低的得分。这种偏见使其在处理需要深度证明的定理时效果较差——这类定理的中间状态可能看似无望，却是最终找到解的关键所在。

1.1 本文贡献
本文挑战了当前普遍认为 BFS 本质上不适用于大规模自动定理证明（ATP）的观点。我们提出了 BFS-Prover 系统，通过有针对性的扩展策略，将 BFS 转变为一种简洁而强大的算法。我们的主要贡献如下：

  • 带自过滤机制的专家迭代：我们构建了一个专家迭代（Anthony 等，2017）框架，在每轮迭代中策略性地过滤掉那些可通过束搜索（beam search）（Steinbiss 等，1994）节点扩展即可解决的问题。这种过滤至关重要，因为它引导训练数据的积累聚焦于更困难的定理。随着专家迭代的推进，策略大语言模型（LLM）持续改进，通过 BFS 学习到更多样化的策略和更深的证明路径。
  • 基于编译器反馈的直接偏好优化（DPO）：我们利用 DPO（Rafailov 等，2024）来优化策略 LLM，所用的偏好对是在树搜索过程中自然生成的。对于给定的证明状态，每个偏好对包含一个正向策略（位于正确证明路径上）和一个负向策略（导致 Lean 编译器报错）。DPO 使策略分布更加锐化，使其能够避免无效策略，从而提升 BFS 的样本效率。
  • 用于深度探索的长度归一化：我们在 BFS 中引入了一种长度归一化的评分函数，以缓解其对深度推理路径的固有偏见。通过对路径长度归一化对数概率，BFS 能更有效地探索更深的证明路径，从而解决那些需要长策略链的定理。
  • 在 MiniF2F 上的实证结果：BFS-Prover 在 MiniF2F 测试集上取得了 72.95% 的累积得分，超越了文献中所有当前最先进的定理证明系统，包括 DeepSeek-Prover-V1.5（Xin 等，2024b）、InternLM2.5-StepProver（Wu 等，2024a）和 HunyuanProver（Li 等，2024b）。这一结果表明，BFS-Prover 能在保持轻量级设计（无需 MCTS 和价值函数的复杂机制）的同时，在自动定理证明任务中达到具有竞争力的性能水平。

论文结构安排：本文其余部分组织如下。第 2 节概述 BFS-Prover 系统，详细说明专家迭代框架、数据过滤机制、用于策略优化的 DPO 方法，以及 BFS 中的长度归一化。第 3 节描述在 MiniF2F 基准上的实际实现细节与实验结果，并与主流证明系统进行对比。第 4 节总结全文。

2 BFS-Prover 系统

本节详细说明 BFS-Prover 系统的设计；图 1 为系统示意图。

打开网易新闻 查看精彩图片

2.1 Lean4 环境与策略大语言模型

我们采用 LeanDojo（Yang 等，2024c）作为 Lean4 与 BFS-Prover 集成的交互式 Python 接口。它将 Lean4 转化为类似 Gym 的环境（Brockman，2016），便于策略大语言模型（LLM）与形式化证明助手之间的交互。具体而言，LeanDojo 通过在 Lean4 编译器中执行策略 LLM 生成的策略（tactic）来管理状态转移。如果某策略无法执行，LeanDojo 会捕获并返回相应的错误信息，为 DPO 提供关键反馈，用于优化策略 LLM。

2.2 长度归一化的最佳优先树搜索

BFS-Prover 采用一种最佳优先树搜索（BFS）的变体，以在庞大的状态-策略空间中进行证明搜索。该 BFS 引擎维护一个证明节点（即状态）的优先队列，其中每个节点（状态）的优先级由一种长度归一化的评分启发函数定义：

打开网易新闻 查看精彩图片
打开网易新闻 查看精彩图片

该评分机制结合可调节的节点扩展宽度，使 BFS 能够在证明空间中动态分配计算资源，在探索与利用之间取得平衡。例如，增大 α 值和/或减小扩展宽度会使搜索系统倾向于探索更深的路径，从而促进发现那些可能需要长策略链的复杂证明。

在每次节点扩展步骤中，策略大语言模型（LLM）通过某种采样机制生成一组策略（tactics），这些策略对应于证明树中的边。LeanDojo 随后在 Lean4 编译器中执行这些采样的策略，并返回执行结果。对于每个策略的应用，可能出现三种结果：(1) 如果该策略产生一个有效的证明状态，则创建一个常规树节点并加入节点队列；(2) 如果该策略完成了整个证明，则创建一个“证明完成”节点并返回该证明；(3) 否则，生成一个终止性错误节点，表示该路径无效。

2.3 专家迭代
BFS-Prover 采用一个专家迭代（expert iteration）流程，以迭代方式增强策略大语言模型（LLM）在复杂证明空间中导航的能力。给定一个包含未解决 Lean4 形式化命题的语料库，每轮专家迭代包含以下步骤：

  1. 束搜索过滤（Beam Search Filtering）：识别出那些可通过 BFS 配合束搜索节点扩展即可证明的形式化命题。这些命题随后从语料库中移除，其对应的证明数据——尽管是新生成的——被有意不加入累积的训练数据集中。束搜索具有确定性，能可靠地选择当前策略 LLM 生成的置信度最高的策略。因此，能通过该方法解决的证明被视为相对简单，因为它们与当前 BFS-Prover 系统的优势高度一致。通过策略性地滤除这些较简单的证明，训练数据语料库在迭代过程中不断被更具挑战性和多样性的样例所丰富。这种迭代式精炼确保策略 LLM 在后续迭代中逐步接触越来越复杂的推理模式，从而提升其解决更难定理的能力。
  2. 数据收集（Data Collection）：随后，我们对语料库中剩余未证明的形式化命题执行带有温度采样的 BFS 扩展以搜索证明。任务完成后，系统收集所有在成功证明路径上遇到的有效（证明状态，策略）对，并将其加入累积的训练数据集。相应已被证明的命题则从语料库中移除。此外，导致 Lean 编译器报错的无效策略也被记录下来，作为策略内（on-policy）的负样本，用于支持 DPO 的优化。
  3. 监督微调（Supervised Fine-Tuning, SFT）：在每次数据收集阶段之后，使用基础模型在全部累积的训练数据语料库上进行 SFT，训练出一个新的策略 LLM。该语料库包含此前所有专家迭代轮次中生成的（证明状态，策略）对。

打开网易新闻 查看精彩图片
打开网易新闻 查看精彩图片
打开网易新闻 查看精彩图片

这一专家迭代流程使策略 LLM 能够持续提升其生成有效策略的能力，同时随着训练数据语料库的增长，逐步适应更具挑战性的证明场景。

3 实践实现与基准测试结果

本节讨论 BFS-Prover 系统的实际实现细节，并展示其在 MiniF2F 测试集上的基准测试结果。所有实验均使用 Lean 4.7.0。

3.1 模型、数据与训练设置

基础模型与初始训练数据：为便于说明，我们在 BFS-Prover 中采用 Qwen2.5-Math-7B（Yang 等，2024a）作为策略大语言模型（LLM）微调的基础模型。为合理初始化专家迭代过程，我们利用 LeanDojo（Yang 等，2024c）从 Mathlib（Moura 和 Ullrich，2021）中提取的证明数据，作为冷启动（cold-start）数据集。随着专家迭代的推进，我们进一步整合来自 Lean-Github（Wu 等，2024b）——一个汇集 GitHub 上 Lean4 仓库的数据集——以及 Lean-Workbook（Ying 等，2024）——专注于奥数级别代数与分析的数据集——的状态-策略（state-tactic）数据。这些数据集覆盖了广泛的数学主题和形式化推理任务，为策略模型提供了生成有效策略和导航证明所需的基础能力。

形式化命题语料库：为构建专家迭代所用的数据语料库，我们使用内部工具对 NuminaMath-CoT 数据集（Li 等，2024a）进行自动形式化（autoformalization）。我们还补充了来自 Mathlib 的未证明定理以及 Lean-Workbook 中的形式化命题。最终形成的语料库包含约 90 万条无证明的形式化数学命题，为专家迭代提供了全面而坚实的基础。

打开网易新闻 查看精彩图片

专家迭代中的 BFS 配置。我们在整个专家迭代过程中将长度归一化参数 α 设为 0.0，以尽量减少归纳偏置。在束搜索过滤阶段，我们使用束宽（beam width）为 32，以识别容易求解的定理。在随后的数据收集阶段，我们采用基于温度的采样策略，温度设为 1.0，核采样（nucleus sampling）参数为 1.0，并设置采样宽度（sampling width）为 2、4 或 8，以探索多样化的证明路径。

3.2 分布式最佳优先搜索基础设施

为实现高效的大规模并行证明搜索，我们基于 Ray 构建了一个分布式系统，在多台机器上进行分布式定理证明。每台机器配备 8 块 A100 80GB GPU 和 128 个 CPU 核心。目标定理被均匀分配到各台机器上，每台机器运行一个独立的证明流水线。该系统由三个主要组件构成：

  • 基于 GPU 的策略 LLM 池：每台本地机器部署 8 个 7B 策略 LLM 实例，每个实例由一个专用 A100 GPU 上运行的异步 vLLM 引擎驱动。这些实例组成一个共享池，用于处理并发的策略生成请求。
  • 基于 CPU 的证明器池：每台机器运行 96 个并发的证明器实例，其余 CPU 核心保留用于常规系统操作。每个证明器实例对其分配到的定理独立执行 BFS 搜索。为实现均衡的 GPU 利用率，各证明器根据其索引对 8 取模的结果，以轮询（round-robin）方式将请求分发到不同的策略 LLM 实例上。每个证明器与其分配的策略 LLM 和 LeanDojo 环境进行异步交互。
  • 异步交互机制：整个分布式搜索系统利用 asyncio 管理证明器与策略 LLM 之间的高并发工作流。策略 LLM 池和证明器池均以 Ray Actor 的形式实现，通过 Ray 运行时系统实现动态资源管理。为确保系统响应性，我们对策略执行（通过 LeanDojo）和模型推理（通过 vLLM）均设置了超时阈值。

该分布式基础设施设计通过在机器间高效分配定理任务，实现了接近线性的扩展能力；同时在单机内部最大化硬件利用率，且无需承担跨机器通信开销。

3.3 专家迭代中的分布偏移

在本小节中，我们讨论并展示在专家迭代过程中，证明层面和策略层面如何出现分布偏移（distribution shift），从而揭示 BFS-Prover 在定理证明能力上的逐步提升。

证明层面。评估一个证明系统（如 BFS-Prover）有效性的一个关键指标，是其发现深度证明的能力。我们将“证明长度”定义为系统完成一个证明所使用的策略（tactic）数量。我们观察到，在每轮专家迭代中，证明长度的分布通常呈现高斯分布或高斯混合分布，这反映了形式化命题语料库中定理复杂度的多样性。有趣的是，随着专家迭代的推进，平均证明长度趋于增加，表明随着策略大语言模型（LLM）能力的提升，BFS 能够发现越来越深、更具挑战性的证明；参见图 2 的示意图。这一现象凸显了专家迭代框架的有效性以及 BFS 的可扩展性——即通过迭代式策略优化和搜索能力的增强，逐步应对更复杂的证明任务。

打开网易新闻 查看精彩图片

策略层面。除了在证明层面的演化之外，我们在专家迭代过程中也观察到策略层面有趣的分布偏移；参见图 3。值得注意的是，BFS-Prover 系统中的策略 LLM 在整个训练过程中维持着多样化的策略长度分布，并未坍缩为单一狭窄分布——后者是强化学习中常见的失败模式，即模型倾向于收敛于少数高奖励动作（Sutton，2018）。相反，我们观察到一种温和但有意义的分布转移：从极简策略（1–10 个 token）向更常用、更实用的策略模式（11–50 个 token）过渡。这种转移表明，通过专家迭代，BFS-Prover 中的策略 LLM 学会生成更复杂的策略，同时仍保留根据情境灵活使用简单策略的能力。保持策略多样性对于有效定理证明至关重要，因为不同的证明状态需要不同复杂度的策略，从简单的项重写到复杂的代数操作不等。

打开网易新闻 查看精彩图片

3.4 MiniF2F 上的结果

本小节讨论 BFS-Prover 在 MiniF2F 测试基准（Zheng 等，2021）上的表现。MiniF2F 是一个被广泛认可的用于评估形式化数学系统性能的数据集，包含一系列多样化的、源自数学竞赛级别的形式化问题。用于评估的策略大语言模型（LLM）检查点，是通过对 BFS-Prover 专家迭代流程中前 10 轮累积的所有状态-策略对进行监督微调（SFT）获得的，并在此基础上额外进行了一轮 DPO 优化，所用的 Lean 编译器错误信号如第 2.3 节所述。

3.4.1 与当前最先进方法的比较

我们现在将本文开发的 BFS-Prover 与文献中的主流定理证明系统进行比较，包括 DeepSeek-Prover-V1.5（Xin 等，2024b）、InternLM2.5-StepProver（Wu 等，2024a）和 HunyuanProver（Li 等，2024b）。

打开网易新闻 查看精彩图片
打开网易新闻 查看精彩图片

3.4.2 BFS 的缩放规律与 DPO 负信号的优势

最后，我们通过考察 BFS-Prover 在 MiniF2F 测试基准上的性能如何随证明搜索遍数（passes）的增加而提升，来研究其搜索时间的缩放规律，并评估利用 DPO 从负信号中学习对系统性能提升所带来的优势。我们总共执行了 pass@4096 实验，并在 pass@64、pass@128、pass@256、pass@1024 和 pass@2048 等中间节点评估性能。每个中间遍数的置信区间通过多次采样 pass@64 的运行结果计算得出。实验结果如图 4 所示，其中横轴采用对数刻度，阴影区域表示最小-最大范围（即置信区间）。

打开网易新闻 查看精彩图片

以下是我们对形式化定理证明中 BFS 缩放特性的若干观察。此处，SFT 指在专家迭代流程中累积的所有状态-策略对上进行的监督微调；SFT+DPO 则指在 SFT 模型基础上，额外应用一轮 DPO 优化，所用的策略内负样本来自 Lean4 编译器反馈（如第 2.3 节所述）。两种方法均采用相同的 BFS 参数配置：采样温度为 1.1，扩展宽度为 2，长度归一化因子 α = 0.5 。

  • SFT 与 SFT+DPO 两种训练方法均表现出对数缩放规律：随着证明搜索遍数的增加，性能提升逐渐放缓。具体而言，当遍数从 64 增至 2048 时，SFT 的得分从 64.58% 提升至 70.38%，而 SFT+DPO 从 64.98% 提升至 70.83%。这表明即使计算预算翻倍，性能增益也呈现持续但递减的趋势。
  • SFT+DPO 方法始终优于 SFT 基线，证明了引入来自 Lean4 编译器错误的负反馈的有效性。这种优化使模型能更好地区分成功与失败的证明策略，从而提升证明搜索效率和成功率。
  • 从最小-最大范围来看，两种方法的性能波动幅度相近（约 3–4%）。这表明，尽管 DPO 提高了整体成功率，但其在证明搜索中的稳定性与 SFT 基线相当。

4 结论与讨论

本工作表明，最佳优先搜索（BFS）能够高效扩展，并在自动定理证明（ATP）中取得当前最优的性能。我们的结果挑战了传统观点——即在大规模形式化定理证明中，必须依赖蒙特卡洛树搜索（MCTS）和/或价值函数等更复杂的搜索方法。通过开发 BFS-Prover，我们论证了：一个经过精心设计的 BFS 系统，若结合专家迭代框架，并融入策略性数据过滤、直接偏好优化（DPO）和长度归一化等机制，不仅能在性能上超越现有方法，还能保持计算上的简洁性。我们在 MiniF2F 基准上取得 72.95% 的当前最优得分，实证验证了该方法的可扩展性。

BFS-Prover 的成功对 ATP 领域具有若干重要启示。首先，它表明算法的简洁性若辅以周密的扩展策略，完全可以胜过更复杂的方案。这一发现提示未来 ATP 研究或许应更多关注对简单方法的精炼与扩展，而非一味追求日益复杂的架构。其次，我们观察到 BFS 性能随计算资源增加而呈现对数缩放规律，这说明尽管增加计算量总能带来一定提升，但仅靠扩大搜索规模可能存在根本性局限。这一观察激励未来研究探索能够实现优于对数缩放（better-than-logarithmic scaling）的新方法。

局限性

尽管 BFS-Prover 系统在自动定理证明中展现出强大的性能，但仍存在若干局限性，尤其体现在模型规模方面。我们当前的实现依赖于一个相对较小的 70 亿参数（7B）策略模型，这可能会限制系统学习和运用更复杂数学推理模式的能力。虽然更大的模型（例如 32B 或 70B 参数）有可能捕捉更深刻的数学洞见并生成更精细的策略，但它们在树搜索场景下会带来显著的计算挑战，无论是在训练还是推理阶段。

这种权衡在实践中尤为明显：更大的模型通常需要更多的 GPU 显存，并具有更长的推理延迟，这会显著减少在固定时间预算内可探索的状态数量。此外，复杂的数学证明可能生成非常冗长的状态描述，这些描述可能超出 7B 模型的实际上下文窗口长度，从而导致模型遗漏生成恰当策略所必需的关键信息。

原文： https://arxiv.org/pdf/2502.03438