昨天DeepSeek发布的DeepSeek-Prover-V2 模型已经有了介绍论文可下载：
github.com/deepseek-ai/DeepSeek-Prover-V2
deepseek研究员邵智宏也在x上介绍了该模型，并引发了前deepseek现在字跳工作的辛华剑评论。这个赛道上好像主要是中国厂商在卷。字跳、kimi、腾讯都有做过类似的模型，成绩都不错。
DeepSeek-Prover-V2 是一个开源的大型语言模型，旨在 Lean 4 中进行形式化定理证明，通过强化学习进行子目标分解，从而推进形式化数学推理 。
该模型使用 DeepSeek-V3 支持的递归定理证明流程收集的数据进行初始化 。冷启动训练过程首先提示 DeepSeek-V3 将复杂问题分解为一系列子目标 。已解决子目标的证明与 DeepSeek-V3 的逐步推理相结合，为强化学习创建了初始的“冷启动”。这个过程使得将非形式化和形式化数学推理整合到一个统一的模型中成为可能 。
由此产生的模型 DeepSeek-Prover-V2-671B 在神经定理证明方面取得了最先进的性能 。它在 MiniF2F-test 上达到了 88.9% 的通过率，并解决了 PutnamBench 中的 658 个问题中的 49 个 。
AI创造营
