摘要

我们在 Lean 4 中引入了 DeepSeek-Prover-V1.5，这是一个专为定理证明而设计的开源语言模型，它通过优化训练和推理过程增强了 DeepSeek-Prover-V1。该模型在 DeepSeekMath-Base 上使用专门用于形式数学语言的数据进行了预训练，并使用源自 DeepSeek-Prover-V1 的增强形式定理证明数据集进行有监督微调。通过从证明助手反馈 (RLPAF) 进行强化学习可以进一步细化。除了 DeepSeek-Prover-V1 的单遍整体证明生成方法之外，我们还提出了 RMaxTS，这是蒙特卡洛树搜索的一种变体，它采用内在奖赏驱动的探索策略来生成不同的证明路径。 DeepSeek-Prover-V1.5 相较于 DeepSeekProver-V1 有显著的提升，在高中水平 miniF2F 基准（63.5%）和本科水平 ProofNet 基准（25.3%）的测试集上均取得了新的最优结果。

1.介绍

　　大型语言模型的最新进展对人工智能中的数学推理和定理证明产生了重大影响。尽管在自然语言领域取得了显著进展，但语言模型在形式化定理证明方面仍然面临巨大挑战，例如使用 Lean 和 Isabelle，这需要严格的推导以满足验证系统的形式化规范。即使是像 GPT-4 这样的高级模型也难以应对复杂的形式化证明，这凸显了所涉及的编码和数学的复杂性。形式化定理证明模型不仅必须掌握像 Lean 定理证明器这样的形式系统的语法和语义，还必须将抽象的数学推理与精确的形式化表示结合起来。
　　形式化定理证明中的语言模型通常采用两种策略：证明步骤生成和整体证明生成。证明步骤生成预测每个后续策略并使用形式化验证器对其进行验证，以获取有关当前策略状态的更新信息，通常使用树搜索技术来构建有效证明。相比之下，整体证明生成具有更高的计算效率，它根据定理陈述生成完整的证明代码，需要较少的通信预算来协调证明器模型和形式化定理验证器之间的协调。虽然 DeepSeek-Prover-V1 在 Lean 4 中通过整体证明生成取得了最先进的成果，但这种范式也带来了独特的挑战。它需要长期序列预测，而无需访问中间策略状态，而未来的策略取决于这些隐藏的结果。在 Lean 的策略模式中，证明是通过一系列转换证明状态的策略构建的。这种顺序性带来了复合错误的风险，一个误解就可能导致与有效证明路径的重大偏差。更具体地说，自回归模型在生成长证明时可能对中间策略状态产生错误的信念。
　　为了在证明步骤生成中无缝集成中间策略状态，同时保持整体证明生成的简单性和计算效率，我们在 DeepSeek-Prover-V1.5 中开发了一种统一的方法。该方法通过截断和恢复机制结合了证明步骤和整体证明生成技术的优势。该过程从标准整体证明生成开始，其中语言模型按照定理语句前缀完成证明代码。然后，Lean 证明器验证此代码。如果证明正确且完整，则该过程终止。如果检测到错误，则在第一个错误消息处截断代码，并丢弃任何后续代码。然后，成功生成的证明代码将用作生成下一个证明段的提示。为了提高模型新完成的准确性，我们将来自 Lean 4 证明器的最新状态作为注释附加在提示的末尾。值得注意的是，我们的方法不限于从上次成功应用的策略恢复。我们将截断和恢复机制集成到蒙特卡洛树搜索中，其中截断点由树搜索策略安排。此外，我们提出了一种新的无奖赏探索算法，用于 MCTS 解决证明搜索的奖励稀疏性问题。我们为树搜索agent分配内在动机，即好奇心，以广泛探索策略状态空间。这些算法模块扩展了我们的整体证明生成模型的功能，使其成为一种灵活的交互式定理证明工具，可以有效利用证明助手反馈并生成多样化的解决方案候选。

1.1 Contributions

我们提出了一个用于开发基于语言模型的形式数学证明器的全面框架，该框架集成了几个关键组件：大规模数学预训练、形式化数学语料库构建和扩充、从证明助手反馈中进行在线强化学习，以及用于定理证明长期规划的树搜索方法。预训练模型、有监督微调模型和强化学习模型以及蒙特卡洛树搜索算法的代码均已公开，可供进一步研究和应用。

• Pre-Training：我们通过对高质量数学和代码数据进行进一步预训练来增强基础模型在形式定理证明和数学推理方面的能力，重点关注 Lean、Isabelle 和 Metamath 等形式语言。
• Supervised Fine-Tuning：我们通过两种数据增强技术来改进 Lean 4 代码补全数据集。首先，我们使用 DeepSeek-Coder V2 236B 标注 Lean 4 代码的自然语言思维链注释，将形式定理证明与自然语言推理相结合。其次，我们在 Lean 4 证明代码中插入中间策略状态信息，使我们的模型能够有效利用编译器反馈。然后使用生成的数据集来微调预训练模型。
• Reinforcement Learning：我们采用 GRPO 算法对有监督微调模型进行证明助手反馈 (RLPAF) 强化学习。Lean 证明器的验证结果作为奖赏监督，以增强模型与验证系统形式化规范的对齐性。
• Monte-Carlo Tree Search：我们通过引入一种新的抽象和相应的搜索算法，改进了形式定理证明中的树搜索方法。我们的截断和恢复机制充当状态动作抽象，将树搜索过程无缝集成到整体证明生成框架中。我们提出了 RMaxTS，这是一种创新的蒙特卡洛树搜索算法，它利用 RMax 策略来解决稀疏奖赏证明搜索问题中的探索挑战。通过分配内在奖赏，该算法鼓励证明agent生成不同的规划路径，从而促进对证明空间的广泛探索。

1.2 Summary of Evaluations and Metrics

• miniF2F：在单次完整证明生成的设置中，DeepSeek-Prover-V1.5 在 miniF2F 测试集上的通过率达到 60.2%，比 DeepSeek-Prover-V1 的 50.0% 显著提升了 10.2 个百分点。结合树搜索技术，通过率进一步提升至新的最佳水平 63.5%。
• ProofNet：DeepSeek-Prover-V1.5 在 ProofNet 的单次完整证明生成设置中也表现出色，验证集的通过率为 21.6%，测试集的通过率为 23.7%。树搜索技术的集成进一步增强了这些结果，在验证集上实现了 25.4% 和测试集上 25.3% 的新最佳通过率。

2.Model Training

2.1 Pre-training

为了提高我们的语言模型生成形式化证明和通过数学语言进行推理的能力，我们进一步预训练了基础模型。这一改进涉及对包含代码和自然语言数学内容的高质量数据集进行训练。我们特别关注证明助手中广泛使用的形式化语言，例如 Lean、Isabelle 和 Metamath。我们将这个改进的模型命名为 DeepSeek-ProverV1.5-Base。

2.2 Supervised Fine-tuning

在本节中，我们探讨了 DeepSeek-Prover-V1.5 的有监督微调 (SFT) 所涉及的方法和流程。具体来说，我们通过添加详细的解释性注释来扩充 DeepSeekProver-V1 的证明数据集。此增强旨在改善自然语言描述和 Lean 4 代码之间的一致性，从而促进更好的形式数学推理。此外，我们将中间策略状态信息作为辅助预测任务纳入其中，以支持蒙特卡洛树搜索过程中使用的截断和恢复机制。我们将生成的模型称为 DeepSeek-ProverV1.5-SFT。
　　Data Curation。我们为有监督微调开发了一个全面的 Lean 4 代码补全数据集。该数据集包括从各种形式定理中得出的合成证明代码。这些定理来自各种项目，例如标准 Lean 4 数学库 Mathlib4、来自 DeepSeekProver-V1 和 Lean Workbook 的合成定理以及来自 miniF2F 和 ProofNet 基准的验证集。为了扩充形式证明数据，我们采用了专家迭代过程。这涉及使用语言模型生成证明、验证生成的证明数据、使用验证的数据重新训练模型，然后使用优化的模型生成其他证明数据。在每次迭代之间，我们使用 DeepSeek-Coder V2 236B 将证明代码之前的思维过程标注为注释。最后，我们针对蒙特卡洛树搜索的截断和恢复机制定制这些数据（详见第 3.1 节）。生成的证明数据集由 9645k 个序列组成。
　　Thought-augmented Proof Generation。 在 DeepSeek-Prover-V1 中，我们发现自然语言中的问题解决策略与 Lean 中的定理证明之间存在显著差距。在自然语言中，模型会生成详细的推理步骤来构建证明，而在 Lean 中，它们通常依赖于一系列高级策略调用来强力解决问题。这些高级策略虽然有效，但却掩盖了其内部工作原理和结果，阻碍了模型使用结构化数学推理解决复杂证明目标的能力。为了解决这个问题，我们开发了一种在生成定理证明代码之前结合自然语言推理的方法。与在每个证明步骤之前执行孤立的思维链推理的 Lean-STaR 类似，我们的方法将此推理直接集成为证明代码中的注释。我们使用 DeepSeekCoder V2 236B 通过两种方式增强 DeepSeek-Prover-V1 中的现有数据：首先，在证明块的开头插入完整的自然语言解决方案；其次，交替插入与设计策略相对应的特定自然语言步骤。使用这种数据格式训练模型会强制它在证明块的开头提出完整的数学推理，并在每个策略之前提出详细的步骤规划。这种方法成功地开发了新的行为，采用精细的数学思维来指导策略的生成。在训练数据中，使用两个不同的提示来区分 CoT（思路链）模式和非 CoT 模式以完成证明代码。两种模式下的输入和输出示例可在附录 A 中找到。
　　Prompt Augmentation with Tactic State Information。为了实现蒙特卡洛树搜索的截断和恢复机制，我们需要从模型生成的代码中提取策略信息。我们使用 LeanDojo 项目中的数据提取工具增强了 Lean REPL。这使我们能够以三元组的形式提取策略信息，其中包括每个策略的位置以及应用之前和之后的策略状态。这些信息有助于我们识别触发验证错误的具体策略代码（用于树搜索的扩展步骤，参见第 3.2 节）。对于生成的有效形式证明中的每个策略，我们将验证器返回的策略状态插入为注释“/- tactic state: … -/”。在训练期间，我们使用“/- tactic state: ”后面的所有token作为响应来计算有监督微调损失，而此注释之前的token用作提示，不参与训练损失计算。
　　Training Setting。我们基于预训练模型进行有监督微调，并使用 2,048 的batch size和 1e-4 的恒定学习率训练 9B 个 token。训练过程从 100 个warm-up步骤开始，以稳定学习动态。训练示例被随机连接以形成序列，最大上下文长度为 4,096 个 token。

2.3 Reinforcement Learning from Proof Assistant Feedback

强化学习 (RL) 已被证明能够有效增强有监督微调语言模型的数学推理能力。为了进一步增强 DeepSeek-Prover-V1.5-SFT，我们加入了强化学习阶段，从而形成了 DeepSeek-Prover-V1.5-RL 模型。此阶段利用 RL 根据 Lean 4 证明器的验证反馈来提高性能。此 RL 过程的具体细节如下所述。
　　Prompts。在强化学习阶段，我们使用有监督微调数据集中的一组定理陈述作为RL训练的提示。我们选择 DeepSeekProver-V1.5-SFT 在多次尝试后生成正确证明的成功率适中的定理。这确保模型有改进空间，同时仍然能够收到积极的反馈。经过筛选，我们保留了大约 4.5k 个独特的定理陈述。每个定理都以 CoT 和非 CoT 提示作为前缀，以增强模型在两种模式下的证明生成能力。
　　Rewards。当通过 RL 训练 LLM 时，训练好的奖赏模型通常会提供反馈信号。相比之下，形式化定理证明受益于证明助手对生成的证明的严格验证，从而提供了显著的优势。具体来说，如果验证正确，则每个生成的证明将获得 1 的奖赏，否则将获得 0 的奖励。虽然这种二元奖赏信号是准确的，但它也很稀疏，尤其是对于那些对有监督微调模型具有挑战性的定理而言。为了缓解这种稀疏性，我们选择了对有监督微调模型具有挑战性但可实现的训练提示，如上所述。
　　Reinforcement Learning Algorithm。我们采用组相对策略优化 (GRPO) 作为我们的 RL 算法，与 PPO 相比，该算法表现出了卓越的有效性和效率，主要是因为它消除了训练额外critic模型的必要性。具体来说，GRPO 为每个定理提示抽取一组候选证明，并根据组内输出的相对奖励优化模型。我们的提示选择策略旨在尽可能在候选中包括正确和不正确的证明，这与 GRPO 的群组相对性质非常吻合，从而增强了训练过程。
　　Training Setting。我们基于 SFT 模型进行强化学习训练，该模型既是初始模型，也是施加 Kullback-Leibler (KL) 散度惩罚的参考模型。我们使用 5e-6 的恒定学习率，KL 惩罚系数设置为 0.02。对于每个定理，我们抽取一组 32 个候选证明，最大长度设置为 2,048。训练batch-size配置为 512。

2.4 Evaluation

3.Exploration-oriented Monte-Carlo Tree Search

3.1 Tactic-level Tree Abstraction

　　为了在整体证明生成环境中实现树搜索方法，我们引入了证明树抽象来定义定制的状态和动作空间，并利用截断和恢复机制。大致遵循 Yao 等人 (2023) 的范式，我们首先将不完整的证明分解为与各个证明步骤相对应的树节点序列，然后利用存储在这些树节点中的部分内容继续证明生成过程。图 4 说明了从整体证明生成构建证明搜索树的过程。
　　Truncate: Proof Decomposition into Tree Nodes。我们在策略级构建证明搜索树，其中每条树的边代表策略状态的单个转移步骤。首先，我们将模型生成的整个证明提交给Lean证明器，以将其解析为策略。然后，我们在最早的验证错误处截断证明，确保所有后续策略代码都可以成功应用，以将证明推进到所需的定理。策略代码被分割成几个代码片段，每个代码片段包含一个有效的策略代码及其相关的思维链注释，对应于代表策略状态转换的单个树边。通过这种抽象，每个策略代码被转换为一系列树节点，形成从根到特定节点的路径。
　　Resume: Proof Generation from a Tree Node。在 Lean 4 中，不同的策略可以导致相同的策略状态，这意味着我们的证明树中的每个节点可以对应于实现相同结果的各种策略代码。为了处理这个问题，我们在每个节点存储一组这些等效的策略代码。当树搜索agent展开一个节点时，它会随机选择一个策略作为语言模型的提示。此提示包括以所选策略结尾的不完整证明代码和来自 Lean 证明器的策略状态信息作为注释块。经过微调的模型经过训练（参见第 2.2 节），可以识别和利用这种格式，使用添加了策略状态注释的不完整代码来指导后续的证明生成。

3.2 Interactive Theorem Proving via Monte-Carlo Tree Search

3.3 Intrinsic Rewards for Monte-Carlo Tree Search

3.4 Parallelization of Monte-Carlo Tree Search

3.5 Comparison with Existing Methods