摘要
我们引入了 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)，进一步扩展了这一范式。
在本文中，我们开发了一种用于子目标分解的推理模型，利用一套合成冷启动数据和大规模强化学习来增强其性能。为了构建冷启动数据集，我们开发了一个简单而有效的递归定理证明流程，利用 DeepSeek-V3 (DeepSeek-AI, 2024) 作为子目标分解和形式化的统一工具。我们提示 DeepSeek-V3 将定理分解为高层次证明草图，同时在 Lean 4 中形式化这些证明步骤，从而产生一系列子目标。由于子目标分解由一个大型通用模型驱动，我们使用一个较小的 7B 模型来处理每个子目标的证明搜索，从而减轻了相关的计算负担。此外，我们引入了一个课程学习框架，该框架利用分解的子目标生成猜想定理，逐步增加训练任务的难度，以更好地指导模型的学习过程。一旦具有挑战性问题的分解步骤被解决，我们将完整的逐步形式化证明与 DeepSeek-V3 相应的思维链配对，创建冷启动推理数据。在此基础上，随后应用强化学习阶段进行进一步强化。图 2 | DeepSeek-Prover-V2 采用的冷启动数据收集过程概述。我们首先提示 DeepSeek-V3 生成自然语言证明草图，同时将其形式化为带有 sorry 占位符的 Lean 语句，用于省略的证明细节。然后，一个 7B 参数模型递归地解决分解的子目标。通过组合这些子目标证明，我们为原始复杂问题构建了一个完整的形式化证明。这个组合证明被附加到 DeepSeek-V3 的原始思维链中，为形式化数学推理创建高质量的冷启动训练数据。
非正式数学推理与形式化证明构建之间的联系。我们的实验表明，从任务分解中的非正式推理冷启动开始的强化学习显著增强了模型在形式化定理证明方面的能力。由此产生的 DeepSeek-Prover-V2-671B 模型在多个基准测试中建立了神经定理证明的新技术水平。在 MiniF2F-test 上，它在 Pass@32 时达到了 82.4% 的准确率，在 Pass@8192 时提高到 88.9%。该模型显示出对大学水平定理证明的强大泛化能力，在 Pass@1024 时解决了 37.1% 的 ProofNet-test 问题，并解决了 658 个具有挑战性的 PutnamBench 问题中的 49 个。此外，我们贡献了 ProverBench，这是一个包含 325 个形式化问题的基准数据集，旨在推进神经定理证明研究，其中包括来自著名 AIME 竞赛（24-25 年）的 15 个问题。DeepSeek-Prover-V2-671B 成功解决了 15 个具有挑战性的 AIME 问题中的 6 个，进一步展示了其复杂的数学推理能力。
2 方法
2.1. 通过子目标分解的递归证明搜索
将复杂定理的证明分解为一系列较小的引理作为垫脚石是人类数学家常用的有效策略。先前的几项研究在神经定理证明的背景下探索了这种分层策略，旨在通过利用现代大语言模型（jiang et al. 2023; Zhao et al. 2023; Wang et al. 2024a; Dong et al. 2024）的非正式推理能力来提高证明搜索效率。在本文中，我们开发了一个简单而有效的流程，该流程利用 DeepSeek-V3 (DeepSeek-AI 2024) 作为形式化定理证明中子目标分解的统一工具。
从自然语言推理中勾勒形式化证明草图
最近大语言模型的进展在非形式化推理能力方面取得了重大突破。为了弥合形式化推理和非形式化推理之间的差距，我们利用了最先进的通用大语言模型，这些模型以其强大的数学推理和指令遵循能力而闻名，来构建我们定理证明系统的基础框架。我们的研究结果表明，现成的模型，例如 DeepSeek-V3，能够分解证明步骤并以形式化语言表达它们。为了证明一个给定的形式化定理陈述，我们提示 DeepSeek-V3 首先用自然语言分析数学问题，然后将证明分解成更小的步骤，将每个步骤翻译成相应的 Lean 形式化陈述。由于通用模型已知在生成完整的 Lean 证明方面存在困难，我们指示 DeepSeek-V3 只生成一个省略细节的高级证明草图。由此产生的思维链最终形成一个 Lean 定理，该定理由一系列 have 语句组成，每个语句都以一个 sorry 占位符结束，表示一个待解决的子目标。这种方法模仿了人类构建证明的方式，其中一个复杂的定理被逐步简化为一系列更易于管理的引理。
子目标的递归求解
利用 DeepSeek-V3 生成的子目标，我们采用递归求解策略来系统地解决每个中间证明步骤。我们从 have 语句中提取子目标表达式，将其替换给定问题中的原始目标（参见图 3(a)），然后将前面的子目标作为前提纳入（参见图 3(b)）。这种构造使得后续子目标能够利用先前步骤的中间结果来解决，从而促进了更局部化的依赖结构，并有助于开发更简单的引理。为了减少大规模证明搜索的计算开销，我们采用了一个更小的 7B 证明器模型，该模型专门针对处理分解后的引理进行了优化。在成功解决所有分解步骤后，可以自动推导出原始定理的完整证明。
基于子目标的定理证明的课程学习
证明器模型的训练需要大型形式化语言问题集，这些问题集通常通过形式化现有自然语言数学语料库获得。尽管对人类撰写的文本进行形式化提供了高质量且多样化的形式化内容，但由此产生的证明器模型的训练信号往往是稀疏的，因为很大一部分计算尝试未能产生成功的证明，因此无法提供积极的奖励信号。为了生成更密集的训练信号，Dong 和 Ma (2025) 提出了一种自博弈方法，通过生成与原始定理陈述密切相关的易于处理的猜想来丰富训练问题，从而更有效地利用训练计算资源。在本文中，我们实现了一种直接的方法，利用子目标来扩展用于模型训练的形式化陈述的范围。我们生成两种类型的子目标定理，一种包含前置子目标作为前提，另一种不包含，分别对应于图 3(b) 和图 3(a)。这两种类型都被整合到专家迭代阶段 (Polu and Sutskver, 2020) 中，建立了一个课程，逐步引导证明器模型系统地解决精选的具有挑战性的问题子集。这一过程建立在与 AlphaProof 的测试时强化学习 (DeepMind, 2024) 相同的基本原理之上，后者通过生成目标问题的变体来增强模型解决具有挑战性的 IMO 级别问题的能力。
2.2. 统一非形式化推理与证明形式化
上述算法框架分两个阶段运行，利用两个互补模型：DeepSeek-V3 用于引理分解，以及一个 7B 证明器模型用于完成相应的形式化证明细节。该流程提供了一种自然且可扩展的机制，通过结合大语言模型的高级推理与精确的形式化验证来合成形式化推理数据。通过这种方式，我们将非形式化数学推理和证明形式化的能力统一在一个模型中。
通过合成数据进行冷启动。我们精选了一部分具有挑战性的问题，这些问题 7B 证明器模型无法端到端地解决，但其所有分解的子目标都已成功解决。通过组合所有子目标的证明，我们构建了原始问题的完整形式化证明。然后将此证明附加到 DeepSeek-V3 的思维链中，该思维链概述了相应的引理分解，从而产生了非形式化推理和后续形式化的连贯综合。这使得能够收集数百个高质量的合成冷启动数据，这些数据构成了训练 DeepSeek-Prover-V2 的基础。这种冷启动数据集生成策略与 Kimina-Prover (Wang et al., 2025) 不同，后者是同期关于形式化推理模型的工作。具体来说，我们通过将自然语言证明直接形式化为结构化的形式化证明草图来合成数据。相比之下，Kimina-Prover 采用逆向工作流程：它首先收集完整的形式化证明及其非形式化对应物，然后使用通用推理模型将中间的自然语言推理步骤逆向合成为连贯的思维块。
面向推理的强化学习。在对合成冷启动数据上的证明器模型进行微调后，我们执行一个强化学习阶段，以进一步增强其连接非形式化推理与形式化证明构建的能力。遵循推理模型的标准训练目标 (DeepSeek-AI, 2025)，我们使用二元正确或错误反馈作为主要的奖励监督形式。在训练过程中，我们观察到生成的证明结构经常与思维链指导提供的引理分解存在差异。为了解决这个问题，我们在训练的早期步骤中引入了一致性奖励，该奖励惩罚结构错位，明确强制在最终证明中包含所有分解的具有结构的引理。在实践中，强制这种对齐可以提高证明准确性，尤其是在需要多步推理的复杂定理上。
两阶段训练
DeepSeek-Prover-V2 通过一个两阶段训练流程开发，该流程建立了两种互补的证明生成模式：
- *高效率非思维链 (non-CoT) 模式*：此模式经过优化，可快速生成形式化的 Lean 证明代码，专注于生成简洁的证明，不包含显式的中间推理步骤。
- *高精度思维链 (CoT) 模式*：此模式在构建最终形式化证明之前，系统地阐述中间推理步骤，强调透明度和逻辑进展。
与 DeepSeek-Prover-V1.5 一致，这两种生成模式由两个不同的引导提示词控制（示例见附录 A）。在第一阶段，我们在课程学习框架内采用专家迭代来训练非 CoT 证明器模型，同时通过基于子目标的递归证明合成困难问题的证明。选择非 CoT 生成模式是为了加速迭代训练和数据收集过程，因为它提供了显著更快的推理和验证周期。在此基础上，第二阶段利用通过整合 DeepSeek-V3 复杂的数学推理模式与我们合成的形式化证明所合成的冷启动思维链 (CoT) 数据。CoT 模式通过进一步的强化学习阶段得到增强，遵循推理模型常用的标准训练流程。
专家迭代
DeepSeek-Prover-V2 的非 CoT 模式的训练过程遵循专家迭代范式，这是一种广泛采用的用于开发形式化定理证明器的框架。在每次训练迭代中，使用当前最佳的证明策略来尝试解决那些在先前迭代中仍未解决的具有挑战性的问题。这些成功的尝试，经过 Lean 证明助手的验证，被纳入 SFT 数据集，用于训练改进的模型。这种迭代循环确保模型不仅从初始演示数据集中学习，还提炼出其自身的成功推理轨迹，逐步提升解决更难问题的能力。整体训练过程与 DeepSeek-Prover-V1 和 DeepSeek-Prover-V1.5的过程基本一致，仅对训练问题的分布进行了两处修改。首先，我们纳入了来自自动形式化和各种开源数据集的额外问题，拓宽了训练问题领域的覆盖范围。其次，我们通过子目标分解增加了数据集中的问题，旨在解决 MiniF2F 基准测试有效分割中更具挑战性的实例。
监督微调
我们在 DeepSeek-V3-Base-671B 上进行监督微调，使用 5e-6 的恒定学习率，上下文窗口为 16,384 个 Token。我们的训练语料库包含两个互补的来源：(1) 通过专家迭代收集的非 CoT 数据，它生成没有中间推理步骤的 Lean 代码；以及 (2) 第 2.2 节中描述的冷启动 CoT 数据，它将 DeepSeek-V3 的高级数学推理过程提炼成结构化的证明路径。非 CoT 组件强调 Lean 定理证明器生态系统中的形式化验证技能，而 CoT 示例则明确地模拟了将数学直觉转化为形式化证明结构的认知过程。
强化学习
我们采用群体相对策略优化（GRPO）作为我们的强化学习算法，该算法在推理任务中表现出卓越的有效性和效率。与PPO不同，GRPO通过为每个定理提示词采样一组候选证明，并根据它们的相对奖励来优化策略，从而消除了对单独评论家模型的需求。训练使用二元奖励，其中每个生成的Lean证明如果被验证为正确则获得奖励1，否则获得奖励0。为了确保有效的学习，我们精心策划训练提示词，使其仅包含那些具有足够挑战性但监督微调模型可解决的问题。在每次迭代中，我们采样256个不同的问题，为每个定理生成32个候选证明，最大序列长度为32,768个Token
蒸馏
我们将 DeepSeek-Prover-V1.5-Base-7B的最大上下文长度从 4,096 个 Token 扩展到 32,768 个 Token，并使用 DeepSeek-Prover-V2-671B 强化学习阶段收集的 rollout 数据对该扩展上下文模型进行微调。除了 CoT 推理模式外，我们还纳入了在专家迭代期间收集的非 CoT 证明数据，从而实现了一种成本效益高的证明选项，该选项使用小型模型生成简洁的正式输出。此外，我们执行了与训练 671B 模型相同的强化学习阶段，以提升 DeepSeek-Prover-V2-7B 的性能。
3. 实验结果
在本节中，我们对 DeepSeek-Prover-V2 在形式定理证明的各种基准数据集上进行了系统评估，涵盖了高中竞赛问题和本科水平数学。DeepSeek-Prover-V2 的所有实验结果均使用 Lean 4.9.0 进行，测试环境与 DeepSeek-Prover-V1.5相同。除非另有说明，基线评估结果均来自其各自的原始论文。
3.1 MiniF2F 基准测试结果
MiniF2F包含 488 个形式化的问题陈述，这些问题来源于多种数学材料，包括 AIME、AMC 和 IMO 竞赛，以及 MATH 数据集中的精选问题。该基准测试包含奥林匹克水平的问题，涵盖初等数学的核心领域，包括代数、数论和归纳法。这些问题被分为两个大小相等的子集，分别表示为 miniF2F-valid 和 miniF2F-test，每个子集包含 244 个问题，在各个学科领域的分布相同。我们将 miniF2F-test 集专门用于评估模型性能，而 miniF2F-valid 问题则被纳入带有子目标分解的课程学习中。我们采用了 [Wang et al., 2025] 发布的 MiniF2F 修订版，并进一步对 miniF2F-valid 进行了两次额外修订，对 miniF2F-test 进行了一次修订（参见附录 C）。
与最先进模型 (SoTA) 的比较
表 1 总结了在 miniF2F-test 数据集上评估的最先进形式化定理证明建模的比较。实验结果表明，DeepSeek-Prover-V2-671B 在 miniF2F-test 基准测试上建立了新的最先进性能，在利用 CoT 生成策略时，仅用 32 个样本就取得了前所未有的 82.4% 准确率。值得注意的是，参数效率更高的
表 1 | 在 miniF2F-test 数据集上与最先进模型的比较。符号 μ ± σ 表示平均准确率 μ 和标准差 σ。标签 CoT 和 non-CoT 指的是统一模型的两种生成模式，每种模式由不同的提示词引导。
表 2 | DeepSeek-Prover-V2-671B 在 miniF2F 基准测试上解决的问题。miniF2F-valid 上的结果是在整个课程学习过程中收集的，DeepSeek-Prover-V2-671B 在剩余问题上进一步调用了 Pass@8192。
DeepSeek-Prover-V2-7B 也表现出具有竞争力的性能，超越了文献中所有现有的开源定理证明器。比较分析进一步揭示了一个引人注目的扩展模式：随着样本预算从 1 增加到 8192，7B 和 671B 变体之间的性能差距显著扩大，较大的模型表现出卓越的样本效率和更陡峭的改进轨迹。
通过子目标引导的课程证明难题。
表2详细列出了DeepSeek-Prover-V2在miniF2F基准测试中解决的问题，它在验证集上取得了91.0%的通过率，在测试集上取得了88.9%的通过率，整体表现强劲。值得注意的是，我们的子目标引导课程学习框架，将通用DeepSeek-V3与轻量级专用7B定理证明器集成，在miniF2F-valid上取得了90.2%的成功率，性能几乎与DeepSeek-Prover-V2-671B相匹配。这些发现突显了最先进的通用大语言模型超越自然语言理解，有效支持复杂形式推理任务的潜力。通过战略性的子目标分解，模型能够将难题分解为一系列易于处理的步骤，作为非形式推理与形式证明构建之间的有效桥梁。
CoT vs. non-CoT.
表1中的实验结果表明，在形式化数学推理中，CoT推理模式相对于non-CoT模式具有显著的性能优势。这进一步证实了CoT提示词的有效性，它鼓励将复杂问题分解为中间步骤，并进一步确认了推理时扩展（inference-time scaling）在形式化定理证明领域是成立的。作为这些发现的补充，表3提供了DeepSeek-Prover-V2在不同推理模式下生成的Token数量统计。正如预期，CoT模式产生了明显更长的输出，反映了其复杂的推理过程。有趣的是，在non-CoT设置下，671B模型平均生成的输出比7B模型更长。仔细检查发现，尽管在non-CoT模式下没有明确提示进行推理，但较大的模型经常在证明代码中插入简短的自然语言注释，这些注释类似于隐式推理步骤（参见附录A）。这表明，即使在没有明确的CoT提示词的情况下，高容量模型也可能隐式地内化和外化中间推理。
3.2. 本科水平基准测试结果
ProofNet (Azerbayev et al. 2023) 包含 Lean 3 中的 371 个问题，这些问题选自一系列流行的本科纯数学教科书，涵盖实分析和复分析、线性代数、抽象代数和拓扑学等主题。我们使用 Xin 等人 (2024b) 提供的 ProofNet 的 Lean 4 翻译版本，该版本进一步分为两个子集：ProofNet-valid 和 ProofNet-test，分别包含 185 个和 186 个问题。ProofNet 的测试子集专门用于模型评估，因为 ProofNet-valid 问题的变体包含在 Dong 和 Ma (2025) 提供的公共合成数据集中，该数据集用于我们的监督微调。结果如表 4 所示，与非 CoT 设置相比，使用 CoT 推理时 DeepSeek-Prover-V2 的通过率有了显著提高。值得注意的是，尽管训练数据主要来自高中水平，
表 4 | ProofNet-test 和 PutnamBench 上的实验结果。 Goedel-Prover-SFT 和 STP 在 PutnamBench 上的得分来自其原始论文，这些论文对包含 644 个问题的早期版本 PutnamBench 进行了评估。 PutnamBench [Tsoukalas et al., 2024] 是一个持续更新的基准测试，包含来自 William Lowell Putnam 数学竞赛的竞赛数学问题，涵盖 1962 年至 2023 年。Putnam 竞赛是美国和加拿大本科生一项享有盛誉的年度数学竞赛，涵盖分析、线性代数、抽象代数、组合学、概率论和集合论等多种大学水平领域。我们在最新发布的 PutnamBench 上评估了我们的模型，该版本包含 658 个用 Lean 4 形式化的问题。我们排除了与 Lean 4.0 不兼容的问题，并在剩余的 649 个问题集上评估了模型。如表 4 所示，DeepSeek-Prover-V2-671B 在 PutnamBench 中展示了增强的推理能力，解决了 49 个问题，显著优于其非 CoT 对应版本。这些结果进一步突显了 CoT 推理方法在处理具有挑战性的大学水平数学问题方面的有效性。
通过强化学习进行技能发现。在我们评估中一个意想不到的发现是 DeepSeek-Prover-V2-7B 在 PutnamBench 数据集上使用非 CoT 生成模式时表现出色。值得注意的是，这个较小的 7B 模型成功解决了 13 个其较大的对应版本 DeepSeek-Prover-V2-671B 未解决的问题，使我们在 PutnamBench 上解决的总问题数从 49 个增加到 62 个（总共 658 个）。在仔细检查模型的输出后，我们发现其推理方法中存在一个独特的模式：7B 模型频繁使用 Cardinal.toNat 和 Cardinal.natCast_inj 来处理涉及有限基数的问题（参见附录 B 中的示例，这些在 671B 版本生成的输出中明显缺失）。这种技术似乎使模型能够有效解决需要对基数值进行细微操作的一部分问题。
*表 6* | ProverBench 上的实验结果。A11 类别代表包含 325 个问题的完整评估集，而 AIME 24&25 表示从近期 AIME 竞赛中形式化的 15 个问题的子集。STP [Dong and Ma 2025] 的结果使用开源模型权重进行评估。
3.3. 组合问题上的结果
CombiBench [Liu et al. 2025] 是一个综合性基准测试，包含 100 个用 Lean 4 形式化的组合竞赛问题，每个问题都配有相应的自然语言陈述。我们在该基准测试的“带解”设置下评估了 DeepSeek-Prover-V2，其中正确答案嵌入在 Lean 陈述中，这使得评估可以专注于证明生成。在过滤掉与 Lean 4.9.0 不兼容以及包含多个 sorry 占位符的问题后，我们评估了基准测试中的 77 个问题，并成功解决了其中的 12 个。这些结果表明，虽然证明器模型主要在数论和代数领域进行训练，但它在组合问题上表现出了有希望的泛化能力，尽管这些问题难度很高。
3.4. ProverBench：AIME 和教科书问题的形式化
为了增强现有基准并推进形式定理证明的研究，我们引入了一个包含 325 个问题的数据集。其中，15 个问题是从最近 AIME 竞赛（AIME 24 和 25）中的数论和代数问题形式化而来，提供了真实的高中竞赛水平挑战。其余 310 个问题来自精选的教科书示例和教育教程，贡献了一个多样化且具有教学基础的形式化数学问题集合。该基准旨在实现对高中竞赛问题和本科水平数学的更全面评估。
AIME 形式化
美国数学邀请赛 (AIME) 是一项年度数学竞赛，旨在挑战和认可在数学方面表现出卓越能力的优秀高中生。AIME 24&25 的问题已成为评估大语言模型推理能力的标准基准。为了弥合形式化数学推理与非形式化数学推理之间模型性能评估的差距，我们整理并形式化了 AIME 24&25 中的一部分问题。为了确保更清晰的形式化，我们过滤掉了几何、组合学和计数问题，因为它们在 Lean 中的表示可能较为繁琐。由此产生了 15 个选定的问题，涵盖了初等数论和代数中竞赛级别的课题。
我们使用标准的自然语言数学推理的“寻找答案”任务，评估了 DeepSeek-V3-0324 在选定问题集上的表现。通过对 16 个采样响应进行多数投票，该模型成功解决了 15 个问题中的 8 个。相比之下，DeepSeek-Prover-V2-671B 在给定正确答案的条件下，在形式化证明生成设置下运行，能够为 15 个问题中的 6 个构建有效的形式化证明。这一比较突出表明，非形式化数学推理与形式化定理证明之间的性能差距正在大幅缩小，这反映出先进语言模型在语言理解和形式逻辑严谨性之间的一致性正在增强。
教材形式化
除了 AIME 24&25，我们还从高中竞赛和本科课程中使用的教材中精心挑选问题，以增强我们的基准，从而加强特定数学领域的覆盖。这一策划过程确保了基准在难度级别和主题领域上的全面代表性。因此，我们形式化了 310 个问题，涵盖了广泛的范围，从竞赛水平的基础数学到本科学习中通常遇到的高级主题。这个全面的基准涵盖了数论、初等代数、线性代数、抽象代数、微积分、实分析、复分析、泛函分析和概率论。通过有意包含如此多样化的数学领域，我们可以全面评估模型在不同抽象级别和推理风格下的能力。数论和代数问题测试模型处理离散结构和方程的能力，而分析类问题则评估模型对极限、连续性和微积分的理解。抽象代数和泛函分析部分挑战模型对抽象结构和空间进行推理，这需要复杂的正式推理能力。评估结果呈现在表 6 中。
4. 结论
在这项工作中，我们提出了一种综合性的流程，用于合成冷启动推理数据，以推进形式化定理证明。我们的数据构建过程基于递归定理证明框架，其中 DeepSeek-V3 作为统一模型，在 Lean 4 证明助手中同时用于子目标分解和引理形式化。我们的方法将高层证明草图与形式化步骤相结合，创建了一系列可管理的子目标，这些子目标可以使用较小的 7B 模型高效解决，显著降低了计算需求。我们开发的课程学习框架利用这些分解的子目标生成难度递增的训练任务，从而创建了更有效的学习进程。通过将完整的形式化证明与 DeepSeek-V3 的思维链推理相结合，我们建立了有价值的冷启动推理数据，弥合了非形式化数学思维与形式化证明结构之间的鸿沟。随后的强化学习阶段显著增强了这种联系，从而大幅提升了形式化定理证明能力。最终的模型 DeepSeek-Prover-V2-671B 在一系列基准测试中持续优于所有基线，涵盖了高中竞赛问题和本科水平数学。我们未来的工作将侧重于将这一范式扩展到类似 AlphaProof 的系统，最终目标是解决代表自动化定理证明挑战前沿的 IMO 级别数学问题。