dota 671b ai 深夜突袭，DeepSeek-Prover-V2加冕数学王者！671B数学推理逆天狂飙
dota 671b ai 深夜突袭，DeepSeek-Prover-V2加冕数学王者！671B数学推理逆天狂飙
就在刚刚，DeepSeek-Prover-V2正式发布。
此次DeepSeek-Prover-V2推出了两款不同规模的模型，分别是7B参数和671B参数的版本。
DeepSeek-Prover-V2-671B模型，在继承了DeepSeek-V3-Base的优良基因后，经过精心训练，其推理能力达到了顶尖水平。
DeepSeek-Prover-V2-7B模型，它是在DeepSeek-Prover-V1.5-Base的基础上进一步研发的，其特色在于将上下文处理能力提升，最大支持长度可达32Ktoken。
Hugging Face平台上的链接是：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B，该链接指向DeepSeek-AI团队开发的DeepSeek-Prover-V2模型，其规模达到6710亿参数。
GitHub平台上的项目链接为：https://github.com/deepseek-ai/DeepSeek-Prover-V2，访问该地址可进入DeepSeek-Prover-V2项目的具体目录。
同时，技术报告也放出了。
该论文可从以下链接获取：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf，其中详细介绍了DeepSeek-Prover-V2的相关内容。
昨日，DeepSeek在Hugging Face平台公开发布了671B模型dota 671b ai 深夜突袭，DeepSeek-Prover-V2加冕数学王者！671B数学推理逆天狂飙，不出所料，紧接着便有了后续动态。
数学证明大提升
本次DeepSeek-Prover-V2的训练重点，主要依赖于递归算法与强化学习技术的结合。
DeepSeek-V3能够将繁复的定理分解，进而形成一系列子目标和推理路径。紧接着dota 671b ai 深夜突袭，DeepSeek-Prover-V2加冕数学王者！671B数学推理逆天狂飙，GRPO算法将自动从众多备选方案中学习，以确定最佳解决方案。
网友们纷纷称赞这项技术，认为它将引领数字AI技术超越人类，从而极大地促进AI领域的研究进程。
方法可以总结如下：
· 优化算法，以实现更快、更智能的模型
· 揭示AI「黑盒」行为的洞见
· 设计更好的架构，无需无尽的试错
· 加速数据分析，以实现更快的突破
因此，这直接引领我们迈向通用人工智能，催生出超越人类智能的超级智能。在不久的将来，人工智能将创造出人类难以理解的高深数学理论。
DeepSeek-Prover-V2这款工具主要针对Lean 4编程语言中的形式化定理证明进行设计。
该数据初始化过程是通过DeepSeek-V3所引领的递归定理证明机制进行搜集的。
在冷启动训练阶段，系统将指导DeepSeek-V3将繁复问题细分为若干个子任务，接着将已解决的子任务的证明整合成思维链，并融合DeepSeek-V3的逐步推理能力，从而为强化学习提供了一次初始的冷启动。
经过这一过程，非正式的数学推理与正式的数学推理得以融合，共同构建成一个统一的模型。
总结来说，亮点如下。
· 生成冷启动推理数据：递归证明搜索方法
为了建立冷启动数据集，该团队设计了一套既简便又高效的递归定理证明步骤，并采用DeepSeek-V3作为核心工具，对子目标进行拆分及规范化处理。
DeepSeek-V3将收到指示，需将定理拆解成高级别的证明草稿。同时，在Lean 4环境中对这些证明步骤进行形式化处理，进而生成一系列子任务。
首先，我们采用一个较小的7B模型来对各个子目标的证明搜索进行操作，这样做有助于减轻计算压力。
一旦分解具有挑战性的问题的步骤被攻克，便将完整的逐步形式化证明与DeepSeek-V3所生成的对应思维链过程相融合，进而形成冷启动推理所需的数据。
· 基于合成冷启动数据的强化学习
团队经过严格筛选，选定了一个充满挑战性的问题子集——这些子问题无法被7B prover以整体方式攻克，然而，将它们拆分后，每一个子目标均已被顺利解决。
经过对各个子目标证明的汇总，该团队成功为原始问题搭建了一个全面的形式化证明结构。
随后，需将这份证据并入DeepSeek-V3的推理链条之中，该链条详细阐述了相关公理的分解过程，进而实现了非正式推理与后续形式化步骤的紧密融合。
对合成冷启动数据进行了prover模型的微调之后，该团队进入了强化学习阶段，旨在进一步强化模型将非正式推理与形式化证明构建能力相连接的能力。
依据推理模型的既定训练宗旨，主要运用二元式的正确与否反馈机制来实施奖励性监督。
最终，DeepSeek-Prover-V2-671B模型在神经定理证明领域取得了最佳表现，MiniF2F-test测试中通过了88.9%，并且成功解决了PutnamBench测试中的658个问题中的49个。
DeepSeek-Prover-V2在miniF2F数据集上生成的证明文件，可通过以下链接获取：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip。
针对AIME竞赛题目与教科书习题的标准化数据集ProverBench，
ProverBench是一个包含325道题目的基准数据集。
这15道题目均来自近期举办的AIME竞赛（AIME 24&25），涵盖了数论与代数领域的题目，它们是极具挑战性的，属于高中竞赛级别的题目。
这310道题目均选自精心挑选的教科书中的典型例题以及教学辅导材料，共同构成了一组丰富多样、富含教学价值的规范化数学题目库。
因此，这项基准更全面地评估高中竞赛和本科阶段的数学水平。
DeepSeek-Prover-V2
在论文研究中，该团队成功搭建了一个子目标分解的推理模型，并借助合成的初始数据和广泛应用的强化学习手段，显著增强了模型的表现力。
通过子目标分解实现递归式证明搜索
在数学领域，人们普遍采纳了一种有效的做法，即将繁复定理的证明步骤分解成若干个较为简单的引理，这些引理充当了连接前后证明环节的桥梁。
近期，神经定理证明领域广泛采纳了分层式策略。该方法的核心在于利用现代大型语言模型（LLM）在非形式化推理方面的优势，从而有效提高定理证明过程中的搜索效率。
本课程内容涵盖三个主要阶段：首先，从自然语言推理过渡至形式化证明的初步草图；其次，涉及子目标的递归求解方法；最后，专注于基于子目标的定理证明过程的学习。
在启动DeepSeek-V3的同时，生成一种自然语言表述的证明草图，并将这些草图转化为Lean语言中的定理表述，对于尚未得到证明的内容，则以“抱歉”作为占位符。
随后，7B证明模型被应用于对分解后的各个子目标进行递归求解。通过整合这些子目标的证明信息，研究团队得以构建起原始复杂问题的全面形式化证明。
冷启动数据收集流程概览
DeepSeek通过设定子目标，有效地拓宽了模型训练中可应用的形式化定理的范畴。
他们成功构建了两种不同类型的子目标定理，其中一种以前序子目标作为必要条件（参照图3(b)所示），而另一种则没有这样的前提条件（参照图3(a)所示）。
这两种子目标均被包含在专家迭代环节中，进而构建起一套逐步推进的课程体系，该体系旨在指导证明模型逐步学会应对精心挑选的难题。
该流程的核心理念与AlphaProof在测试阶段所采纳的强化学习方式相仿，即通过构建目标问题的不同版本，从而增强模型应对难度较高的IMO级别问题的解决能力。
将分解后的子目标转化为一系列引理（lemma）陈述
首先执行步骤 (a)：将原始目标状态替换为当前子目标。
在完成步骤 (b) 的过程中，需将先前设定的子目标视作基础，并将其纳入当前的引理之中。
类型(b)的陈述适用于通过递归方式解决繁复问题，同时，类型(a)和类型(b)的陈述均包含在课程学习的过程中，旨在培养模型逐步提升其推理技能。
最终，将此组合而成的正式证据附加至DeepSeek-V3最初构建的「思维链」之中，进而构建出高标准的冷启动训练资料，以助力形式化数学推理的习得。
统一非形式化推理与形式化证明
算法框架由两个阶段构成，这两个阶段分别依赖于两种相互补充的模型：一是DeepSeek-V3模型，它主要负责引理的分解工作；二是7B证明模型，该模型则专注于补充和完善形式化证明的具体细节。
此方法巧妙地将高水平的自然语言理解与低级的精确验证步骤相结合，从而为打造适用于训练的规范化推理数据集奠定了关键基石。
· 用合成数据实现冷启动
在研究过程中，DeepSeek挑选出一些特别难解决的问题。
这些问题相当复杂，即便是运用7B证明模型，也难以从始至终直接找到解决方案。
然而，有趣的是，一旦将这些难题分解为一系列的小目标，每个小目标都能得到有效的验证。这就像拼图游戏，将各个小目标的验证步骤依次排列组合，便能够构建出原始问题的全面证明，而这个证明过程既严谨又规范，是一种形式化的严谨证明。
随后，DeepSeek将这一完整的证明，并入到了由DeepSeek-V3所构建的「思维链」之中。
这里的“思维链”恰似解题过程中的草图，详尽地记录了将复杂问题拆解为若干小目标的具体步骤。
DeepSeek因此获得了这份独特的样本，其中既包含了类似日常思维的非正式推理过程，又融合了严格的形式化证明环节，二者相得益彰。
通过这种方式，团队成功收集到了几百条高质量的数据。
这些内容至关重要，构成了训练DeepSeek-Prover-V2模型的基础要素。
此方法之核心在于，将日常用语中所阐述的证明步骤，直接转变为具备逻辑结构的规范化框架。
· 用强化学习提升推理能力
通过使用冷启动合成数据对证明模型进行初步的优化调整，我们便顺利过渡到了强化学习的环节。
强化学习的目标在于使模型能够更有效地将日常语言的推理步骤转化为规范化的形式化论证。
在训练过程中，需遵循规范推理模型的训练规范，主要依赖“正确”与“错误”这两种基础反馈信号进行奖励监督。换言之，当模型输出的证明结果准确无误时，将获得奖励；反之，若证明结果存在偏差，则不予奖励。
然而，在训练过程中存在一个问题：模型所输出的证明结构，往往与“思维链”中分解问题的思路存在不一致之处。
为了应对这一挑战，训练初期，该团队便引入了一套全新的激励机制，该机制旨在对那些与分解结构不符的输出结果进行惩戒。
在实践训练中，该确保结构统一的方法展现出卓越成效，显著提升了证明的精确度。特别是在处理那些步骤繁复、结构复杂的定理证明时，其优势尤为突出。
训练细节
DeepSeek-Prover-V2的训练过程分为了两个阶段，并形成了两种相互补充的证明生成方式：
这两个生成模式在构思上沿袭了DeepSeek-Prover-V1.5的理念，只是在提示模板的设计上有所差异。
在第一阶段，团队依托课程学习框架与专家迭代策略，对non-CoT证明模型进行了训练，并且通过将子目标进行分解，实现了对复杂问题证明的递归合成。
non-CoT模式凭借其推理速度之快、验证成本之低，因而特别适宜于快速迭代过程以及数据搜集工作。
在第一阶段的基础上，第二阶段采纳了冷启动的思维链数据，这些数据融合了DeepSeek-V3所具备的高级数学推理功能以及构建的形式化证明。
CoT模式继而在强化学习阶段得以深化，旨在进一步增强模型在推理与形式化构建间的过渡能力。
专家迭代（Expert Iteration）
DeepSeek-Prover-V2的非CoT模型在训练过程中，采纳了“专家迭代”这一策略，该策略在现行的形式化定理证明系统训练中得到了普遍应用。
论文可在此链接查阅：https://arxiv.org/abs/2009.03393。
在每一轮的训练过程中，表现最为出色的模型将致力于攻克那些在前几轮未能得到有效验证的难题。
经过Lean系统的核实，这些成功的验证结果被纳入监督微调（SFT）的数据集，进而用于培育出更强大的后续模型。
这一过程不仅使模型持续吸收初始演示数据中的知识，而且能够总结出自己成功的推理方法，从而不断提升解决复杂问题的技巧。
DeepSeek-Prover-V2的训练过程与V1及V1.5版本保持同步，但在训练问题的分配上进行了两项优化：
监督微调（Supervised Fine-tuning）
该团队在DeepSeek-V3-Base-671B模型的基础上进行了细致的调整，将学习率设定为固定值5e-6，并确定了最大的上下文长度为16,384个token。
训练数据来自两个来源：
非CoT数据强化模型在Lean生态系统内展现出其形式验证的效能，与此同时，CoT数据模型则更侧重于将数学上的直观感受转化为系统化的形式化证明流程。
强化学习（Reinforcement Learning）
DeepSeek运用了Group Relative Policy Optimization这一强化学习算法。
GRPO无需独立的价值评估模型，它通过选取每题的多个备选证明，并依据相对奖励来实施策略的优化。
在训练过程中dota 671b ai，我们采纳了Lean这种二元奖励机制，若验证结果为成功，我们获得1分；若验证结果为失败，则不得分。
为确保训练成效显著，该团队细致筛选出既具挑战性又能够解决的题目，用作训练的指导。
在每一轮的训练过程中，我们会随机挑选出256道各不相同的题目，针对每一道题目，我们会生成32个可能的证明方案，同时，这些证明方案所包含的最大序列长度被设定为32,768个token。
蒸馏与小模型训练（Distillation）
团队提升了DeepSeek-Prover-V1.5-Base-7B的最大上下文处理能力，将其上限从4,096 token增至32,768 token，同时运用了在671B模型强化学习过程中收集的rollout数据对模型进行了细致的调整。
在CoT模式之外，团队进一步融入了专家在迭代过程中收集的非CoT数据。这一举措旨在使小型模型拥有更低的成本证明能力，并能够迅速提供简洁的形式化结论。
此外，该团队还对7B小规模模型实施了与671B大模型一致的强化学习步骤。
实验结果
MiniF2F基准测试结果
MiniF2F项目内含488道形式化的习题，这些题目源自AIME、AMC和IMO等知名竞赛，还包含了MATH数据集的内容，全面覆盖了初等数学的各个核心领域，例如代数、数论以及归纳法等。
这些题目被划分成两个同等规模的子集，分别是miniF2F-valid和miniF2F-test，每个子集均包含244道题目，且在各个学科领域中的分布情况保持一致。
如表格一所示，实验数据表明，DeepSeek-Prover-V2-671B在miniF2F-test测试基准上实现了最先进的性能表现；在运用CoT生成策略的情况下，仅需32个样本便实现了高达82.4%的准确率，这一成果是前所未有的。
值得注意的是，即便参数效率更胜一筹的DeepSeek-Prover-V2-7B也显现出了显著的竞争力，其表现已超越了现有文献中提及的所有开源定理证明工具。
他们还观察到一条显著的趋势：当样本预算从1增至8192时，7B与671B模型间的性能差异显著增强；规模更大的模型在样本利用率和性能提升速度方面均表现出更为优越的表现。
· 子目标引导的课程学习在难题证明中的应用
表2详尽地呈现了DeepSeek-Prover-V2在miniF2F基准测试中的解题表现，它在验证集上实现了91.0%的高通过率，而在测试集上则达到了88.9%的通过率。
值得关注的是，该团队设计了一套以子目标为导向的课程学习架构，其中将通用的DeepSeek-V3模型与轻量级的专用7B prover相融合，在miniF2F-valid测试集上达到了90.2%的准确率，其性能与DeepSeekProver-V2-671B几乎相当。
这些研究成果揭示了，当前最先进的通用大型语言模型不仅具备出色的自然语言处理能力，而且能够高效地协助完成各种复杂的形式推理作业。
借助精妙的子目标拆分技巧，模型能够将复杂问题细化为多个易于处理的环节，进而成功实现非正式推理与规范化证明之间的有效衔接。
· CoT vs. non-CoT
表1中的实验数据揭示了，在形式化的数学推理论证过程中，采用CoT推理模式的效率相较于non-CoT模式有着明显的提升。
这一发现进一步印证了CoT提示的实用性，该提示倡导将复杂问题拆解为若干中间环节，同时亦证明了在形式化定理证明领域中，推理过程中的扩展方法依然保持着其适用性。
此外，表3详细展示了DeepSeek-Prover-V2在各类推理情境下所产生token数量的具体统计数据。
正如人们所预料，CoT模式输出的内容显著更长，这体现了其繁复的推理步骤。
有趣的是，在non-CoT的配置中，671B模型所产出的平均输出长度相较于7B模型，明显要长。
深入的分析进一步揭示，即便在non-CoT模式中缺乏直接的推理提示，但较大的模型往往会在其证明代码中加入简短的自然语言注释，此类注释与隐含的推理步骤相仿。
这暗示着，即便缺乏明确的CoT提示，高容量模型依旧可能在内部及外部层面，通过隐性的方式完成中间推理的过程。
本科水平基准测试结果
· ProofNet
ProofNet中收录了371个题目，它们均以Lean 3语言编写而成。这些题目源自多个广受欢迎的本科纯数学教材，内容涉及实分析、复分析、线性代数、抽象代数以及拓扑等多个领域。
表4的数据表明，与未使用CoT的配置相比，在应用CoT推理方法后，DeepSeek-Prover-V2的通过率明显增加。
尽管其训练数据主要集中于高中数学领域，然而，该模型在处理更为复杂的大学数学问题时，却展现出了卓越的推广能力，这充分体现了其强大的形式化推理实力。
· PutnamBench
普特南Bench基准测试集涵盖了从1962年到2023年期间普特南数学竞赛所出现的各类数学题目。
该竞赛在美国和加拿大享有极高的声誉，每年举行，面向本科生，内容广泛，包括分析学、线性代数、抽象代数、组合数学、概率论以及集合论等多个大学数学分支的知识点。
如表4所展示，DeepSeek-Prover-V2-671B在PutnamBench测试中表现出更为强大的推理水平，成功解答了49个问题，且其表现明显超越了其non-CoT版本。
这表明，CoT推理技术已经能够高效解决那些极具挑战性的高等数学难题。
·RL实现的技能发现：7B胜过671B！
此外，团队还意外地观察到：在PutnamBench数据集上，当DeepSeek-Prover-V2-7B采用non-CoT生成模式进行操作时，其性能同样表现出色。
更令人惊叹的是，即便是一个规模较小的7B模型，也成功攻克了DeepSeek-Prover-V2-671B未能解决的13道难题！
这是为什么？
仔细分析模型的输出后，团队从中发现了一种独特的推理模式——
7B模型在处理与有限基数相关的问题时，频繁地运用Cardinal.toNat以及Cardinal.natCast_inj这两个函数，然而，671B模型所输出的结果中并未展现出这种处理手段。
似乎是这种技术使得7B能够高效地处理那些对基数值操作要求精细的问题。
组合问题测试结果
CombiBench构成了一个全面的基准测试库，它汇集了100道以Lean 4进行形式化表述的组合竞赛题目，并附有详细的自然语言说明。
团队选择了带有解决方案的配置，在此情况下，准确的答案已融入Lean的代码之中，这使得评估工作可以完全聚焦于生成证明过程。
对其中77道题进行评估后，模型成功解决了12道。
研究结果显示，尽管该模型主要在数论与代数范畴接受了训练，它却在组合学的挑战中表现出了出色的推广能力，即便这些组合问题相当复杂。
ProverBench数据集
为了提升既有的基准水平，该团队精心打造了一个由325道题目组成的基准数据集。
这些题目中，有15道源自AIME 24和25竞赛中的数论与代数难题，它们属于极具挑战性的高中级别竞赛题目；而其余的310道题目，则均选自精心挑选的教科书实例及教学辅导材料。
这就能更全面评估高中竞赛和本科阶段的数学水平。
· AIME题目形式化
美国数学邀请赛AIME的24和25届赛事中的题目，已经成为衡量大型语言模型推理能力的重要标准。
为了缩小模型在形式化与非形式化数学推理能力评估方面的差距，我们对AIME 24&25中的若干题目进行了整理和形式化处理，同时去除了涉及几何、组合与计数的内容，这些内容在Lean中的表述相对繁复。
最终，该团队筛选出了15个题目，这些题目不仅包括了初等数论，还涉猎了代数领域，且均属于竞赛级别的知识点。
结果显示，DeepSeek-V3-0324在15道题目中，成功解答了其中的8道。
在已知正确答案的情况下，DeepSeek-Prover-V2-671B能够为15道题目中的6道成功创建出有效的形式化证明。
这种趋势显示出，非形式化的数学推理论证与形式化的定理证明之间的性能差异正逐步减小dota 671b ai，而高级语言模型在语言解析以及形式逻辑的严密性方面，正逐渐逼近。
· 教科书题目形式化
除了AIME 24和25之外，该团队还精选了高中竞赛题目以及本科课程教材中的习题，以此丰富基准测试集的内容。
最终，他们完成了对310道题目的形式化处理，这些题目难度跨度较大，从竞赛级别的初等数学问题，到本科阶段常见的高级数学主题，均有所涵盖。
如表6所展示，研究结果显示，运用CoT推理的DeepSeek-Prover-V2-671B模型在各项对比中始终超越了所有基准模型dota 671b ai，其表现与在其它基准测试中观察到的结果保持一致。
在论文的结尾部分，该团队明确提出，他们计划在未来的研究中，致力于将现有范例推广至与AlphaProof系统相仿的其他系统之中。
我们的最终目的是攻克那些代表着自动定理证明领域最尖端水平的IMO级别数学难题！
快速开始
我们可直接运用Hugging Face的Transformers库来执行模型推断操作。
以下是一个展示如何在miniF2F数据集中生成问题证明的简易案例：
参考资料：
DeepSeek-Prover-V2项目位于GitHub平台，具体路径为https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main。
