五一劳动节期间，DeepSeek再度给AI领域带来重磅消息——开源了全新的DeepSeek-Prover-V2模型。尽管近期网络上流传着DeepSeek-R2即将发布的传言，但DeepSeek先行推出了这款专注于数学定理证明的强大模型，并继续秉承其一贯的开源精神。
两款强大模型同步开源
此次DeepSeek开源了两个版本的DeepSeek-Prover-V2模型:
- DeepSeek-Prover-V2-671B：基于DeepSeek-V3-Base构建，拥有6710亿参数，目前是定理证明领域的性能之王
- DeepSeek-Prover-V2-7B：基于DeepSeek-Prover-V1.5-Base构建，参数量为70亿，支持长达32K tokens的上下文长度
这两款模型都已在Hugging Face上正式发布：
- DeepSeek-Prover-V2-7B: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
- DeepSeek-Prover-V2-671B: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
什么是DeepSeek-Prover-V2？
DeepSeek-Prover-V2是一款专为”数学AI编程语言”Lean 4打造的开源大语言模型，专注于形式化定理证明。简单来说，它能够将抽象的数学定理转化为计算机可验证的严格证明过程，为数学研究带来革命性的工具。
它的最大特点是能够将非形式化的数学推理(即人类常用的推理方式)和严格的形式化证明无缝结合，让模型既能像人类一样灵活思考，又能像计算机一样严谨论证，实现了数学推理的一体化融合。
惊人性能：刷新多项记录
在定理证明的各项基准测试中，DeepSeek-Prover-V2-671B展现出前所未有的实力：
- 在MiniF2F测试集上达到了88.9%的通过率，创下历史新高
- 成功解决PutnamBench数据集中658道题目中的49道
- 在AIME 24和25等高难度数学竞赛问题上也表现出色
不少网友测试后表示，这款模型在解决复杂数学问题上的能力甚至超过了OpenAI的o4-mini和XAI的Grok-3等顶级模型。有钻研数学奥林匹克的学生惊呼：”奥数从没这么简单过！”
技术创新：递归与强化学习结合
DeepSeek团队在技术报告中详细揭示了Prover-V2的核心训练方法，主要基于”递归+强化学习”的创新组合。模型训练过程分为几个关键步骤：
1. 通过子目标分解实现递归式证明搜索
DeepSeek-Prover-V2采用了类似人类数学家的思考方式——将复杂定理拆解为一系列较小的引理来证明。具体实现过程包括：
- 首先提示DeepSeek-V3生成自然语言形式的证明草图，并将其形式化为Lean语言的定理陈述
- 然后使用7B证明模型递归地解决分解出的子目标
- 最后组合这些子目标的证明，构建出原始复杂问题的完整形式化证明
这种方法不仅提高了证明效率，还扩展了模型能够处理的定理范围。
2. 统一非形式化推理与形式化证明
DeepSeek团队巧妙地融合了高层次的自然语言推理和低层次的精确证明过程：
- 挑选出特别难解决的问题，将它们拆解成一个个小目标
- 当小目标各自得到证明后，组合成完整的严谨证明
- 将这个完整证明添加到DeepSeek-V3生成的”思维链”中，形成集人类思维和机器验证于一体的训练数据
通过这种方式，团队收集了几百条高质量的训练数据，为模型提供了坚实的学习基础。
3. 强化学习提升推理能力
在初步微调后，团队引入了Group Relative Policy Optimization (GRPO)强化学习算法：
- 对每道题采样多个候选证明，通过相对奖励优化策略
- 使用二元奖励机制：Lean验证成功得分1，失败则为0
- 特别设计了结构一致性奖励，确保模型生成的证明与思维链分解思路保持一致
这一训练方法极大提高了模型在复杂定理证明中的准确率。
ProverBench：全新的数学基准测试集
除了模型本身，DeepSeek还发布了ProverBench——一个包含325道题目的基准数据集：
- 15道题来自AIME 24和25等最新数学竞赛的数论与代数题目
- 310道题精选自教材示例和教学教程，覆盖多种难度和领域
这个数据集旨在对模型在高中竞赛和本科数学两个层面进行全面评估，为数学AI研究提供更系统的测试平台。
ProverBench链接：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench
实验结果与亮点发现
研究过程中，团队发现了几个有趣的现象：
CoT vs. non-CoT模式
DeepSeek-Prover-V2支持两种互补的证明生成模式：
- 高效率非思维链(non-CoT)模式：快速生成精简的Lean代码，不包含中间推理步骤
- 高精度思维链(CoT)模式：系统化表达推理过程，逐步构建逻辑清晰的证明
实验表明，在形式化数学推理中，CoT模式相比non-CoT模式具有显著的性能优势，证实了思维链提示在定理证明领域的有效性。
小模型的意外能力
令人惊讶的是，DeepSeek-Prover-V2-7B在PutnamBench数据集上采用non-CoT模式时，表现出了超越预期的能力。它甚至解决了13道671B模型未能解决的题目！
分析发现，7B模型习得了一种独特的技术——频繁使用Cardinal.toNat和Cardinal.natCast_inj来处理涉及有限基数的问题，这种技术在671B模型中罕见。这一发现表明，强化学习不仅能提升整体表现，还能使模型发展出专门的解题技巧。
快速上手指南
想试用DeepSeek-Prover-V2吗？这里是一个简单的示例，展示如何使用Hugging Face的Transformers库进行模型推理：
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)
model_id = "deepseek-ai/DeepSeek-Prover-V2-7B" # 或 deepseek-ai/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
{}未来展望
DeepSeek团队表示，未来的工作将着重于将这一框架扩展到类似AlphaProof的系统。其最终目标是解决代表自动定理证明领域前沿的IMO级数学难题。随着DeepSeek-Prover-V2的发布，我们可能正在见证数学研究方式的重大变革。这款模型不仅仅是一个技术进步，更代表了人类与AI协作解决复杂问题的新范式。
与此同时，大家对DeepSeek-R2的期待也愈发强烈。正如一位网友所说：”敲敲这头小蓝鲸，R2到底什么时候发出啊！”
如果想要使用GPT Plus、Claude Pro、Grok Super官方付费独享账户的，自己不会充值可以联系我们专业团队（wx：abch891）
