DeepSeek-Prover-V2-671B 模型训练流程解析

摘要：DeepSeek 在节前发布的模型DeepSeek-Prover-V2-671B在数学定理证明方面实现了当前最优的性能，在MiniF2F-test上达到了88.9%的通过率，并解决了PutnamBench中658个问题中的49个；怀着对技术的好奇心，搬运工仔细

DeepSeek 在节前发布的模型DeepSeek-Prover-V2-671B在数学定理证明方面实现了当前最优的性能，在MiniF2F-test上达到了88.9%的通过率，并解决了PutnamBench中658个问题中的49个；怀着对技术的好奇心，搬运工仔细阅读了《DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition》这篇paper， DeepSeek-Prover-V2-671B 最大的亮点是结合了数学的形式化推理（在完备数学概念基础上，采用具有确定语义定义并有严格语法的语言表达的规范风格）和语言模型的CoT（非形式化推理）能力。

具体在 DeepSeek-Prover-V2-671B 上，非形式化推理：语言模型基于数学直觉利用CoT能力将一个复杂问题分解为多个步骤，形式化证明部分：模型将分解得到的子问，生成基于Lean4的形式化证明过程，结合两部分数据，在冷启动阶段进行 SFT 基础 DeepSeek-V3-671B模型，在SFT 之后，让模型进行GRPO 的强化训练，这样最终的模型不仅具备进行自然语言CoT思考，还能有效支持复杂的形式化推理任务。

具体模型演绎流程图如下：