最近,DeepSeek在毫无预告的情况下,就在Hugging Face平台上开源了最新大模型DeepSeek-Prover-V2,这是一款专门针对数学领域的大模型。
DeepSeek-Prover-V2一共有671B和7B两种参数,在超难数学评估测试MiniF2F中,671B通过率达到了88.9%,并且在PutnamBench的658个问题中解决49个,数学能力非常强。此外,还开源了一个高水准的数学评估集ProverBench。
DeepSeek-Prover-V2-671B是在DeepSeek-V3-Base的基础上进一步训练而成,而DeepSeek-Prover-V2-7B是在DeepSeek-Prover-V1.5-Base的基础上构建,并扩展了上下文长度,最大可达32K个标记。
DeepSeek-Prover-V2建立在DeepSeek-V3架构之上,因此许多配置与通用的DeepSeek-V3模型相似。它采用了混合专家(MoE,Mixture-of-Experts)的设计,具体来说,每层包含256个路由专家(routed experts)和1个共享专家(shared expert),每个专家的中间层大小(moe_intermediate_size)为2048,在处理每个输入符号(token)时会激活其中的8个专家。此外,该模型支持的最大上下文长度达到了163,840个token。
DeepSeek-Prover-V2构建了一个统一的数学推理框架,融合了非形式化和形式化数学推理。通过将复杂的数学问题分解为一系列子目标,并利用DeepSeek-V3的逐步推理能力,将非形式化的推理过程与形式化的证明过程相结合,从而实现了从问题分解到证明生成的无缝衔接。
为了生成冷启动数据,V2采用了一种递归定理证明管道。V3被用于将定理分解为高级别的证明草图,并同时在Lean4中形式化这些证明步骤,生成一系列子目标。随后,一个较小的7B模型被用于处理每个子目标的证明搜索,这种方式有效减轻了计算负担。当一个复杂问题的分解步骤被解决后,完整的逐步形式化证明与DeepSeek-V3的链式思考过程相结合,生成了冷启动推理数据。这些数据为模型的初始训练提供了重要的基础。
在冷启动数据的基础上,V2进行了强化学习阶段。筛选出那些7B证明模型无法端到端解决的难题,但这些难题的所有分解子目标都已成功解决。通过组合所有子目标的证明,构建出原始问题的完整形式化证明,并将其附加到V3的链式思考中,从而产生了非形式化推理与形式化证明的连贯合成。
在强化学习阶段,模型使用二元正确或错误反馈作为主要的奖励监督形式,进一步增强了其将非形式化推理与形式化证明构建相结合的能力。
DeepSeek开发了ProverBench基准测试数据集来评估模型的性能,该数据集包含325个问题,其中15个问题是从最近的AIME竞赛(AIME24和25)中的数论和代数问题形式化而来,提供了真实的高中竞赛水平挑战。其余的310个问题则来自精选的教科书示例和教育教程,涵盖了从高中到本科水平的多样化数学问题,包括数论、初等代数、线性代数、抽象代数、微积分、实分析、复分析、泛函分析、概率等多个领域,为模型的性能评估提供了丰富的测试场景。