职贝云数AI新零售门户

标题: DeepSeek「五一礼包」来了!新开源模型数学推理才能大提升|附实测细节 [打印本页]

作者: 0qCf 时间: 昨天 19:48
标题: DeepSeek「五一礼包」来了!新开源模型数学推理才能大提升|附实测细节
赶在五一假期前夕，DeepSeek 给我们送出一份惊喜大礼。延续一向的开源节拍，DeepSeek 在 Hugging Face 正式发布 DeepSeek-Prover-V2，并同步上线模型卡及示例代码。此次共推出两个版本：
DeepSeek-Prover-V2-7B：基于上一代 V1.5 模型，支持最长 32K 上下文输入；
DeepSeek-Prover-V2-671B：在 DeepSeek-V3-Base 基础上训练，推理功能最强。

*核心贡献者 †在 DeepSeek-AI 实习时期完成的工作，扫描文末二维码，进社群获取残缺报告据官方论文披露，DeepSeek-Prover-V2 的训练核心是「递归+强化学习」的组合：即先由 DeepSeek-V3 拆解复杂定理，生成一系列子目的和推理思绪；再经过 GRPO 算法，从多种候选方案中自动学习如何选出最优解。
模型特别引入了两种互补的「解题风格」：

疾速形式（non-CoT）：专注于速度，像是一位纯熟工匠，直接生成精炼的 Lean 代码答案，不展现思索过程，合适处理大量标题。
逻辑形式（CoT）：更像一个耐烦的数学教师，会详细列出每一步推理过程，确保逻辑明晰、思绪透明。
训练过程分为两阶段，在第一阶段，研讨人员次要训练疾速形式，采用「专家迭代」方法：模型先尝试处理难题，成功的答案再作为新数据反哺模型，不断打磨本人的才能。

待疾速形式趋于波动后，研讨人员进入第二阶段，末尾训练更复杂的逻辑推理才能。他们将 DeepSeek-V3 的数学知识迁移到新模型中，并结合方式化数据，引入「冷启动」机制，构建起更复杂的推理途径。

(, 下载次数: 0)

为了进一步提升推理才能，研讨人员引入了 GRPO 的强化学习算法，不同于传统的 PPO，它直接在多个候选答案中比较优劣，引导模型自主学会选择最优解。

详细做法是：每次输入一个定理，系统会生成 32 个不同的证明方案，然后只保留被 Lean 验证系统断定为「正确」的答案（奖励 1 分，否则 0 分），这样模型就能在高质量反馈中不断退化。

在开发出功能弱小的 671B 模型后，DeepSeek 研讨团队又尝试把这些才能「蒸馏」到更小的 7B 模型中，而整个过程就像是徒弟教徒弟:

先用大模型生成解题过程，再教会小模型了解并复现；同时将小模型输入长度扩展至与大模型分歧，并阅历相反的强化训练。

这样，即便在资源有限的设备上，用户也能运用小体积模型获得接近大模型的数学推理才能，并根据需求选择疾速或详细解题风格。

(, 下载次数: 0)

整个体系中，DeepSeek-V3 担任拆解复杂定理，生成自然言语的推理草图，同步转译为 Lean 言语表示的一系列子目的，并生成「思绪链」作为中间引导。7B 模型再一步步完成子证明，最终拼接成残缺推理。这种「模糊思索 + 准确证明」的训练机制，有效提升了小模型的数学了解深度。
(, 下载次数: 0)
在最终功能评价中，DeepSeek-Prover-V2-671B 在 MiniF2F 测试中完成了 88.9% 的经过率，成功解出 PutnamBench 数据集中的 49 道难题。与此同时，DeepSeek 还同步推出了一个全新的数学方式化数据集 ProverBench，共包含 325 道成绩标题。涵盖：
AIME 竞赛题（15 题）
数论、代数、线性代数、微积分、实分析等多个方向
(, 下载次数: 0)
这一数据集不只包含真实的高中竞赛标题，还涵盖从基础代数、实变分析到概率论等多个本科阶段知识点，可以系统评价模型在不同数学范畴的推理才能。结果显示，在 15 道 AIME 竞赛题中，DeepSeek-Prover-V2 成功解出其中 6 道，而 DeepSeek-V3 运用多数投票方式（majority voting）则处理了 8 道。按照官方的说法，这组对比凸显出一个重要趋向：大型言语模型在「非正式数学推理」和「正式数学推理」之间的表现差距正在分明减少。
非正式数学推理：指模型像人类一样用自然言语思索、了解并解答数学题，比如我们日常说「这道题怎样算？」的方式。它更灵敏、不需求严厉的逻辑方式。
正式数学推理：指模型能用像 Lean 这样的方式言语，写出符合数学逻辑、可被验证器检验的严谨证明。它像数学论文中的证明，强调每一步推理都必须严厉准确。换句话说，过去模型更像是「会算但不会写出严谨证明」。而如今，在模型结构和训练策略不断演进下，言语模型也逐渐学会了写出规范、可验证的数学证明。此外，DeepSeek 宣布新模型的运用将遵照其公开答应证。🔗 https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/LICENSE-MODEL目前，Prover-V2 系列已可经过 Hugging Face 平台收费下载，并支持 Transformers 接口部署。Novita AI 是首批上线 Prover-V2-671B 推理服务的第三方提供商，我们也借此测试了一些成绩。
(, 下载次数: 0)
经典的「一根 5.5 米长的竹竿可以经过高 4 米宽 3 米的门吗？」很遗憾，结果它没答对。
(, 下载次数: 0)

对于这道笼统代数，它的回答不只正确，还能从基本定义出发，解释了什么是群同态、Z₁₂ 和 Z₄ 的含义，以及同态的运算规则，显然，这对于初学者很敌对。

(, 下载次数: 0)

从论文所泄漏的方向来看，DeepSeek-Prover-V2 给出的不只是数学答案，更指明了言语模型下一阶段的能够途径。

假如说过去我们关怀的是大模型「能说什么」，那么在 Prover-V2 身上，我们得需求关注它「能证明什么」。

数学只是切入口，推理才是 DeepSeek 这次真正下注的方向。

从生成内容迈向生成结构化逻辑，这条道路不够性感，也不容易讲故事，却能够最早触碰通用人工智能的底层结构。

毕竟，AI 可以不懂人之常情，但它必须学会推理，由于任何知识系统的边界，归根结底都是逻辑能否闭环、以及推理能否成立。
最后附上相关地址：1️⃣ DeepSeek-Prover-V2-7B HuggingFace 地址：
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B

2️⃣ DeepSeek-Prover-V2-671B HuggingFace 地址：
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

3️⃣ DeepSeek-ProverBench HuggingFace 地址：
https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

4️⃣ DeepSeek-Prover-V2 GitHub 地址：
https://github.com/deepseek-ai/DeepSeek-Prover-V2
文 | Prover
(, 下载次数: 0)
我们正在招募伙伴📮 简历投递邮箱hr@ifanr.com✉️ 邮件标题「姓名+岗位称号」（请随简历附上项目/作品或相关链接）更多岗位信息请点击这里🔗
(, 下载次数: 0)

欢迎光临职贝云数AI新零售门户 (https://www.taojin168.com/cloud/)