---

1. 引言：开启AI数学推理新篇章

在人工智能领域，形式化定理证明一直被视为一项极具挑战性的任务，它要求机器不仅能够理解复杂的数学概念，还能遵循严格的逻辑规则推导出正确的证明。今天，我们荣幸地向大家介绍DeepSeek-Prover-V2——一款专为Lean 4中的形式化定理证明而设计的开源大型语言模型。这款模型的诞生，标志着AI在数学推理领域迈出了重要的一步，其初始化数据通过由DeepSeek-V3驱动的递归定理证明流水线收集而成，为解决复杂数学问题提供了全新的思路和方法。

DeepSeek-Prover-V2的冷启动训练过程别具一格。它首先利用DeepSeek-V3将复杂问题分解为一系列子目标，这种分解能力是解决复杂数学问题的关键。已解决子目标的证明被综合成思维链过程，并与DeepSeek-V3的逐步推理相结合，为强化学习创建了初始的冷启动数据。这一创新过程使得我们能够将非形式化和形式化的数学推理无缝集成到一个统一的模型中，极大地提升了模型的推理能力和泛化性。

如上图所示，这是DeepSeek-V3的官方标志。该标志简洁而富有科技感，代表着DeepSeek系列模型在人工智能领域的创新与探索精神。对于关注AI数学推理的研究者和开发者而言，这个标志象征着前沿技术的引领者，预示着DeepSeek-Prover-V2将在形式化定理证明领域带来突破性进展。

2. 模型纵览：创新技术驱动卓越性能

通过递归证明搜索合成冷启动推理数据

构建高质量的冷启动数据集是训练强大定理证明模型的基础。为此，我们开发了一个简单而高效的递归定理证明流水线，将DeepSeek-V3作为子目标分解和形式化的统一工具。我们通过提示DeepSeek-V3将定理分解为高层证明框架，同时在Lean 4中形式化这些证明步骤，从而生成一系列子目标。这种方法确保了问题分解的逻辑性和形式化的准确性。

为了降低计算负担，我们采用了一种分层策略：使用较小的7B模型来处理每个子目标的证明搜索。一旦一个具有挑战性的问题的分解步骤全部得到解决，我们就将完整的逐步形式化证明与DeepSeek-V3相应的思维链配对，从而创建高质量的冷启动推理数据。这种数据合成方法不仅高效，而且能够确保数据的多样性和复杂性，为后续的模型训练奠定了坚实的基础。

利用合成冷启动数据进行强化学习

仅仅拥有高质量的数据还不足以训练出顶尖的定理证明模型，还需要先进的训练方法。我们精心挑选了一部分具有挑战性的问题，这些问题无法被7B证明器模型以端到端的方式解决，但所有分解的子目标都已成功解决。通过组合所有子目标的证明，我们为原始问题构建了一个完整的形式化证明。然后，我们将这个证明附加到DeepSeek-V3的思维链之后，该思维链概述了相应的引理分解，从而产生了非形式化推理与后续形式化的连贯合成体。

在使用合成冷启动数据对证明器模型进行微调之后，我们进行了一个强化学习阶段，以进一步增强其将非形式化推理与形式化证明构建相结合的能力。遵循推理模型的标准训练目标，我们使用二元的"正确或不正确"反馈作为主要的奖励监督形式。这种强化学习策略能够有效地引导模型学习到更优的推理路径和证明策略。

最终得到的模型——DeepSeek-Prover-V2-671B，在神经定理证明方面实现了最先进的性能。在MiniF2F-test上，它达到了88.9%的通过率，在PutnamBench的658个问题中成功解决了49个。这些成绩充分证明了我们提出的训练方法的有效性和模型的强大能力。MiniF2F数据集上DeepSeek-Prover-V2生成的证明可作为ZIP存档下载，为研究者提供了宝贵的资源。

如上图所示，该图展示了DeepSeek-Prover-V2与其他先进定理证明模型在关键基准测试上的性能对比。从图中可以清晰地看到，DeepSeek-Prover-V2在各项指标上均表现出显著优势，尤其是在MiniF2F-test上的高通过率。这一性能优势充分体现了DeepSeek-Prover-V2在形式化定理证明领域的领先地位，为相关领域的研究人员提供了一个强大的工具和新的研究起点。

3. ProverBench：AIME与教材问题的形式化新基准

为了更全面地评估定理证明模型的能力，一个多样化且具有挑战性的基准数据集至关重要。为此，我们引入了ProverBench，一个包含325个问题的基准数据集。其中，15个问题来自最近AIME竞赛（AIME 24和25）中的数论和代数题目，提供了真实的高中竞赛级别的挑战。这些题目通常需要灵活的思维和巧妙的解题技巧，能够有效测试模型的创造性推理能力。

其余310个问题则来源于精选的教材例题和教育教程，构成了一个多样化且具有教学基础的形式化数学问题集合。ProverBench的设计旨在实现对高中竞赛问题和本科级数学的更全面评估，涵盖了从基础到进阶的多个数学领域。

这个表格详细列出了ProverBench数据集在各个数学领域的分布情况。从表格中可以看出，微积分和线性代数题目数量较多，这反映了它们在本科数学教育中的核心地位。同时，AIME竞赛题目的加入也为评估模型解决非常规问题的能力提供了途径。ProverBench的多样性确保了它能够全面评估模型在不同数学分支和难度级别上的表现。

4. 模型与数据集下载：轻松获取前沿资源

为了促进相关领域的研究和应用，我们以两种模型规模发布DeepSeek-Prover-V2：7B和671B参数版本。DeepSeek-Prover-V2-671B构建于DeepSeek-V3-Base之上，继承了其强大的语言理解和生成能力，并针对定理证明任务进行了专门优化。而DeepSeek-Prover-V2-7B则基于DeepSeek-Prover-V1.5-Base构建，并将上下文长度扩展到了32K tokens，这使得它能够处理更长的证明过程和更复杂的问题描述。

除了模型本身，我们还发布了配套的数据集，以便研究者能够更好地复现我们的结果并进行进一步的创新。

这些资源的开放获取，体现了我们推动AI数学推理领域发展的决心。无论是学术界的研究者还是工业界的开发者，都可以利用这些先进的模型和数据来探索新的算法、开发新的应用，共同推动该领域的进步。

5. 快速上手：开启你的定理证明之旅

为了让用户能够快速体验DeepSeek-Prover-V2的强大功能，我们提供了简单易用的接口。你可以直接使用Huggingface's Transformers库进行模型推理。DeepSeek-Prover-V2-671B与DeepSeek-V3共享相同的架构，因此熟悉DeepSeek-V3的用户可以无缝过渡。有关详细信息和支持的功能，请参考Hugging Face上的DeepSeek-V3文档。

以下是一个为miniF2F数据集问题生成证明的基本示例代码：

from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # 或使用 DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
  sorry
""".strip()

prompt = """
Complete the following Lean 4 code:

```lean4
{}
```

Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
""".strip()

chat = [
  {"role": "user", "content": prompt.format(formal_statement)},
]

model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)

import time
start = time.time()
outputs = model.generate(inputs, max_new_tokens=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)

这段代码展示了如何使用DeepSeek-Prover-V2来解决一个具体的数学问题。通过简单的几行代码，用户就可以调用强大的定理证明模型，体验AI辅助数学推理的魅力。我们鼓励用户在此基础上进行扩展和创新，探索模型在更多复杂场景下的应用。

6. 许可协议

DeepSeek-Prover-V2模型的使用受模型许可协议的约束。我们致力于在促进创新的同时保护知识产权，因此请用户在使用前仔细阅读并遵守许可协议的各项规定。这不仅是对模型开发者劳动成果的尊重，也是确保AI技术健康有序发展的重要保障。

7. 联系我们

如果您在使用模型或数据集的过程中有任何问题、建议或发现bug，请随时通过提出issue或发送邮件至service@deepseek.com与我们联系。我们的团队致力于为用户提供及时的支持和帮助，并非常重视来自社区的反馈。您的参与将帮助我们不断改进DeepSeek-Prover-V2，使其更好地服务于科研和应用需求。

DeepSeek-Prover-V2的发布，不仅是DeepSeek团队在AI数学推理领域的一个重要里程碑，也为整个社区带来了新的机遇和挑战。我们相信，随着技术的不断进步，AI将在更多数学领域发挥重要作用，从辅助证明到发现新的数学定理。我们期待与全球的研究者和开发者一起，共同探索AI与数学交叉领域的无限可能，推动人工智能技术向更深层次、更广范围发展，为人类知识的进步贡献力量。未来，我们将继续优化模型性能，扩展其在更多数学分支和实际问题中的应用，努力实现AI在数学推理领域的更大突破。

【免费下载链接】DeepSeek-Prover-V2-7B 项目地址: https://ai.gitcode.com/hf_mirrors/deepseek-ai/DeepSeek-Prover-V2-7B