刚刚！DeepSeek-Prover-V2 技术细节公布，附论文
仅用于站内搜索，没有排版格式，具体信息请跳转上方微信公众号内链接
大家好，我是Ai学习的老章
刚刚，DeepSeek开源新模型Prover-V2-671B
DeepSeek一贯的作风，先敲不作声放出模型文件，随后才公布技术细节。
1小时前，DeepSeek在其GitHub账号放出了部分技术文档和论文📑
DeepSeek-Prover-V2是一个开源的大型语言模型，专为Lean4形式化定理证明而设计。该模型的初始化数据是通过DeepSeek-V3驱动的递归定理证明流程收集而来。其冷启动训练过程始于提示DeepSeek-V3将复杂问题分解为一系列子目标。已解决子目标的证明被合成为思维链过程，结合DeepSeek-V3的逐步推理，为强化学习创建初始冷启动。这一过程使我们能够将非形式化和形式化数学推理整合到一个统一的模型中。
DeepSeek-Prover-V2正是为了应对这一挑战而生，其核心创新在于：
结合非形式化与形式化推理：利用强大的基础模型(DeepSeek-V3)进行初始的非形式化推理（如生成证明思路、分解问题），然后将其与严谨的形式化证明步骤相结合。
强化学习优化：通过强化学习，特别是利用子目标分解的策略，进一步提升模型在形式化证明构建中的能力。
DeepSeek-Prover-V2的训练过程独具特色，主要包含两个阶段：
a)冷启动数据合成(SynthesizeCold-StartReasoningData)
递归证明流水线：团队开发了一个简洁有效的递归定理证明流水线。首先，利用DeepSeek-V3将复杂的定理分解为高级别的证明草图（ProofSketches）和一系列子目标（Subgoals）。
子目标证明：为了降低计算成本，使用一个较小的7B参数模型来处理每个子目标的证明搜索。
数据合成：当一个复杂问题的所有子目标都被解决后，将完整的、逐步的形式化证明（由子目标证明组合而成）与DeepSeek-V3生成的相应思维链（Chain-of-Thought,CoT，包含高级证明思路和引理分解）配对，形成用于模型初始训练的“冷启动”推理数据。这一过程巧妙地将非形式化的解题思路与形式化的证明步骤融为一体。
b)基于合成数据的强化学习(ReinforcementLearningwithSyntheticCold-StartData)
筛选挑战性问题：选取一部分对于7B模型来说端到端无法解决、但其所有分解子目标都已被成功证明的难题。
数据增强：将这些难题的完整形式化证明（由子目标证明拼接而成）附加到DeepSeek-V3对应的CoT后面，生成更丰富的训练数据。
强化学习微调：在冷启动数据上进行初步微调后，采用强化学习进一步优化模型。奖励信号主要采用二元反馈（证明正确或错误），目标是增强模型连接非形式化推理和形式化证明构建的能力。
DeepSeek-Prover-V2发布了两个尺寸的模型：
DeepSeek-Prover-V2-7B:基于DeepSeek-Prover-V1.5-Base构建，上下文长度扩展至32Ktokens。
DeepSeek-Prover-V2-671B:基于DeepSeek-V3-Base训练。
性能方面，DeepSeek-Prover-V2-671B表现出色，达到了当前神经定理证明领域的SOTA(State-of-the-Art)水平：
在MiniF2F-test数据集上达到88.9%的通过率。
解决了PutnamBench数据集中658个问题中的49个。
团队还公开了模型在miniF2F数据集上生成的证明，可供下载研究：minif2f-solutions.zip[1]
模型文件：https ://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
为了更全面地评估模型在不同难度数学问题上的能力，团队还推出了ProverBench基准测试集，包含325个问题：
15个AIME问题：来自近两年的美国数学邀请赛(AIME24,25)的数论和代数题目，代表了真实的高中竞赛水平挑战。
310个教科书/教程问题：来自精选的教科书案例和教育教程，提供了多样化且具有教学意义的形式化数学问题。
ProverBench旨在覆盖从高中竞赛到本科水平的数学问题，为形式化推理模型的评估提供了更丰富的视角。
ProverBench数据集地址：https ://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench[2]
用户可以直接通过HuggingFace的transformers库来使用DeepSeek-Prover-V2进行推理。
模型下载：
7B模型：https ://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B[3]
671B模型：https ://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B[4]
架构说明：DeepSeek-Prover-V2-671B与DeepSeek-V3共享相同架构，详细信息可参考HuggingFace上的DeepSeek-V3文档[5]。
制作不易，如果这篇文章觉得对你有用，可否点个关注。给我个三连击：点赞、转发和在看。若可以再给我加个🌟，谢谢你看我的文章，我们下篇再见！
搭建完美的写作环境：工具篇（12章）图解机器学习-中文版（72张PNG）ChatGPT、大模型系列研究报告（50个PDF）108页PDF小册子：搭建机器学习开发环境及Python基础116页PDF小册子：机器学习中的概率论、统计学、线性代数史上最全！371张速查表，涵盖AI、ChatGPT、Python、R、深度学习、机器学习等
参考资料
