全球首个，最接近原版DeepSeek开源复现来了！R1四个月狂飙26倍
【导读】近日，来自SGLang、英伟达等机构的联合团队发了一篇万字技术报告：短短4个月，他们就让DeepSeek-R1在H100上的性能提升了26倍，吞吐量已非常接近DeepSeek官博数据！
DeepSeek的含金量还在上升。
就在最近，Hugging Face联创、首席科学家Thomas Wolf表示——
DeepSeek的出现，是开源AI领域的ChatGPT时刻！
用他的话说，「正如ChatGPT让全世界认识到AI的存在，DeepSeek则让全世界意识到，原来还有着这样一个充满活力的开源社区。」
DeepSeek-R1的性能已经媲美甚至超越美国最顶尖的闭源AI模型，对于全球AI圈来说，这件事的意义都极其深远。
与此同时，来自SGLang、英伟达等机构的数十人联合团队，也在DeepSeek上整了个大活。
在短短4个月内，他们利用最新的SGLang推理优化，直接让DeepSeek-R1在H100上的性能提升了26倍！
这是怎么做到的？
团队发布了长篇博文，详细展示了这一过程。
文章地址：https://lmsys.org/blog/2025-05-05-large-scale-ep/
在96块H100 GPU上优化部署DeepSeek
要知道，DeepSeek模型因为庞大的参数，以及多头潜注意力（MLA）和专家混合机制（MoE）等独特架构，如果想要大规模部署，就必须使用更先进的系统。
为此，团队先是对SGLang进行了全面升级，完整支持了PD分离、大规模EP、DeepEP、DeepGEMM及EPLB等功能。
然后凭借这些新特性，成功地在12个节点共96块GPU的集群上，复现了DeepSeek的推理系统。
最终，在处理2000个token的输入序列时，实现了每个节点每秒52.3k输入token和22.3k输出token的吞吐量。
方案运行在Atlas Cloud的12个节点上，每个节点均配备8块H100 GPU
团队表示，这应该是首个吞吐量接近DeepSeek官方数据的开源实现。
在本地环境下部署此方案，成本可降至0.20美元/1M输出token，约为DeepSeek Chat API官方定价的五分之一。
相较于使用相同资源的原始张量并行策略，此优化方案可将输出吞吐量提升高达5倍。
接下来，团队深入探讨了他们的并行设计、优化方法以及最终成果。
并行设计
高效的并行化设计，对于控制DeepSeek架构的计算复杂度和内存需求至关重要。
针对以下关键组件，团队都给出了优化方案：注意力层、稠密前馈网络（FFN)、稀疏FFN以及语言模型（LM）的头部。
每个组件都采用了专门设计的并行化策略，以提升可扩展性、内存效率和整体性能。
注意力层
DeepSeek采用了多头潜注意力机制（MLA)，从而能够有效地对输入序列中的复杂依赖关系进行建模。
为了优化这一机制，团队实现了DP attention，这是一种数据并行策略，目的是消除跨设备的KV缓存冗余，从而显著降低内存开销。
在SGLang v0.4版本中引入的该方法，现已扩展至支持混合数据并行和张量并行，为高效处理小批量数据提供了更大的灵活性。
稠密FFN
即便DeepSeek-V3仅使用了三个稠密FFN层，其计算过程仍然可能显著增加峰值内存占用，若不加以谨慎管理，极易导致系统崩溃。
为了解决这个问题，团队选择采用数据并行（DP）策略，而非张量并行（TP)，主要是考虑到DP的以下优势。
· 更强的可扩展性
当中间层维度为18,432时，较高的TP度（例如TP32）会导致数据被低效地分割成小单元片段（例如576个单元），而这些单元无法被128整除。
128，就是现代GPU（如H100）常见的对齐边界。
这种未对齐的情况，会严重阻碍计算效率和内存利用率。
相比之下，DP能够避免数据碎片化，从而提供更具可扩展性的解决方案，确保跨设备的工作负载均衡分配。
· 优化的内存效率
传统观念认为，TP可以随着worker size的增加而降低内存使用量，但这种优势在DP attention的应用场景下会逐渐减弱。
在纯TP设置中，单层Transformer模型的内存需求与DP size的关系如下：
其中，是每个设备（DP rank）上隐藏状态的大小，是模型参数的数量，k是一个系数，表示来自CUDA Graph复制的额外内存开销。
通过假设DP=TP，当时，此内存的使用函数达到最小值。
DeepSeek-V3使用18,432的中间大小。在prefill阶段，CUDA Graph通常被禁用，因此k=0。
但是，每个设备的token大小很容易超过2,048，导致最佳TP大小为3或更小。
在解码阶段，一个实际的配置可能使用每个设备128个token，并设置k=3。在这种情况下，内存最佳的TP大小为6。
在这两个阶段，较低的TP度可以最大限度地减少每个设备的内存使用量。
因此，与仅依赖TP相比，DP可以提供更节省内存的扩展方法。
·最小化的通信开销
在纯TP模式下，每个FFN层都需要执行两次all-reduce操作，从而导致巨大的通信开销。
通过采用DP策略，团队将该过程优化为：在先前的attention层之后执行一次reduce-scatter操作，并在下一个attention层之前执行一次all-gather操作，从而将通信成本降低50%。
更进一步，如果attention计算也采用纯DP模式，那么设备间的通信将被完全消除，进而显著提升整体效率。
DP稠密FFN与DP attention的集成方案如下图左侧所示。用户可以通过设置--moe-dense-tp-size=1来启用。
稀疏FFN
在DeepSeek-V3的MoE架构中，稀疏FFN需要处理大量的专家权重，进而造成显著的内存瓶颈。
为了缓解这一问题，团队采用了专家并行（EP）策略，将专家权重分散到多个设备上。
这种方法能够有效地扩展内存容量，不过，它在维持高性能的同时，也带来了一些新的挑战，比如不规则的全互联通信以及工作负载不均衡等。
团队利用DeepEP框架实现的EP方案
LM头
LM头（LM Head）负责计算大型词汇表上的输出概率，这是一项资源稠密型的操作，传统方案是采用词汇表并行技术，从TP组中聚合token logits。
为了进一步提升可扩展性和效率，团队采用了数据并行（DP）策略，与处理稠密FFN的方法保持一致。
这种做法不仅可以降低内存开销，还能简化跨设备的通信过程，从而提供了更加精简的解决方案。
预填充和解码分离
LLM的推理过程主要包含两个不同的阶段：预填充（prefill）和解码（decode)。
预填充阶段属于计算密集型，需要处理完整的输入序列；而解码阶段则属于内存密集型，主要负责管理用于生成token的KV缓存。
传统方案通常在一个统一的引擎中处理这两个阶段，然而，这种预填充和解码batch的混合调度方式会引入效率问题。
为了解决这些挑战，团队在SGLang中引入了预填充和解码（PD）分离技术。
如下图所示，SGLang会通过预填充服务器和解码服务器的协同工作，实现两个阶段的交错执行。
接收到输入请求后，系统的工作流程如下：
预填充服务器和解码服务器通过握手配对，各自作为本地发送者和接收者。
解码服务器预先分配KV缓存，并通知预填充服务器启动模型前向传递，计算KV缓存。
完成计算后，数据将被传输至解码服务器，由该服务器负责进行迭代式的token生成。
这种分离机制确保了每个阶段都能在最佳状态下运行，从而最大限度地利用GPU资源。
并且，为了进一步提升性能，团队的实现方案还包含以下特性。
非阻塞传输：数据发送和接收操作在后台线程中执行，从而保证调度器的事件循环不会被中断。
基于RDMA的传输：远程直接内存访问（RDMA）技术利用队列对（Queue Pairs）进行连接管理，并利用分散-聚集元素（Scatter-Gather Elements, SGE）实现非连续内存块的高效传输。
灵活的API集成：SGLang提供了高度可定制的API，能够与Mooncake和NIXL等高性能RDMA库无缝集成，从而简化了数据传输流程。
大规模专家并行性
基于DeepEP的专家并行
由DeepSeek团队开发的DeepEP提供了一系列优化过的通信内核，可以有效降低延迟并提升吞吐量，高效地将token路由到多个GPU上。
DeepEP有两种专门设计的调度模式，以满足不同的工作负载需求。
标准调度模式（Normal Dispatch）：主要针对处理较长的输入序列进行优化，例如预填充阶段，其首要目标是最大化计算吞吐量。 但会生成与CUDA Graph不兼容的符号形状，从而降低其在解码阶段的效率，因为在解码阶段，内核启动开销会成为一个显著的瓶颈。
低延迟调度模式（Low-Latency Dispatch）：专门为解码阶段生成输出token而设计，其核心目标是最小化延迟，从而确保实时性能。尽管它支持CUDA Graph，但需要预先分配固定大小的内存。如果实际内存需求超过了预分配的容量，则会触发运行时错误。
在SGLang中，DeepEP的集成提供了一种自动模式，能够根据当前的工作负载，动态地在上述两种调度模式之间进行选择。
与此同时，通过利用PD分离技术，使得在DP attention机制下，预填充阶段能够采用标准调度模式（Normal Dispatch)，而解码阶段则能够采用低延迟调度模式（Low-Latency Dispatch)。
这种集成方式能够根据每个阶段的具体需求来调整调度模式，从而优化资源利用率，并提升整体性能。
DeepGEMM集成
由DeepSeek团队开发的DeepGEMM，则被用于优化MoE模型中的计算过程。
DeepGEMM提供了两个经过专门设计的函数，用于处理与MoE相关的矩阵乘法运算（分组GEMM），每个函数都针对推理过程的不同阶段进行了定制。
分组GEMM（连续布局）：这种内核专门为动态输入形状而设计，使其成为MoE推理预填充阶段的理想选择。 它可以处理来自不同专家的输入数据，这些数据以连续的方式连接在一起，从而灵活地处理各种输入尺寸的变化。
分组GEMM（掩码布局）：这种内核假定输入形状是固定的，并使用掩码张量来仅计算输入的有效部分。 由于它与CUDA Graph兼容（可优化内核启动过程），因此特别适合于需要显著降低开销的解码阶段。
DeepGEMM与DeepEP的调度模式可以实现无缝集成：
对于与预填充阶段的标准调度模式配合使用的连续布局内核，需要执行一个额外的步骤。团队参考了LightLLM项目，并实现了一个自定义的Triton内核来实现高效的置换。确保了从标准调度模式输出的数据能够被正确地重新排列，从而实现与连续GEMM内核的平滑集成。
掩码布局内核与DeepEP的低延迟调度模式能够实现无缝对接，因为两者都针对解码阶段进行了专门优化，并且都支持CUDA Graph。
SGLang集成了DeepGEMM，用于在张量并行模式下进行MoE计算。通过在SGLang中设置环境变量SGL_ENABLE_JIT_DEEPGEMM为1，即可激活该内核，从而为非MoE操作提供更高的计算效率。
双batch重叠
在多节点环境下，有限的通信带宽可能会显著增加整体延迟。
为了应对这一挑战，团队遵循DeepSeek的系统设计理念，实现了双batch重叠（TBO）技术。
TBO将单个batch拆分为两个micro-batch，从而允许计算和通信过程相互重叠，同时，通过将有效batch大小减半，也降低了峰值内存的使用量。
为了创建更易于维护和重用的代码库，团队采用了一个由操作和yield点构成的抽象层。
这种方法可以让用户像处理单个micro-batch一样编写代码，同时通过策略性地插入yield点来暂停执行，从而允许其他micro-batch继续进行。
如此一来，不仅消除了代码重复，减少了对变量后缀的需求，并且还能有效地管理某些执行在层末尾完成而其他执行尚未完成的情况。
此外，抽象层还能轻松地适应不同的重叠区域选择，或者未来的增强功能，例如三batch重叠，而只需要进行极少的代码修改。
operations = [
self._forward_attn,YieldOperation(),# Pause execution for other micro-batchesself._forward_dispatch,self._forward_mlp,YieldOperation(),# Another pause pointself._forward_combine,]# Process a single micro-batch without duplicating codedef _forward_attn(self, state):state.hidden_states = self.self_attn(state.hidden_states, ...)
团队优化了预填充阶段的启动顺序，以避免通过DeepEP中的调度操作阻塞CPU，即使用的是其异步模式。
具体来说：
在GPU从其他rank接收到元数据，从而能够正确分配大小合适的张量之前，调度操作会阻塞CPU。
不正确的实施方式会导致在此期间计算流处于空闲状态，因为没有计算任务被提交给GPU。
为了实现优化，团队优先将计算任务提交给GPU，然后再启动可能导致CPU阻塞的通信操作。这样可以确保GPU在通信期间保持活跃状态。
如下图所示，通过采用正确的启动顺序，TBO可以避免由CPU阻塞操作引起的性能瓶颈。
专家并行负载均衡器
为了解决由专家并行（EP）引起的各个GPU工作负载分布不均匀的问题，DeepSeek开发了专家并行负载均衡器（Expert Parallelism Load Balancer, EPLB)。
EPLB以专家分布的统计信息作为输入，计算出专家的最佳排列方式，从而最大限度地减少不平衡现象。
用户可以分配冗余专家（例如，增加32个专家），这些冗余专家与原有的256个专家组合在一起，形成一个包含288个专家的资源池。
借助这个资源池，EPLB能够策略性地放置或复制专家——例如，多次复制最常用的专家，或者将使用频率适中的专家与在单个GPU上很少使用的专家组合在一起。
除了平衡工作负载之外，EPLB还在并行设计方面提供了更大的灵活性。如果使用最初的256个专家，并行规模只能被限制为2的幂次方。而EPLB通过使用288个专家，能够实现更多样化的配置，例如将并行规模设置为12或72。
在下图中，团队展示了系统规模和EPLB算法对不平衡问题的影响。
他们将GPU的平衡度，定义为GPU中MoE层的平均计算时间与最大计算时间之比，并使用GPU处理的token数量来估计其计算时间。
从图中可以看出，当系统随着节点数量的增加而扩展时，GPU的利用率会降低，而启用EPLB则可以显著提高了GPU的利用率。
EPLB在实际服务中的应用
为了使EPLB能够有效发挥作用，输入数据的分布必须与实际服务的工作负载高度吻合。通过以下两种策略，可以增强这种吻合度：
增加batch大小：更大的batch可以减少专家使用过程中的随机波动，从而提高负载均衡的效果。这一目标可以通过扩展集群规模或者采用多token预测（MTP）等技术来实现。
定期进行重新平衡：定期更新专家的排列方式可以利用时间局部性原理，但这需要高效地重新加载专家模型。因此，需要尽可能降低专家模型重新加载操作的成本。
即使采用了EPLB，一定程度的不平衡现象仍然难以避免，未来仍需进一步优化。
重新平衡的具体实施方案
SGLang通过三个阶段的重新平衡操作，来确保既高效又不会造成中断，进而在权重更新期间维持系统的性能。
系统加载阶段：可以选择从磁盘预加载权重数据到主内存中，以加快重新平衡的速度；也可以选择将权重数据保存在磁盘上，并使用内存映射（memory mapping, mmap）技术，从而减少内存的占用量。
重新平衡准备阶段：所需的权重数据会在后台异步传输到设备内存中，利用空闲的DMA硬件引擎，从而避免中断正在进行的GPU操作。
重新平衡执行阶段：通过设备到设备的数据复制来更新权重数据。还可以通过物理内存重绑定等技术来进一步优化这一步骤。
评估
为了突出使用的先进优化技术带来的吞吐量提升，团队使用DeepSeek-V3模型，在一个包含12个节点的集群上，对 SGLang 的不同配置进行了端到端性能评估。
他们比较了以下四种不同的配置：
SGLang（采用TP16x6）
SGLang（采用PD分离）
SGLang（采用PD分离和模拟MTP）
DeepSeek的结果
为了适应不同的工作负载需求，团队分别独立地评估了预填充阶段和解码阶段的性能。
评估结果总结如下：
· 预填充阶段：在4个节点的配置下，对于prompt长度分别为1K、2K和4K的情况，系统所实现的单节点吞吐量分别为每秒57,674、54,543和50,302个token。
如下图所示，与TP16基线相比，这种配置实现了高达3.3倍的性能提升。
在假设工作负载完全平衡的前提下，此系统的吞吐量与DeepSeek官方数据之间的差距在5.6%以内。
· 解码阶段：在9个节点的配置下进行评估，对于2K的输入，系统实现的单节点吞吐量为22,282个token/秒，这意味着与TP16基线相比，性能提升了5.2倍。
在模拟MTP条件下，对于4K的输入，系统仍然能够保持每节点17,373个token/秒的高吞吐量，仅比DeepSeek官方性能分析数据低6.6%。
接着，团队将SGLang的性能与DeepSeek的推理系统进行对比，力求使实验设置尽可能贴近DeepSeek的生产环境。
对于预填充阶段，团队测试了一个场景，在该场景中，每个设备处理16,384个token，输入长度为4,096。
考虑到DeepSeek的专家分布存在不确定性，他们评估了两种情况：一种是采用默认的专家分布，另一种是模拟理想状态下的EPLB，并将后者的结果作为性能上限。
评估结果如下所示：
DeepSeek的性能分析数据显示，其所报告的吞吐量大约是其生产环境的两倍。
在默认的专家不平衡情况下，SGLang的性能比DeepSeek的性能分析数据慢20%；而在模拟的理想EPLB情况下，这个差距缩小到了6%。
对于解码阶段，结果如下所示：
在使用DeepSeek一半数量的节点的情况下，搭载模拟MTP的SGLang仅比DeepSeek的性能分析数据略慢。
在更高的batch大小设置下（256个序列，2,000个输入长度），SGLang实现了每节点每秒22,282个token的处理速度，充分展现了其强大的可扩展性。
下图详细分析了预填充阶段各个内核的执行时间。
如下图所示，SGLang的解码内核分析结果与DeepSeek的结果非常接近：
可以看出，SGLang的解码性能在很大程度上与DeepSeek的性能相一致。
因此，下一步的工作重点，就是预填充阶段的优化了。
局限性与未来工作
总的来说，项目在吞吐量上有着显著的提升，但仍然存在一些局限性以及需要增强的领域：
延迟优化：目前因为专注于提升吞吐量，导致首token时间（TTFT）达到2-5秒，token间延迟（ITL）大约100毫秒。之后还需要进一步优化，来满足实时使用场景的需求。
序列长度约束：由于使用了96个GPU，因此序列长度被限制在较短的范围内。 扩展GPU资源将支持更长的序列，这对于特定应用至关重要。
多token预测（MTP）集成：SGLang支持MTP，但缺乏与DP注意力的完全集成，降低了混合并行配置的效率。
专家并行负载均衡（EPLB）分布：本次实验使用了专家并行负载均衡器（EPLB）的同分布数据，这可能无法反映真实场景中的数据变动。之后还需要研究出现分布偏移时的性能表现。
灵活的张量并行（TP）规模：对于DeepSeek-V3而言，稠密FFN的内存最优TP规模较小，但大于1。目前SGLang仅支持纯TP或DP，导致内存利用率不高。之后还需要支持更灵活的TP选项。
Blackwell支持：目前的实现仅支持NVIDIA Hopper架构。团队正在努力将兼容性扩展到下一代Blackwell架构。
参考资料：
https://lmsys.org/blog/2025-05-05-large-scale-ep/
深夜突袭，
DeepSeek-Prover-V2加冕数学王者！
671B数学推理逆天狂飙
【导读】就在刚刚，DeepSeek-Prover-V2技术报告也来了！34页论文揭秘了模型的训练核心——递归+强化学习，让数学推理大提升。有人盛赞：DeepSeek已找到通往AGI的正确路径！
就在刚刚，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
GitHub：https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main
同时，技术报告也放出了。
论文链接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf
昨天，DeepSeek突然在Hugging Face上开源了671B模型，果然很快就有后续了。
数学证明大提升
此次DeepSeek-Prover-V2的训练核心，就是靠「递归+强化学习」。
首先，DeepSeek-V3会拆解复杂定理，生成一系列子目标和推理思路。随后，GRPO算法就会从多种候选方案中自动学习如何选出最优解。
对于这次放出的技术，网友盛赞说，这将导致超越人类的数字AI，极大地推动AI研究。
方法可以总结如下：
· 优化算法，以实现更快、更智能的模型
· 揭示AI「黑盒」行为的洞见
· 设计更好的架构，无需无尽的试错
· 加速数据分析，以实现更快的突破
因此，这就导致我们通向AGI，产生超级智能。几年内，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）擅长的非形式化推理能力，来提升定理证明搜索的效率。
这部分包括3阶段：从自然语言推理到形式化证明草图、子目标的递归求解、基于子目标的定理证明中的课程学习。
首先提示DeepSeek-V3，同时生成自然语言形式的证明草图，并将其形式化为Lean语言中的定理陈述，其中对于尚未证明的部分使用sorry占位。
接着，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的训练采用了两阶段策略，建立了两种互补的证明生成模式：
高效率非思维链（non-CoT）模式：优化用于快速生成Lean形式化代码，重点在于输出简洁、高效的证明，不包含显式的中间推理步骤
高精度思维链（CoT）模式：注重系统化表达推理过程，逐步构建逻辑清晰的中间步骤，最后生成完整的形式化证明
这两个生成模式的设计延续了DeepSeek-Prover-V1.5的思路，区别在于不同的提示模板。
在第一阶段中，团队结合课程学习框架和专家迭代机制，训练non-CoT证明模型，并通过子目标分解递归地合成复杂问题的证明。
由于non-CoT模式推理速度快、验证成本低，因此非常适合快速迭代与数据采集。
在此基础上，第二阶段引入了冷启动的思维链数据，这些数据整合了DeepSeek-V3的高级数学推理能力与合成的形式化证明。
CoT模式随后进入强化学习阶段，以进一步提升模型在推理和形式化构造之间的衔接能力。
专家迭代（Expert Iteration）
DeepSeek-Prover-V2的non-CoT模型训练采用了「专家迭代」方法，这是目前形式化定理证明系统中广泛使用的训练范式。
论文链接：https://arxiv.org/abs/2009.03393
每轮训练中，当前性能最好的模型会尝试解决前几轮未成功证明的难题。
成功的证明结果经Lean系统验证后被加入监督微调（SFT）数据集中，用于训练下一代更强的模型。
这个过程不仅让模型持续从初始演示数据中学习，还能提炼自身的成功推理路径，不断优化解决难题的能力。
DeepSeek-Prover-V2整体训练流程与V1和V1.5保持一致，只在训练问题的分布上做了两处改进：
加入更多来自自动形式化和开源数据集的题目，扩大训练覆盖范围
加入基于子目标分解生成的题目，尤其针对MiniF2F基准数据集中验证集的高难度问题
监督微调（Supervised Fine-tuning）
团队在DeepSeek-V3-Base-671B的基础上进行微调，学习率设置为常数5e-6，最大上下文长度为16,384 token。
训练数据来自两个来源：
non-CoT数据：由专家迭代生成，强调高效生成Lean代码，但不包含推理过程
冷启动CoT数据：来自DeepSeek-V3的高阶数学推理，通过形式化草图展现清晰的推理路径
non-CoT数据强化模型在Lean生态中的形式验证能力，而CoT数据则更强调将数学直觉转化为结构化形式证明的过程。
强化学习（Reinforcement Learning）
DeepSeek采用了Group Relative Policy Optimization（GRPO）作为强化学习算法。
GRPO不需要单独的价值评估模型，而是通过对每道题采样多个候选证明，并基于相对奖励进行策略优化。
训练时，我们使用二元奖励机制Lean验证成功则得分1，失败则为0。
为了确保训练有效性，团队精心挑选了具有挑战性但又可解的题目作为训练提示。
在每轮训练中，随机选取256道不同题目，每道题生成32个候选证明，最大序列长度为32,768 token。
蒸馏与小模型训练（Distillation）
团队将DeepSeek-Prover-V1.5-Base-7B的最大上下文长度从4,096扩展到32,768 token，并利用在671B模型强化学习阶段采集的rollout数据对模型进行微调。
在CoT模式之外，团队还加入了专家迭代期间采集的non-CoT数据，旨在让小模型具备成本更低的证明能力，能够快速输出精炼的形式化结果。
此外，团队也在7B小模型上执行与671B模型相同的强化学习流程。
实验结果
MiniF2F基准测试结果
MiniF2F包含488个形式化的题目，来源包括AIME、AMC和IMO等竞赛，以及MATH数据集，涵盖了初等数学的核心领域，如代数、数论和归纳法。
这些题目被分为两个大小相等的子集，即miniF2F-valid和miniF2F-test，每个子集包含244道题目，并且在各个学科领域具有相同的分布。
如表1所示，实验结果表明，DeepSeek-Prover-V2-671B在miniF2F-test基准上取得了SOTA性能，当采用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的性能几乎持平。
这些发现表明，SOTA的通用LLM不仅能进行自然语言理解，还能有效支持复杂的形式推理任务。
通过巧妙的子目标分解，模型便可将难题分解为一系列可处理的步骤，从而有效连接非正式推理与形式化证明构建。
· 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的结果显示，相比于non-CoT设置，采用CoT推理时DeepSeek-Prover-V2的通过率得到了显著提升。
尽管训练数据主要源自高中数学，但该模型在更高级的大学数学问题上展现出了强大的泛化能力，代表着强大的形式推理能力。
· PutnamBench
PutnamBench基准测试集包含了1962年至2023年普特南数学竞赛中的数学题。
它是美国和加拿大极负盛名的年度本科生数学竞赛，涵盖分析、线性代数、抽象代数、组合数学、概率论和集合论等多个大学领域的知识。
如表4所示，DeepSeek-Prover-V2-671B在PutnamBench中展现了增强的推理能力，解决了49道题目，并显著优于其non-CoT版本。
这说明，CoT推理方法已经可以有效处理极有挑战性的大学数学问题。
·RL实现的技能发现：7B胜过671B！
此外，团队意外地发现：DeepSeek-Prover-V2-7B在PutnamBench数据集上采用non-CoT生成模式时，也表现出了卓越的性能。
更令人称奇的是，这个较小的7B模型成功解决了DeepSeek-Prover-V2-671B仍未能解决的13道题！
这是为什么？
仔细分析模型的输出后，团队从中发现了一种独特的推理模式——
7B模型经常使用Cardinal.toNat和Cardinal.natCast_inj来处理涉及有限基数的问题，而671B模型生成的输出中明显缺少这种处理方式。
似乎就是这种技术，让7B能有效解决需要精细操作基数值的问题。
组合问题测试结果
CombiBench是一个综合性的基准测试集，其中包含了100道用Lean 4形式化表示的组合竞赛题，配有自然语言描述。
团队采用with-solution设置，此时正确的答案已嵌入在Lean代码中，因此评估可以完全集中在证明过程的生成上。
对其中77道题进行评估后，模型成功解决了12道。
结果表明，尽管该Prover模型主要在数论和代数领域进行训练，但在组合问题上也展现出了良好的泛化潜力，即使这些问题相当难。
ProverBench数据集
为了增强现有基准，团队构建了一个包含325道题目的基准数据集。
其中，15道题目来自AIME 24和25中的数论和代数题目，属于极难的高中竞赛级别题目。剩余的310道题目则来自精选的教科书例题和教学教程。
这就能更全面评估高中竞赛和本科阶段的数学水平。
· AIME题目形式化
美国数学邀请赛AIME 24&25中的题目，已成为评估LLM推理能力的常用基准。
为了弥合模型在形式化和非形式化数学推理能力评估上的差异，我们整理并形式化了AIME 24&25中的部分题目，并排除了几何、组合和计数问题，因为它们在Lean中的表示较复杂。
最终，团队选择了15道题目，涵盖了初等数论和代数中竞赛级别的知识点。
结果显示，DeepSeek-V3-0324成功解决了15道题中的8道题。
而DeepSeek-Prover-V2-671B在已知正确答案的前提下，能够为15道题目中的6道构建出有效的形式化证明。
这种表明，非形式化数学推理与形式化定理证明的性能差距正在显著缩小，高级语言模型在语言理解和形式逻辑的严谨性上正日益接近。
· 教科书题目形式化
除了AIME 24&25之外，团队还从高中竞赛和本科课程教材中挑出题目来扩充基准测试集。
最终，他们形式化了310道题，难度范围很广，覆盖了竞赛级别的初等数学到本科常见的高级主题。
如表6所示，结果表明，采用CoT推理的DeepSeek-Prover-V2-671B始终优于所有基线模型，与在其他基准测试中的表现一致。
在论文最后，团队表示，未来的工作将着重于将范例扩展到类似AlphaProof的系统。
最终目标，就是解决代表自动定理证明领域前沿的IMO级数学难题！
快速开始
我们可以直接使用Hugging Face的Transformers库进行模型推理。
以下是如何生成miniF2F数据集中问题证明的一个简单示例：
from transformers import AutoModelForCausalLM, Autotokenizer
import torch
torch.manual_seed(30)
model_id = "DeepSeek-Prover-V2-7B" # or DeepSeek-Prover-V2-671B
tokenizer = Autotokenizer.from_pretrained(model_id)
formal_statement = """
import Mathlib
import Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
sorry
""".strip()
prompt = """
Complete the following Lean 4 code:
```lean4
{}
```
Before producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
""".strip()
chat = [
{"role": "user", "content": prompt.format(formal_statement)},
]
model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)
import time
start = time.time()
outputs = model.generate(inputs, max_new_token=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)参考资料：
https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main
来源：新智元
为伟大思想而生！
AI+时代，互联网思想（wanging0123)，
第一必读自媒体