[ai也算国新]deepseek在4月30日发布新模型prover-v2

DeepSeek-Prover-V2 是一个专门解决数学难题的超级AI，有俩版本，一个“巨无霸”(6710亿参数)，一个“轻量版”(70亿参数)。

巨无霸是当前开源数学AI里最大的，解题能力直接碾压以前的小模型。

它内部由256个路由专家组成，但每次解题只激活8个干活，耗能仅普通显卡的1.8倍。

其解题像人类一样拆步骤，遇到超难数学题，先拆成小问题，逐个解决再拼起来(比如先证明A，再证明B，最后合起来搞定大题)。也会边学边改，像考试后对答案，对了就奖励自己，错了就调整，越练越准。

而且， 不光算出结果，还能用Lean4等专业工具写出一步步的证明过程(类似数学老师批改时要求的严谨推导)，在奥数题测试中正确率近90%，比GPT-4的数学模块还高。

巨无霸模型压缩后能用普通显卡跑，还支持多种精度模式，穷学生用4块A100显卡就能每分钟解18道题。

---
对AI行业有啥贡献？

不仅能解奥数题(比如美国大学生数学竞赛题)，还意外发现了一个数学新理论(张量-范畴同调)，说明AI有潜力自己搞科研了。

推动通用人工智能(AGI)。它处理复杂逻辑的能力(比如拆解问题、分层推理)，给AI解决其他领域难题(比如物理公式、编程bug)打了个样。

训练成本只有GPT-4的1/20，调用价格是GPT-4的1%，穷实验室也玩得起。


省流：专攻数学领域的版本，目前该领域性能最佳，并且不是用算力堆性能，而是技术领域又有了突破。