推理

引言 近期大语言模型的进展显著影响了人工智能中的数学推理和定理证明。尽管在自然语言领域取得了显著进步，但语言模型在形式化定理证明方面仍然面临巨大挑战，例如使用 Lean 和 Isabelle，这需要满足验证系统形式化规范的严格推导。即使是像 GPT-4 这样的先进模型，在处理复杂的形式化证明时也显得力不从心，这突显了所涉及的编码和数学的复杂性。一个形式化定理证明模型不仅必须掌握像 Lean 定理证明器这样的形式化系统的语法和语义，还必须将抽象的数学推理与精确的形式化表示对齐。 形式化定理证明中的语言模型通常采用两种策略：证明步骤生成和完整证明生成。证明步骤生成预测每个后续策略（tactic）并使用形式化验证器对其进行验证，以获取有关当前策略状态的更新信息，通常利用树搜索技术来构建有效证明。相比之下，完整证明生成计算效率高，它根据定理陈述生成整个证明代码，协调证明器模型和形式化定理验证器之间的通信预算较少。虽然 DeepSeek-Prover-V1 在 Lean 4 中通过完整证明生成取得了最先进的结果，但这种范式也带来了其独特的挑战。它需要在无法访问中间策略状态的情况下进行长序列预测，并且未来的策略依赖于这些隐藏的结果。在 Lean 的策略模式中，证明是通过一系列转换证明状态的策略来构建的。这种顺序性引入了复合错误的风险，即单个误解可能导致严重偏离有效的证明路径。更具体地说，自回归模型在生成长证明时可能对中间策略状态有错误的认知。 为了在证明步骤生成中无缝集成中间策略状态，同时保持完整证明生成的简单性和计算效率，我们在 DeepSeek-Prover-V1.5 中开发了一种统一的方法。该方法通过截断-恢复机制结合了证明步骤生成和完整证明生成技术的优点。该过程始于标准的完整证明生成，其中语言模型在定理陈述前缀之后完成证明代码。然后 Lean 证明器验证此代码。如果证明正确且完整，则过程终止。如果检测到错误，则代码在第一个错误消息处被截断，并丢弃任何后续代码。成功生成的证明代码随后被用作生成下一个证明片段的提示词。为了提高模型新补全的准确性，我们将来自 Lean 4 证明器的最新状态作为注释附加在提示词的末尾。值得注意的是，我们的方法不限于从最后成功应用的策略恢复。我们将截断-恢复机制集成到蒙特卡洛树搜索 [MCTS] 中，其中截断点由树搜索策略安排。此外，我们提出了一种新颖的用于 MCTS 的无奖励探索算法，以解决证明搜索的奖励稀疏性问题。我们赋予树搜索智能体内在动机，即好奇心（a.k.a. curiosity），以广泛探索策略状态空间。这些算法模块扩展了我们完整证明生成模型的功能，使其成为交互式定理证明的灵活工具，可以有效利用证明助手反馈并生成多样化的解决方案候选。 贡献 我们提出了一个用于开发基于语言模型的形式化数学证明器的综合框架，该框架集成了几个关键组成部分：大规模数学预训练、形式化数学语料库的构建与增强、利用证明助手反馈的在线强化学习，以及用于定理证明中长期规划的树搜索方法。预训练模型、监督微调模型、强化学习模型，以及蒙特卡洛树搜索算法的代码，均已公开，可供进一步研究和应用。 预训练：我们通过在高质量的数学和代码数据上进行进一步预训练，重点关注 Lean、Isabelle 和 Metamath 等形式化语言，以增强我们基础模型在形式化定理证明和数学推理方面的能力。 监督微调：我们通过实施两种数据增强技术来改进 Lean 4 代码补全数据集。首先，我们使用 DeepSeek-Coder V2 236B 为 Lean 4 代码标注自然语言思维链注释，从而将形式化定理证明与自然语言推理对齐。其次，我们在 Lean 4 证明代码中插入中间策略状态信息，使我们的模型能够有效利用编译器反馈。然后，使用生成的数据集对预训练模型进行微调。 强化学习：我们采用 GRPO 算法，利用证明助手反馈（RLPAF）对监督微调模型进行强化学习。Lean 证明器提供的验证结果作为奖励监督信号，增强了模型与验证系统形式化规范的对齐。 蒙特卡洛树搜索：我们通过引入一种新颖的抽象及其对应的搜索算法，推进了形式化定理证明中的树搜索方法。我们提出的截断并恢复机制作为一种状态-动作抽象，将树搜索过程无缝集成到完整证明生成框架中。我们推出了 RMaxTS，这是一种创新的蒙特卡洛树搜索算法，它利用 RMax 策略来解决稀疏奖励证明搜索问题中的探索难题。通过分配内在奖励，该算法鼓励证明器智能体生成多样化的规划路径，从而促进对证明空间的广泛探索。 评估和指标总结 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% 的新最先进通过率。 预训练 为了增强我们语言模型在生成形式化证明和通过数学语言进行推理方面的熟练度，我们进一步对我们的基础模型进行了预训练。这一改进涉及在包含代码和自然语言数学内容的高质量数据集上进行训练。我们特别关注了在证明助手中广泛使用的形式化语言，例如 Lean、Isabelle 和 Metamath。我们将这个改进后的模型命名为 DeepSeek-Prover-V1.5-Base。 ...

摘要 我们引入了 DeepSeek-Prover-V2，这是一个开源的大语言模型，专为 Lean 4 中的形式化定理证明而设计，其初始化数据通过由 DeepSeek-V3 驱动的递归定理证明流程收集。冷启动训练过程始于通过提示 DeepSeek-V3 将复杂问题分解为一系列子目标。已解决子目标的证明被整合成思维链，结合 DeepSeek-V3 的逐步推理，为强化学习提供初始冷启动。这个过程使我们能够将非形式化和形式化数学推理整合到一个统一的模型中。由此产生的模型 DeepSeek-Prover-V2-671B 在神经定理证明方面取得了最先进的性能，在 MiniF2F-test 上达到了 88.9% 的通过率，并解决了 PutnamBench 中 658 个问题中的 49 个。除了标准基准测试，我们引入了 ProverBench，这是一个包含 325 个形式化问题的集合，以丰富我们的评估，其中包括从近期 AIME 竞赛（24-25 年）中选取的 15 个问题。对这 15 个 AIME 问题的进一步评估显示，该模型成功解决了其中的 6 个。相比之下，DeepSeek-V3 使用多数投票解决了这些问题中的 8 个，这突出表明大语言模型中形式化和非形式化数学推理之间的差距正在大幅缩小。 1. 引言 大语言模型 (LLMs) 推理能力的出现彻底改变了人工智能的众多领域，特别是在数学问题解决领域 (DeepSeek-AI, 2025)。这些进展很大程度上得益于推理阶段的扩展范式，最显著的是通过自然语言思维链推理 (Jaech et al., 2024)。LLMs 不再仅仅依靠一次前向传播来得出答案，而是可以反思中间推理步骤，从而提高准确性和可解释性。尽管自然语言推理在解决竞赛级数学问题方面取得了成功，但其应用于形式化定理证明仍然面临根本性挑战。LLMs 以一种固有的非形式化方式进行自然语言推理，依赖于启发式方法、近似和数据驱动的猜测模式，这些往往缺乏形式化验证系统所需的严格结构。相比之下，Lean (Moura and Ullrich, 2021)、Isabelle (Paulson, 1994) 和 Coq (Barras et al., 1999) 等证明助手在严格的逻辑基础上运行，其中每个证明步骤都必须明确构建并形式化验证。这些系统不允许任何歧义、隐含假设或细节遗漏。弥合非形式化、高层次推理与形式化验证系统的句法严谨性之间的差距，仍然是神经定理证明领域一个长期存在的挑战 (Yang et al., 2024)。为了利用非形式化数学推理的优势来支持形式化定理证明，一种经典方法是根据自然语言证明草图的指导，对形式化证明进行分层分解。Jiang 等人 (2023) 提出了一个名为 Draft, Sketch, and Prove (DSP) 的框架，该框架利用大语言模型生成自然语言的证明草图，然后将其翻译成形式化证明步骤。这种非形式化到形式化的定理证明范式与分层强化学习中的子目标概念非常相似 (Barto and Mahadevan, 2003; Nachum et al., 2018; Eppe et al., 2022)，其中复杂的任务被分解为更简单的子任务的层次结构，这些子任务可以独立解决，以逐步实现总体目标。在形式化定理证明中，子目标通常是一个中间命题或引理，有助于证明更大的定理 (Zhao et al., 2023, 2024)。这种分层分解与人类解决问题的策略一致，并支持模块化、可重用性和更高效的证明搜索 (Wang et al., 2024b; Zheng et al., 2024)。最近的研究通过采用多层层次结构进行结构化证明生成 (Wang et al., 2024a)，以及利用强化学习技术优化复杂定理分解为可管理子目标 (Dong et al., 2024)，进一步扩展了这一范式。 ...