深夜炸场！中国团队开源“数学之神”，88.9% 正确率碾压全球

luyuanhong

深夜炸场！中国团队开源“数学之神”，88.9% 正确率碾压全球，网友：奥数题从此变乐高？

原创  知了  程序员 AI 破局  2025 年 05 月 02 日 22:19  浙江

大家好，我知了，10 年+程序员，架构师，曾负责过千万用户的系统架构，目前在研究 AI 智能体和 AI 编程方向，欢迎感兴趣的朋友关注一起学习。

五一假期前一天，当大家还在盘算着去哪玩的时候，AI 圈又炸了！DeepSeek（深度求索）突然甩出一枚“王炸”—— DeepSeek-Prover-V2 ，一个专门攻克数学证明的 AI 模型，直接刷新全球纪录！

这玩意儿有多强？88.9% 的通过率，在高中数学竞赛级别的 MiniF2F 测试上碾压所有对手，甚至把地狱级难度的普特南数学竞赛（PutnamBench）49 道题给干趴下了！

要知道，之前的 SOTA（当前最优）模型只能解出 10 道，而没专门优化的 DeepSeek-R1 才勉强搞定 1 道。



“数学证明”这种人类都觉得头秃的东西，AI 凭啥这么猛？

答案就俩字——“拆题”！

DeepSeek-Prover-V2 的绝活，就是像乐高大师一样，把一道超难的数学题拆成一堆小积木块，再一块块拼回去。

它先用 DeepSeek-V3（DeepSeek 自家的超强基座模型）把问题“切碎”，生成一堆子目标，再用一个 7B 小模型挨个攻破这些小目标，最后用 671B 巨无霸统筹全局，把答案拼成完整证明。

这还没完！它还有个“双语学习”的骚操作——一边学人类“说人话”推理，一边学机器专属的 Lean4 代码写证明，确保逻辑既符合直觉，又严谨到能让计算机点头。

最离谱的是，7B 小模型居然自学了大模型不会的技能！

在普特南测试里，7B 版本用非 CoT（非思维链）模式解决了 13 道 671B 搞不定的题！团队一查，发现这小家伙在处理“有限基数”问题时，偷偷用了 Cardinal.toNat 和 Cardinal.natCast_inj 这些招数，而大模型压根没这操作……这算不算 AI 界的“青出于蓝”？



开源！全开源！

DeepSeek 这次是真·大气，671B 和 7B 双版本直接甩上 Hugging Face ，连配套的 ProverBench 数据集（325道高中到大学级别的数学题）也一起送了。有网友实测，7B 版本在 RTX4090 上就能跑，效果吊打一堆闭源大佬（比如 Grok-3 、Claude-3 ）。

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



网友炸锅：

●“奥数教练要失业了？”

● “这哪是 AI ，分明是数学系的菲尔兹奖外挂！”

●“R2 还没来，数学之神先到了？DeepSeek 这节奏……”

更可怕的是，它可能只是开始。

论文里提到，训练中模型曾“意外”推导出新的数学结构，比如张量-范畴同调理论。如果 AI 哪天能自主发现新公理，那离真正的 AGI（通用人工智能）还远吗？

最后手动 @DeepSeek ：R2 到底啥时候发？

好了今天的分享就到这里了，三连一下吧，你的鼓励是我继续分享的动力，感谢大家关注。

程序员 AI 破局