主要观点总结
本文介绍了DeepSeek和月之暗面两家公司分别推出的大模型Prover-V2和Kimina-Prover，两家模型在数学测试集上的效率和正确率有所提升。但两家公司都面临着被追赶和超越的挑战。DeepSeek面临来自阿里巴巴和百度的竞争，而月之暗面则面临来自字节跳动的挑战。同时，市场上对两家公司的新模型充满了期待，但两家公司的领先地位能否保持尚不确定。
关键观点总结
关键观点1: DeepSeek推出Prover-V2模型，参数规模扩展至671B，提高了在数学测试集上的效率和正确率。
DeepSeek推出的Prover-V2模型在miniF2F测试通过率达到88.9%，解决了PutnamBench的49道题。该模型的技术报告强调了强化学习的应用。
关键观点2: 月之暗面推出Kimina-Prover模型，与DeepSeek竞争。
月之暗面推出了一款用于形式化定理证明的大模型Kimina-Prover，其miniF2F测试通过率为80.7%，PutnamBench测试成绩为10道题。两家公司在技术报告中都提到了强化学习。
关键观点3: 两家公司面临不同挑战，市场上期待其新模型发布。
DeepSeek面临阿里巴巴和百度的竞争压力，而月之暗面则面临来自字节跳动的挑战。市场上对两家公司的新模型充满了期待，包括R2模型和V4模型的上线。
关键观点4: 大模型领域竞争激烈，DeepSeek和月之暗面是否能保持领先地位尚不确定。
随着越来越多的大模型开源竞赛的参与者，DeepSeek和月之暗面作为初创公司能否保持领先地位尚不确定。市场上有许多传言和猜测关于两家公司的新模型，包括合作和竞争的可能性。
文章预览
摘要： 被追赶和超越，是创业者常面对的挑战。 来源｜中国企业家杂志 作者｜闫俊文 编辑｜张晓迪 继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测试通过
………………………………
