继 2 月论文“撞车”之后，梁文锋和杨植麟又在另一个大模型赛道上相遇了。4 月 30 日，DeepSeek 上线新模型 DeepSeek-Prover-V2，这是一个数学定理证明专用模型。Prover-V2 的参数规模进一步扩展到 671B（6710 亿规模参数），相较于前一代 V1.5 版本的 7B 规模增加了近百倍，这让其在数学测试集上的效率和正确率更高。
巧合的是，4 月中旬，月之暗面也曾推出一款用于形式化定理证明的大模型 Kimina-Prover，这是 Kimi 团队和 Numina 共同研发的大模型，该产品也开源了 1.5B 和 7B 参数的模型蒸馏版本。该模型的 miniF2F 测试通过率为 80.7%，PutnamBench 测试成绩为 10 道题。
两者相比较，在 miniF2F 测试通过率以及普特南测试上，DeepSeek-Prover-V2 的表现超过了 Kimina-Prover 预览版。值得注意的是，两家公司在技术报告中都提到了强化学习。比如 DeepSeek 的题目为《DeepSeek-Prover-V2：通过子目标分解的强化学习推进形式数学推理》，而月之暗面的题目为《Kimina-Prover Preview：基于强化学习技术的大型形式推理模型》。（凤凰网科技）
