梁文锋和杨植麟再“撞车”
以下文章来源于中国企业家杂志 ,作者闫俊文 中国企业家杂志 . 讲好企业家故事,弘扬企业家精神 本文来自微信公众号: 中国企业家杂志 (ID:iceo-com-cn) ,作者:闫俊文,编辑:张晓迪,题图来自: AI生成 继2月论文"撞车"之后,梁文锋和杨植麟又在另一个大模型赛道上相遇了。 4月30日,DeepSeek上线新模型DeepSeek-Prover-V2,这是一个数学定理证明专用模型。 Prover-V2的参数规模进一步扩展到671B (6710亿规模参数) ,相较于前一代V1.5版本的7B规模增加了近 百倍 ,这让其在数学测试集上的效率和正确率更高,比如,该模型的miniF2F测试通过率达到88.9%,它还 解决了PutnamBench (普特南测试) 的49道题。 巧合的是, 4月中旬,月之暗面也曾推出一款用于形式化定理证明的大模型Kimina-Prover ,这是Kimi团队 和Numina共同研发的大模型,该产品也开源了1.5B和7B参数的模型蒸馏版本。该模型的miniF2F测试通过率 为80.7%,PutnamBench测试成绩为10道题。 两者相比较,在miniF2F测试通过率以及普特南测 ...