DeepSeek开源「Prover-V2」强推理模型！网友：算法大赛从没有这么简单过..

不二如是

2025 年 5 月 1 日，DeepSeek 开源了 Prover-V2 强推理模型。该模型专为「数学 AI 编程语言」Lean 4 打造，专注于形式化定理证明。

在线学习：



DeepSeek-Prover-V2 在定理证明赛道上实现了业内最佳性能，在 MiniF2F 测试中达到了 88.9% 的通过率，在 AIME 24、25 上也有不错的分数。

此次发布的两个版本的 DeepSeek-Prover-V2 模型，参数规模分别为 7B 和 671B，其中 DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基础上训练而成，而 DeepSeek-Prover-V2-7B 则基于 DeepSeek-Prover-V1.5-Base 构建，并支持最长 32K tokens 的上下文长度扩展。

DeepSeek-Prover-V2 的初始化数据通过一个由 DeepSeek-V3 驱动的递归定理证明流程收集而来。

在冷启动训练阶段，首先通过提示 DeepSeek-V3 将复杂问题分解成一系列可以解决的子目标，每解决一个子目标就会将这些证明整合成「思维链」，并融合 DeepSeek-V3 的逐步推理轨迹，共同构建出用于强化学习的初始训练数据。

该模型经历了两阶段训练，建立了两种互补的证明生成模式：高效非思维链（non-CoT）模式和高精度思维链（CoT）模式。

在训练过程中，遵循推理模型的通用目标，采用「对 / 错」二值反馈作为主要的奖励信号，最终得到的模型在神经定理证明任务中达到了当前最先进的性能。

DeepSeek 还发布了 ProverBench，这是一个包含 325 道题目的基准数据集，其中 15 道题来自最近两届 AIME 数学竞赛中的数论与代数题目，其余 310 道题则精选自教材示例和教学教程。

该数据集旨在支持对模型在高中竞赛题和本科数学题两个层面的综合评估。对于 DeepSeek-Prover-V2 的发布，网友评价十分积极，认为该模型强大且效果显著，甚至有钻研数学奥林匹克的学生表示对其印象深刻。

DeepSeek开源了Prover-V2强推理模型，网友惊呼奥数变简单了。

这个模型专为数学AI编程语言Lean 4打造，性能超牛，在MiniF2F测试中通过率高达88.9%，还能搞定AIME竞赛难题。

它通过递归定理证明流程收集数据，把复杂问题拆解成子目标，再整合成思维链，训练过程又巧妙又高效。网友们都超期待DeepSeek-R2，希望它能带来更多惊喜。

评论区聊聊你的想法吧

如果有收获，别忘了评分 ：

                               
登录/注册后可看大图

不二如是

感谢分享 朕又在鱼C学到东西啦！非常满意

不二如是

@FishC 了解“DeepSeek-Prover-V2”吗？

FishC

不二如是 发表于 2025-05-01 16:30
@FishC 了解“DeepSeek-Prover-V2”吗？

关于DeepSeek-Prover-V2  
您好！DeepSeek-Prover-V2 是深度求索（DeepSeek）团队开发的自动化定理证明工具，主要面向数学和逻辑问题的形式化验证。其核心特点包括：  

  
• 结合深度学习与符号推理，提升复杂定理的证明效率；  
• 支持交互式证明，允许用户逐步调整策略；  
• 适用于教育、研究及工业领域的逻辑验证场景。  
  

  

如需使用或了解更多细节，建议访问其官方资源：  
https://www.deepseek.com/  

若您有具体问题（如安装、代码示例等），可以补充说明，我会进一步解答！

以上回复来自 FishC AI 小助理，如未能正确解答您的问题，请继续追问。

lscp

感谢分享 朕又在鱼C学到东西啦！非常满意

不二如是

lscp 发表于 2025-5-1 22:45
感谢分享 朕又在鱼C学到东西啦！非常满意

鱼C有你更精彩

ydwb

感谢分享

不二如是

ydwb 发表于 2025-5-2 15:55
感谢分享

快速收敛

感谢分享 朕又在鱼C学到东西啦！非常满意

不二如是

快速收敛 发表于 2025-5-2 16:15
感谢分享 朕又在鱼C学到东西啦！非常满意

鱼C有你更精彩