全球首個，最接近原版DeepSeek開源復現(xiàn)來了！R1四個月狂飆26倍

【導讀】近日，來自SGLang、英偉達等機構(gòu)的聯(lián)合團隊發(fā)了一篇萬字技術(shù)報告：短短4個月，他們就讓DeepSeek-R1在H100上的性能提升了26倍，吞吐量已非常接近DeepSeek官博數(shù)據(jù)！

DeepSeek的含金量還在上升。

就在最近，Hugging Face聯(lián)創(chuàng)、首席科學家Thomas Wolf表示——

DeepSeek的出現(xiàn)，是開源AI領(lǐng)域的ChatGPT時刻！

用他的話說，「正如ChatGPT讓全世界認識到AI的存在，DeepSeek則讓全世界意識到，原來還有著這樣一個充滿活力的開源社區(qū)�！�

DeepSeek-R1的性能已經(jīng)媲美甚至超越美國最頂尖的閉源AI模型，對于全球AI圈來說，這件事的意義都極其深遠。

與此同時，來自SGLang、英偉達等機構(gòu)的數(shù)十人聯(lián)合團隊，也在DeepSeek上整了個大活。

在短短4個月內(nèi)，他們利用最新的SGLang推理優(yōu)化，直接讓DeepSeek-R1在H100上的性能提升了26倍！

這是怎么做到的？

團隊發(fā)布了長篇博文，詳細展示了這一過程。

文章地址：https://lmsys.org/blog/2025-05-05-large-scale-ep/

在96塊H100 GPU上優(yōu)化部署DeepSeek

要知道，DeepSeek模型因為龐大的參數(shù)，以及多頭潛注意力（MLA）和專家混合機制（MoE）等獨特架構(gòu)，如果想要大規(guī)模部署，就必須使用更先進的系統(tǒng)。

為此，團隊先是對SGLang進行了全面升級，完整支持了PD分離、大規(guī)模EP、DeepEP、DeepGEMM及EPLB等功能。

然后憑借這些新特性，成功地在12個節(jié)點共96塊GPU的集群上，復現(xiàn)了DeepSeek的推理系統(tǒng)。

最終，在處理2000個token的輸入序列時，實現(xiàn)了每個節(jié)點每秒52.3k輸入token和22.3k輸出token的吞吐量。

方案運行在Atlas Cloud的12個節(jié)點上，每個節(jié)點均配備8塊H100 GPU

團隊表示，這應(yīng)該是首個吞吐量接近DeepSeek官方數(shù)據(jù)的開源實現(xiàn)。

在本地環(huán)境下部署此方案，成本可降至0.20美元/1M輸出token，約為DeepSeek Chat API官方定價的五分之一。

相較于使用相同資源的原始張量并行策略，此優(yōu)化方案可將輸出吞吐量提升高達5倍。

接下來，團隊深入探討了他們的并行設(shè)計、優(yōu)化方法以及最終成果。

并行設(shè)計

高效的并行化設(shè)計，對于控制DeepSeek架構(gòu)的計算復雜度和內(nèi)存需求至關(guān)重要。

針對以下關(guān)鍵組件，團隊都給出了優(yōu)化方案：注意力層、稠密前饋網(wǎng)絡(luò)（FFN)、稀疏FFN以及語言模型（LM）的頭部。

每個組件都采用了專門設(shè)計的并行化策略，以提升可擴展性、內(nèi)存效率和整體性能。

注意力層

DeepSeek采用了多頭潛注意力機制（MLA)，從而能夠有效地對輸入序列中的復雜依賴關(guān)系進行建模。

為了優(yōu)化這一機制，團隊實現(xiàn)了DP attention，這是一種數(shù)據(jù)并行策略，目的是消除跨設(shè)備的KV緩存冗余，從而顯著降低內(nèi)存開銷。

在SGLang v0.4版本中引入的該方法，現(xiàn)已擴展至支持混合數(shù)據(jù)并行和張量并行，為高效處理小批量數(shù)據(jù)提供了更大的靈活性。

稠密FFN

即便DeepSeek-V3僅使用了三個稠密FFN層，其計算過程仍然可能顯著增加峰值內(nèi)存占用，若不加以謹慎管理，極易導致系統(tǒng)崩潰。

為了解決這個問題，團隊選擇采用數(shù)據(jù)并行（DP）策略，而非張量并行（TP)，主要是考慮到DP的以下優(yōu)勢。

· 更強的可擴展性

當中間層維度為18,432時，較高的TP度（例如TP32）會導致數(shù)據(jù)被低效地分割成小單元片段（例如576個單元），而這些單元無法被128整除。

128，就是現(xiàn)代GPU（如H100）常見的對齊邊界。

這種未對齊的情況，會嚴重阻礙計算效率和內(nèi)存利用率。

相比之下，DP能夠避免數(shù)據(jù)碎片化，從而提供更具可擴展性的解決方案，確�？缭O(shè)備的工作負載均衡分配。

· 優(yōu)化的內(nèi)存效率

傳統(tǒng)觀念認為，TP可以隨著worker size的增加而降低內(nèi)存使用量，但這種優(yōu)勢在DP attention的應(yīng)用場景下會逐漸減弱。

在純TP設(shè)置中，單層Transformer模型的內(nèi)存需求與DP size的關(guān)系如下：

其中，是每個設(shè)備（DP rank）上隱藏狀態(tài)的大小，是模型參數(shù)的數(shù)量，k是一個系數(shù)，表示來自CUDA Graph復制的額外內(nèi)存開銷。

通過假設(shè)DP=TP，當時，此內(nèi)存的使用函數(shù)達到最小值。

DeepSeek-V3使用18,432的中間大小。在prefill階段，CUDA Graph通常被禁用，因此k=0。

但是，每個設(shè)備的token大小很容易超過2,048，導致最佳TP大小為3或更小。

在解碼階段，一個實際的配置可能使用每個設(shè)備128個token，并設(shè)置k=3。在這種情況下，內(nèi)存最佳的TP大小為6。

在這兩個階段，較低的TP度可以最大限度地減少每個設(shè)備的內(nèi)存使用量。

因此，與僅依賴TP相比，DP可以提供更節(jié)省內(nèi)存的擴展方法。

·最小化的通信開銷

在純TP模式下，每個FFN層都需要執(zhí)行兩次all-reduce操作，從而導致巨大的通信開銷。

通過采用DP策略，團隊將該過程優(yōu)化為：在先前的attention層之后執(zhí)行一次reduce-scatter操作，并在下一個attention層之前執(zhí)行一次all-gather操作，從而將通信成本降低50%。

更進一步，如果attention計算也采用純DP模式，那么設(shè)備間的通信將被完全消除，進而顯著提升整體效率。

DP稠密FFN與DP attention的集成方案如下圖左側(cè)所示。用戶可以通過設(shè)置--moe-dense-tp-size=1來啟用。

稀疏FFN

在DeepSeek-V3的MoE架構(gòu)中，稀疏FFN需要處理大量的專家權(quán)重，進而造成顯著的內(nèi)存瓶頸。

為了緩解這一問題，團隊采用了專家并行（EP）策略，將專家權(quán)重分散到多個設(shè)備上。

這種方法能夠有效地擴展內(nèi)存容量，不過，它在維持高性能的同時，也帶來了一些新的挑戰(zhàn)，比如不規(guī)則的全互聯(lián)通信以及工作負載不均衡等。

團隊利用DeepEP框架實現(xiàn)的EP方案

LM頭

LM頭（LM Head）負責計算大型詞匯表上的輸出概率，這是一項資源稠密型的操作，傳統(tǒng)方案是采用詞匯表并行技術(shù)，從TP組中聚合token logits。

為了進一步提升可擴展性和效率，團隊采用了數(shù)據(jù)并行（DP）策略，與處理稠密FFN的方法保持一致。

這種做法不僅可以降低內(nèi)存開銷，還能簡化跨設(shè)備的通信過程，從而提供了更加精簡的解決方案。

預(yù)填充和解碼分離

LLM的推理過程主要包含兩個不同的階段：預(yù)填充（prefill）和解碼（decode)。

預(yù)填充階段屬于計算密集型，需要處理完整的輸入序列；而解碼階段則屬于內(nèi)存密集型，主要負責管理用于生成token的KV緩存。

傳統(tǒng)方案通常在一個統(tǒng)一的引擎中處理這兩個階段，然而，這種預(yù)填充和解碼batch的混合調(diào)度方式會引入效率問題。

為了解決這些挑戰(zhàn)，團隊在SGLang中引入了預(yù)填充和解碼（PD）分離技術(shù)。

如下圖所示，SGLang會通過預(yù)填充服務(wù)器和解碼服務(wù)器的協(xié)同工作，實現(xiàn)兩個階段的交錯執(zhí)行。

接收到輸入請求后，系統(tǒng)的工作流程如下：

1. 預(yù)填充服務(wù)器和解碼服務(wù)器通過握手配對，各自作為本地發(fā)送者和接收者。

2. 解碼服務(wù)器預(yù)先分配KV緩存，并通知預(yù)填充服務(wù)器啟動模型前向傳遞，計算KV緩存。

3. 完成計算后，數(shù)據(jù)將被傳輸至解碼服務(wù)器，由該服務(wù)器負責進行迭代式的token生成。

這種分離機制確保了每個階段都能在最佳狀態(tài)下運行，從而最大限度地利用GPU資源。

并且，為了進一步提升性能，團隊的實現(xiàn)方案還包含以下特性。

• 非阻塞傳輸：數(shù)據(jù)發(fā)送和接收操作在后臺線程中執(zhí)行，從而保證調(diào)度器的事件循環(huán)不會被中斷。

• 基于RDMA的傳輸：遠程直接內(nèi)存訪問（RDMA）技術(shù)利用隊列對（Queue Pairs）進行連接管理，并利用分散-聚集元素（Scatter-Gather Elements, SGE）實現(xiàn)非連續(xù)內(nèi)存塊的高效傳輸。

• 靈活的API集成：SGLang提供了高度可定制的API，能夠與Mooncake和NIXL等高性能RDMA庫無縫集成，從而簡化了數(shù)據(jù)傳輸流程。

大規(guī)模專家并行性

基于DeepEP的專家并行

由DeepSeek團隊開發(fā)的DeepEP提供了一系列優(yōu)化過的通信內(nèi)核，可以有效降低延遲并提升吞吐量，高效地將token路由到多個GPU上。

DeepEP有兩種專門設(shè)計的調(diào)度模式，以滿足不同的工作負載需求。

• 標準調(diào)度模式（Normal Dispatch）：主要針對處理較長的輸入序列進行優(yōu)化，例如預(yù)填充階段，其首要目標是最大化計算吞吐量。 但會生成與CUDA Graph不兼容的符號形狀，從而降低其在解碼階段的效率，因為在解碼階段，內(nèi)核啟動開銷會成為一個顯著的瓶頸。

• 低延遲調(diào)度模式（Low-Latency Dispatch）：專門為解碼階段生成輸出token而設(shè)計，其核心目標是最小化延遲，從而確保實時性能。盡管它支持CUDA Graph，但需要預(yù)先分配固定大小的內(nèi)存。如果實際內(nèi)存需求超過了預(yù)分配的容量，則會觸發(fā)運行時錯誤。

在SGLang中，DeepEP的集成提供了一種自動模式，能夠根據(jù)當前的工作負載，動態(tài)地在上述兩種調(diào)度模式之間進行選擇。

與此同時，通過利用PD分離技術(shù)，使得在DP attention機制下，預(yù)填充階段能夠采用標準調(diào)度模式（Normal Dispatch)，而解碼階段則能夠采用低延遲調(diào)度模式（Low-Latency Dispatch)。

這種集成方式能夠根據(jù)每個階段的具體需求來調(diào)整調(diào)度模式，從而優(yōu)化資源利用率，并提升整體性能。

DeepGEMM集成

由DeepSeek團隊開發(fā)的DeepGEMM，則被用于優(yōu)化MoE模型中的計算過程。

DeepGEMM提供了兩個經(jīng)過專門設(shè)計的函數(shù)，用于處理與MoE相關(guān)的矩陣乘法運算（分組GEMM），每個函數(shù)都針對推理過程的不同階段進行了定制。

• 分組GEMM（連續(xù)布局）：這種內(nèi)核專門為動態(tài)輸入形狀而設(shè)計，使其成為MoE推理預(yù)填充階段的理想選擇。 它可以處理來自不同專家的輸入數(shù)據(jù)，這些數(shù)據(jù)以連續(xù)的方式連接在一起，從而靈活地處理各種輸入尺寸的變化。

• 分組GEMM（掩碼布局）：這種內(nèi)核假定輸入形狀是固定的，并使用掩碼張量來僅計算輸入的有效部分。 由于它與CUDA Graph兼容（可優(yōu)化內(nèi)核啟動過程），因此特別適合于需要顯著降低開銷的解碼階段。

DeepGEMM與DeepEP的調(diào)度模式可以實現(xiàn)無縫集成：

• 對于與預(yù)填充階段的標準調(diào)度模式配合使用的連續(xù)布局內(nèi)核，需要執(zhí)行一個額外的步驟。團隊參考了LightLLM項目，并實現(xiàn)了一個自定義的Triton內(nèi)核來實現(xiàn)高效的置換。確保了從標準調(diào)度模式輸出的數(shù)據(jù)能夠被正確地重新排列，從而實現(xiàn)與連續(xù)GEMM內(nèi)核的平滑集成。

• 掩碼布局內(nèi)核與DeepEP的低延遲調(diào)度模式能夠?qū)崿F(xiàn)無縫對接，因為兩者都針對解碼階段進行了專門優(yōu)化，并且都支持CUDA Graph。

SGLang集成了DeepGEMM，用于在張量并行模式下進行MoE計算。通過在SGLang中設(shè)置環(huán)境變量SGL_ENABLE_JIT_DEEPGEMM為1，即可激活該內(nèi)核，從而為非MoE操作提供更高的計算效率。

雙batch重疊

在多節(jié)點環(huán)境下，有限的通信帶寬可能會顯著增加整體延遲。

為了應(yīng)對這一挑戰(zhàn)，團隊遵循DeepSeek的系統(tǒng)設(shè)計理念，實現(xiàn)了雙batch重疊（TBO）技術(shù)。

TBO將單個batch拆分為兩個micro-batch，從而允許計算和通信過程相互重疊，同時，通過將有效batch大小減半，也降低了峰值內(nèi)存的使用量。

為了創(chuàng)建更易于維護和重用的代碼庫，團隊采用了一個由操作和yield點構(gòu)成的抽象層。

這種方法可以讓用戶像處理單個micro-batch一樣編寫代碼，同時通過策略性地插入yield點來暫停執(zhí)行，從而允許其他micro-batch繼續(xù)進行。

如此一來，不僅消除了代碼重復，減少了對變量后綴的需求，并且還能有效地管理某些執(zhí)行在層末尾完成而其他執(zhí)行尚未完成的情況。

此外，抽象層還能輕松地適應(yīng)不同的重疊區(qū)域選擇，或者未來的增強功能，例如三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, ...)

團隊優(yōu)化了預(yù)填充階段的啟動順序，以避免通過DeepEP中的調(diào)度操作阻塞CPU，即使用的是其異步模式。

具體來說：

• 在GPU從其他rank接收到元數(shù)據(jù)，從而能夠正確分配大小合適的張量之前，調(diào)度操作會阻塞CPU。

• 不正確的實施方式會導致在此期間計算流處于空閑狀態(tài)，因為沒有計算任務(wù)被提交給GPU。

為了實現(xiàn)優(yōu)化，團隊優(yōu)先將計算任務(wù)提交給GPU，然后再啟動可能導致CPU阻塞的通信操作。這樣可以確保GPU在通信期間保持活躍狀態(tài)。

如下圖所示，通過采用正確的啟動順序，TBO可以避免由CPU阻塞操作引起的性能瓶頸。

專家并行負載均衡器

為了解決由專家并行（EP）引起的各個GPU工作負載分布不均勻的問題，DeepSeek開發(fā)了專家并行負載均衡器（Expert Parallelism Load Balancer, EPLB)。

EPLB以專家分布的統(tǒng)計信息作為輸入，計算出專家的最佳排列方式，從而最大限度地減少不平衡現(xiàn)象。

用戶可以分配冗余專家（例如，增加32個專家），這些冗余專家與原有的256個專家組合在一起，形成一個包含288個專家的資源池。

借助這個資源池，EPLB能夠策略性地放置或復制專家——例如，多次復制最常用的專家，或者將使用頻率適中的專家與在單個GPU上很少使用的專家組合在一起。

除了平衡工作負載之外，EPLB還在并行設(shè)計方面提供了更大的靈活性。如果使用最初的256個專家，并行規(guī)模只能被限制為2的冪次方。而EPLB通過使用288個專家，能夠?qū)崿F(xiàn)更多樣化的配置，例如將并行規(guī)模設(shè)置為12或72。

在下圖中，團隊展示了系統(tǒng)規(guī)模和EPLB算法對不平衡問題的影響。

他們將GPU的平衡度，定義為GPU中MoE層的平均計算時間與最大計算時間之比，并使用GPU處理的token數(shù)量來估計其計算時間。

從圖中可以看出，當系統(tǒng)隨著節(jié)點數(shù)量的增加而擴展時，GPU的利用率會降低，而啟用EPLB則可以顯著提高了GPU的利用率。

EPLB在實際服務(wù)中的應(yīng)用

為了使EPLB能夠有效發(fā)揮作用，輸入數(shù)據(jù)的分布必須與實際服務(wù)的工作負載高度吻合。通過以下兩種策略，可以增強這種吻合度：

• 增加batch大小：更大的batch可以減少專家使用過程中的隨機波動，從而提高負載均衡的效果。這一目標可以通過擴展集群規(guī)�；蛘卟捎枚鄑oken預(yù)測（MTP）等技術(shù)來實現(xiàn)。

• 定期進行重新平衡：定期更新專家的排列方式可以利用時間局部性原理，但這需要高效地重新加載專家模型。因此，需要盡可能降低專家模型重新加載操作的成本。

即使采用了EPLB，一定程度的不平衡現(xiàn)象仍然難以避免，未來仍需進一步優(yōu)化。

重新平衡的具體實施方案

SGLang通過三個階段的重新平衡操作，來確保既高效又不會造成中斷，進而在權(quán)重更新期間維持系統(tǒng)的性能。

1. 系統(tǒng)加載階段：可以選擇從磁盤預(yù)加載權(quán)重數(shù)據(jù)到主內(nèi)存中，以加快重新平衡的速度；也可以選擇將權(quán)重數(shù)據(jù)保存在磁盤上，并使用內(nèi)存映射（memory mapping, mmap）技術(shù)，從而減少內(nèi)存的占用量。

2. 重新平衡準備階段：所需的權(quán)重數(shù)據(jù)會在后臺異步傳輸?shù)皆O(shè)備內(nèi)存中，利用空閑的DMA硬件引擎，從而避免中斷正在進行的GPU操作。

3. 重新平衡執(zhí)行階段：通過設(shè)備到設(shè)備的數(shù)據(jù)復制來更新權(quán)重數(shù)據(jù)。還可以通過物理內(nèi)存重綁定等技術(shù)來進一步優(yōu)化這一步驟。

評估

為了突出使用的先進優(yōu)化技術(shù)帶來的吞吐量提升，團隊使用DeepSeek-V3模型，在一個包含12個節(jié)點的集群上，對 SGLang 的不同配置進行了端到端性能評估。

他們比較了以下四種不同的配置：

• SGLang（采用TP16x6）

• SGLang（采用PD分離）

• SGLang（采用PD分離和模擬MTP）

• DeepSeek的結(jié)果

為了適應(yīng)不同的工作負載需求，團隊分別獨立地評估了預(yù)填充階段和解碼階段的性能。

評估結(jié)果總結(jié)如下：

· 預(yù)填充階段：在4個節(jié)點的配置下，對于prompt長度分別為1K、2K和4K的情況，系統(tǒng)所實現(xiàn)的單節(jié)點吞吐量分別為每秒57,674、54,543和50,302個token。

如下圖所示，與TP16基線相比，這種配置實現(xiàn)了高達3.3倍的性能提升。

在假設(shè)工作負載完全平衡的前提下，此系統(tǒng)的吞吐量與DeepSeek官方數(shù)據(jù)之間的差距在5.6%以內(nèi)。

· 解碼階段：在9個節(jié)點的配置下進行評估，對于2K的輸入，系統(tǒng)實現(xiàn)的單節(jié)點吞吐量為22,282個token/秒，這意味著與TP16基線相比，性能提升了5.2倍。

在模擬MTP條件下，對于4K的輸入，系統(tǒng)仍然能夠保持每節(jié)點17,373個token/秒的高吞吐量，僅比DeepSeek官方性能分析數(shù)據(jù)低6.6%。

接著，團隊將SGLang的性能與DeepSeek的推理系統(tǒng)進行對比，力求使實驗設(shè)置盡可能貼近DeepSeek的生產(chǎn)環(huán)境。

對于預(yù)填充階段，團隊測試了一個場景，在該場景中，每個設(shè)備處理16,384個token，輸入長度為4,096。

考慮到DeepSeek的專家分布存在不確定性，他們評估了兩種情況：一種是采用默認的專家分布，另一種是模擬理想狀態(tài)下的EPLB，并將后者的結(jié)果作為性能上限。

評估結(jié)果如下所示：

DeepSeek的性能分析數(shù)據(jù)顯示，其所報告的吞吐量大約是其生產(chǎn)環(huán)境的兩倍。

在默認的專家不平衡情況下，SGLang的性能比DeepSeek的性能分析數(shù)據(jù)慢20%；而在模擬的理想EPLB情況下，這個差距縮小到了6%。

對于解碼階段，結(jié)果如下所示：

在使用DeepSeek一半數(shù)量的節(jié)點的情況下，搭載模擬MTP的SGLang僅比DeepSeek的性能分析數(shù)據(jù)略慢。

在更高的batch大小設(shè)置下（256個序列，2,000個輸入長度），SGLang實現(xiàn)了每節(jié)點每秒22,282個token的處理速度，充分展現(xiàn)了其強大的可擴展性。

下圖詳細分析了預(yù)填充階段各個內(nèi)核的執(zhí)行時間。

如下圖所示，SGLang的解碼內(nèi)核分析結(jié)果與DeepSeek的結(jié)果非常接近：

可以看出，SGLang的解碼性能在很大程度上與DeepSeek的性能相一致。

因此，下一步的工作重點，就是預(yù)填充階段的優(yōu)化了。

局限性與未來工作

總的來說，項目在吞吐量上有著顯著的提升，但仍然存在一些局限性以及需要增強的領(lǐng)域：

• 延遲優(yōu)化：目前因為專注于提升吞吐量，導致首token時間（TTFT）達到2-5秒，token間延遲（ITL）大約100毫秒。之后還需要進一步優(yōu)化，來滿足實時使用場景的需求。

• 序列長度約束：由于使用了96個GPU，因此序列長度被限制在較短的范圍內(nèi)。 擴展GPU資源將支持更長的序列，這對于特定應(yīng)用至關(guān)重要。

• 多token預(yù)測（MTP）集成：SGLang支持MTP，但缺乏與DP注意力的完全集成，降低了混合并行配置的效率。

• 專家并行負載均衡（EPLB）分布：本次實驗使用了專家并行負載均衡器（EPLB）的同分布數(shù)據(jù)，這可能無法反映真實場景中的數(shù)據(jù)變動。之后還需要研究出現(xiàn)分布偏移時的性能表現(xiàn)。

• 靈活的張量并行（TP）規(guī)模：對于DeepSeek-V3而言，稠密FFN的內(nèi)存最優(yōu)TP規(guī)模較小，但大于1。目前SGLang僅支持純TP或DP，導致內(nèi)存利用率不高。之后還需要支持更靈活的TP選項。

• Blackwell支持：目前的實現(xiàn)僅支持NVIDIA Hopper架構(gòu)。團隊正在努力將兼容性擴展到下一代Blackwell架構(gòu)。

參考資料：

https://lmsys.org/blog/2025-05-05-large-scale-ep/

深夜突襲，

DeepSeek-Prover-V2加冕數(shù)學王者！

671B數(shù)學推理逆天狂飆

【導讀】就在剛剛，DeepSeek-Prover-V2技術(shù)報告也來了！34頁論文揭秘了模型的訓練核心——遞歸+強化學習，讓數(shù)學推理大提升。有人盛贊：DeepSeek已找到通往AGI的正確路徑！

就在剛剛，DeepSeek-Prover-V2正式發(fā)布。

此次DeepSeek-Prover-V2提供了兩種模型尺寸：7B和671B參數(shù)。

DeepSeek-Prover-V2-671B：在DeepSeek-V3-Base基礎(chǔ)上訓練，推理性能最強。

DeepSeek-Prover-V2-7B：基于DeepSeek-Prover-V1.5-Base構(gòu)建，上下文長度擴展至高達32Ktoken。

Hugging Face：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

GitHub：https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main

同時，技術(shù)報告也放出了。

論文鏈接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf

昨天，DeepSeek突然在Hugging Face上開源了671B模型，果然很快就有后續(xù)了。

數(shù)學證明大提升

此次DeepSeek-Prover-V2的訓練核心，就是靠「遞歸+強化學習」。

首先，DeepSeek-V3會拆解復雜定理，生成一系列子目標和推理思路。隨后，GRPO算法就會從多種候選方案中自動學習如何選出最優(yōu)解。

對于這次放出的技術(shù)，網(wǎng)友盛贊說，這將導致超越人類的數(shù)字AI，極大地推動AI研究。

方法可以總結(jié)如下：

· 優(yōu)化算法，以實現(xiàn)更快、更智能的模型

· 揭示AI「黑盒」行為的洞見

· 設(shè)計更好的架構(gòu)，無需無盡的試錯

· 加速數(shù)據(jù)分析，以實現(xiàn)更快的突破

因此，這就導致我們通向AGI，產(chǎn)生超級智能。幾年內(nèi)，AI就將產(chǎn)生人類無法理解的高級數(shù)學。

具體來說，DeepSeek-Prover-V2專門用于Lean 4中的形式化定理證明。

其中，初始化數(shù)據(jù)是通過DeepSeek-V3驅(qū)動的遞歸定理證明流程來收集的。

冷啟動訓練過程中，會首先提示DeepSeek-V3將復雜問題分解為一系列子目標，然后將已解決子目標的證明合成為思維鏈過程，并結(jié)合DeepSeek-V3的逐步推理，為強化學習提供了一個初始冷啟動。

通過這個過程，非正式和正式的數(shù)學推理就能集成到一個統(tǒng)一的模型中。

總結(jié)來說，亮點如下。

· 生成冷啟動推理數(shù)據(jù)：遞歸證明搜索方法

為構(gòu)建冷啟動數(shù)據(jù)集，團隊開發(fā)了一個簡單而有效的遞歸定理證明流程，利用 DeepSeek-V3作為統(tǒng)一工具，進行子目標分解和形式化。

DeepSeek-V3會被提示，將定理分解為高層次的證明草圖。同時，在Lean 4中形式化這些證明步驟，從而產(chǎn)生一系列子目標。

首先使用一個較小的 7B 模型來處理每個子目標的證明搜索，以此降低計算負擔。

一旦具有挑戰(zhàn)性的問題的分解步驟得到解決，就將完整的逐步形式化證明與DeepSeek-V3產(chǎn)生的相應(yīng)思維鏈過程相結(jié)合，從而生成冷啟動推理數(shù)據(jù)。

· 基于合成冷啟動數(shù)據(jù)的強化學習

團隊精心挑選了一個具有挑戰(zhàn)性的問題子集——它們無法通過7B prover以端到端的方式解決，但分解后的所有子目標都已成功解決。

通過整合所有子目標的證明，團隊為原始問題構(gòu)建了一個完整的形式化證明。

然后，將此證明附加到DeepSeek-V3的思維鏈中，該思維鏈概述了相應(yīng)的引理分解，從而將非正式推理與后續(xù)形式化過程有機結(jié)合。

在合成冷啟動數(shù)據(jù)上微調(diào)prover模型后，團隊執(zhí)行了強化學習階段，以進一步增強其連接非正式推理與形式化證明構(gòu)建的能力。

根據(jù)推理模型的標準訓練目標，采用二元正確/不正確反饋作為主要的獎勵監(jiān)督形式。

最終，模型DeepSeek-Prover-V2-671B在神經(jīng)定理證明方面實現(xiàn)了當前最優(yōu)的性能，在MiniF2F-test上達到了88.9%的通過率，并解決了PutnamBench中658個問題中的49個。

DeepSeek-Prover-V2為miniF2F數(shù)據(jù)集生成的證明：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip

· 針對AIME與教科書題目的形式化數(shù)據(jù)集ProverBench

ProverBench是一個包含325道題目的基準數(shù)據(jù)集。

其中，15道題目源自最近AIME競賽（AIME 24&25）中的數(shù)論和代數(shù)題目，提供了極具挑戰(zhàn)性的高中競賽級別題目。

剩余的310道題目則來自精選的教科書例題和教學教程，構(gòu)建了一個多樣化的、具有教學意義的形式化數(shù)學題目集合。

因此，這項基準更全面地評估高中競賽和本科階段的數(shù)學水平。

DeepSeek-Prover-V2

在論文中，團隊構(gòu)建了用于子目標分解的推理模型，利用合成的冷啟動數(shù)據(jù)和大規(guī)模強化學習技術(shù)來提升其性能。

通過子目標分解實現(xiàn)遞歸式證明搜索

將復雜定理的證明過程拆解為一系列較小的引理，作為中間步驟，是人類數(shù)學家普遍采用的一種高效策略。

近年來，分層式方法在神經(jīng)定理證明領(lǐng)域得到了廣泛應(yīng)用。它的核心思路是借助現(xiàn)代大型語言模型（LLM）擅長的非形式化推理能力，來提升定理證明搜索的效率。

這部分包括3階段：從自然語言推理到形式化證明草圖、子目標的遞歸求解、基于子目標的定理證明中的課程學習。

首先提示DeepSeek-V3，同時生成自然語言形式的證明草圖，并將其形式化為Lean語言中的定理陳述，其中對于尚未證明的部分使用sorry占位。

接著，7B證明模型用于遞歸地求解被分解出的各個子目標。通過組合這些子目標的證明內(nèi)容，團隊可以構(gòu)建出原始復雜問題的完整形式化證明。

冷啟動數(shù)據(jù)收集流程概覽

DeepSeek利用子目標來擴展可用于模型訓練的形式化定理范圍。

他們生成了兩種類型的子目標定理：一種包含前序子目標作為前提條件（對應(yīng)圖 3(b)），另一種則不包含前提條件（對應(yīng)圖 3(a)）。

這兩種類型的子目標都被納入到專家迭代階段，形成一個漸進式的課程體系，引導證明模型逐步掌握解決精選難題的方法。

這一流程的核心思想與AlphaProof 在測試階段采用的強化學習策略類似：生成目標問題的多種變體，提升模型解決高難度的IMO級別問題的能力。

將分解后的子目標轉(zhuǎn)化為一系列引理（lemma）陳述

首先執(zhí)行步驟 (a)：將原始目標狀態(tài)替換為當前子目標。

接著進行步驟 (b)：將之前的子目標作為前提條件納入當前引理中。

類型 (b) 的陳述用于遞歸求解復雜問題，而類型 (a) 和 (b) 的陳述都被納入課程學習流程中，用于訓練模型逐步掌握推理能力。

最后，將這個組合后的正式證明附加到 DeepSeek-V3最初生成的「思維鏈」之上，形成高質(zhì)量的冷啟動訓練數(shù)據(jù)，用于支持形式化數(shù)學推理的學習。

統(tǒng)一非形式化推理與形式化證明

算法框架包括兩個階段，分別依賴兩個互補模型：用于引理分解的 DeepSeek-V3，以及用于補全具體形式化證明細節(jié)的7B證明模型。

這種方法巧妙地融合了高層次的自然語言推理和低層次的精確證明過程，為構(gòu)建可用于訓練的形式化推理數(shù)據(jù)提供了重要基礎(chǔ)。

· 用合成數(shù)據(jù)實現(xiàn)冷啟動

在研究過程中，DeepSeek挑選出一些特別難解決的問題。

這些問題很棘手，即便用7B證明模型，也沒辦法從頭到尾直接解決。

不過有意思的是，把這些問題拆解成一個個小目標后，每個小目標都能被成功證明。就像拼拼圖一樣，把這些小目標的證明過程按順序組合起來，就能得到原始難題的完整證明，而且這個證明是非常嚴謹、規(guī)范的形式化證明。

接著，DeepSeek把這個完整的證明，添加到 DeepSeek-V3 生成的 「思維鏈」 里。

這里的 「思維鏈」 就像是解題的思路草稿，詳細記錄了把難題分解成小目標的過程。

這樣一來，DeepSeek就得到了一份特殊的證明樣本，它既有像日常思考那樣的非形式化推理過程，又有嚴謹?shù)男问交C明步驟，兩者完美結(jié)合。

通過這種方式，團隊成功收集到了幾百條高質(zhì)量的數(shù)據(jù)。

它們非常重要，是訓練 DeepSeek-Prover-V2模型的基礎(chǔ)。

這里方法的核心是把日常語言描述的證明過程，直接轉(zhuǎn)化成有邏輯結(jié)構(gòu)的形式化框架。

· 用強化學習提升推理能力

用冷啟動合成數(shù)據(jù)對證明模型進行初步優(yōu)化后，就進入了強化學習階段。

強化學習階段目的是讓模型更好地把日常語言的推理過程，轉(zhuǎn)化成嚴謹?shù)男问交C明。

在這個過程中，按照標準的推理模型訓練要求，用 「正確」 或 「錯誤」 這兩種簡單的反饋，作為主要的獎勵監(jiān)督信號。也就是說，如果模型給出的證明是對的，就獎勵它；如果錯了，就不給獎勵。

但訓練有個問題：模型生成的證明結(jié)構(gòu)，經(jīng)常和 「思維鏈」 里分解問題的思路對不上。

為了解決這個問題，在訓練剛開始的時候，團隊就加入了一種新的獎勵機制，專門用來懲罰那些和分解結(jié)構(gòu)不一致的輸出結(jié)果。

在實際訓練中，這個保證結(jié)構(gòu)一致的方法效果非常好，大大提高了證明的準確率。尤其是在證明那些需要很多步驟、特別復雜的定理時，優(yōu)勢更加明顯。

訓練細節(jié)

DeepSeek-Prover-V2的訓練采用了兩階段策略，建立了兩種互補的證明生成模式：

• 高效率非思維鏈（non-CoT）模式：優(yōu)化用于快速生成Lean形式化代碼，重點在于輸出簡潔、高效的證明，不包含顯式的中間推理步驟

• 高精度思維鏈（CoT）模式：注重系統(tǒng)化表達推理過程，逐步構(gòu)建邏輯清晰的中間步驟，最后生成完整的形式化證明

這兩個生成模式的設(shè)計延續(xù)了DeepSeek-Prover-V1.5的思路，區(qū)別在于不同的提示模板。

在第一階段中，團隊結(jié)合課程學習框架和專家迭代機制，訓練non-CoT證明模型，并通過子目標分解遞歸地合成復雜問題的證明。

由于non-CoT模式推理速度快、驗證成本低，因此非常適合快速迭代與數(shù)據(jù)采集。

在此基礎(chǔ)上，第二階段引入了冷啟動的思維鏈數(shù)據(jù)，這些數(shù)據(jù)整合了DeepSeek-V3的高級數(shù)學推理能力與合成的形式化證明。

CoT模式隨后進入強化學習階段，以進一步提升模型在推理和形式化構(gòu)造之間的銜接能力。

專家迭代（Expert Iteration）

DeepSeek-Prover-V2的non-CoT模型訓練采用了「專家迭代」方法，這是目前形式化定理證明系統(tǒng)中廣泛使用的訓練范式。

論文鏈接：https://arxiv.org/abs/2009.03393

每輪訓練中，當前性能最好的模型會嘗試解決前幾輪未成功證明的難題。

成功的證明結(jié)果經(jīng)Lean系統(tǒng)驗證后被加入監(jiān)督微調(diào)（SFT）數(shù)據(jù)集中，用于訓練下一代更強的模型。

這個過程不僅讓模型持續(xù)從初始演示數(shù)據(jù)中學習，還能提煉自身的成功推理路徑，不斷優(yōu)化解決難題的能力。

DeepSeek-Prover-V2整體訓練流程與V1和V1.5保持一致，只在訓練問題的分布上做了兩處改進：

• 加入更多來自自動形式化和開源數(shù)據(jù)集的題目，擴大訓練覆蓋范圍

• 加入基于子目標分解生成的題目，尤其針對MiniF2F基準數(shù)據(jù)集中驗證集的高難度問題

監(jiān)督微調(diào)（Supervised Fine-tuning）

團隊在DeepSeek-V3-Base-671B的基礎(chǔ)上進行微調(diào)，學習率設(shè)置為常數(shù)5e-6，最大上下文長度為16,384 token。

訓練數(shù)據(jù)來自兩個來源：

• non-CoT數(shù)據(jù)：由專家迭代生成，強調(diào)高效生成Lean代碼，但不包含推理過程

• 冷啟動CoT數(shù)據(jù)：來自DeepSeek-V3的高階數(shù)學推理，通過形式化草圖展現(xiàn)清晰的推理路徑

non-CoT數(shù)據(jù)強化模型在Lean生態(tài)中的形式驗證能力，而CoT數(shù)據(jù)則更強調(diào)將數(shù)學直覺轉(zhuǎn)化為結(jié)構(gòu)化形式證明的過程。

強化學習（Reinforcement Learning）

DeepSeek采用了Group Relative Policy Optimization（GRPO）作為強化學習算法。

GRPO不需要單獨的價值評估模型，而是通過對每道題采樣多個候選證明，并基于相對獎勵進行策略優(yōu)化。

訓練時，我們使用二元獎勵機制Lean驗證成功則得分1，失敗則為0。

為了確保訓練有效性，團隊精心挑選了具有挑戰(zhàn)性但又可解的題目作為訓練提示。

在每輪訓練中，隨機選取256道不同題目，每道題生成32個候選證明，最大序列長度為32,768 token。

蒸餾與小模型訓練（Distillation）

團隊將DeepSeek-Prover-V1.5-Base-7B的最大上下文長度從4,096擴展到32,768 token，并利用在671B模型強化學習階段采集的rollout數(shù)據(jù)對模型進行微調(diào)。

在CoT模式之外，團隊還加入了專家迭代期間采集的non-CoT數(shù)據(jù)，旨在讓小模型具備成本更低的證明能力，能夠快速輸出精煉的形式化結(jié)果。

此外，團隊也在7B小模型上執(zhí)行與671B模型相同的強化學習流程。

實驗結(jié)果

MiniF2F基準測試結(jié)果

MiniF2F包含488個形式化的題目，來源包括AIME、AMC和IMO等競賽，以及MATH數(shù)據(jù)集，涵蓋了初等數(shù)學的核心領(lǐng)域，如代數(shù)、數(shù)論和歸納法。

這些題目被分為兩個大小相等的子集，即miniF2F-valid和miniF2F-test，每個子集包含244道題目，并且在各個學科領(lǐng)域具有相同的分布。

如表1所示，實驗結(jié)果表明，DeepSeek-Prover-V2-671B在miniF2F-test基準上取得了SOTA性能，當采用CoT生成策略時，僅用32個樣本便達到了前所未有的82.4%的準確率。

值得注意的是，參數(shù)效率更高的DeepSeek-Prover-V2-7B也展現(xiàn)出了很強的競爭力，超越了現(xiàn)有文獻中的所有開源定理證明器。

他們還發(fā)現(xiàn)了一個明顯的規(guī)律：隨著樣本預(yù)算從1增加到8192，7B和671B模型之間的性能差距顯著擴大，更大規(guī)模的模型展現(xiàn)出更高的樣本效率和更快的性能提升。

· 子目標引導的課程學習在難題證明中的應(yīng)用

表2詳細展示了DeepSeek-Prover-V2在miniF2F基準測試中的解題情況，其在驗證集和測試集上分別取得了91.0%和88.9%的高通過率。

值得注意的是，團隊提出了子目標引導的課程學習框架，將通用模型DeepSeek-V3與輕量級專用7B prover相結(jié)合，在miniF2F-valid上實現(xiàn)了90.2%的成功率，與DeepSeekProver-V2-671B的性能幾乎持平。

這些發(fā)現(xiàn)表明，SOTA的通用LLM不僅能進行自然語言理解，還能有效支持復雜的形式推理任務(wù)。

通過巧妙的子目標分解，模型便可將難題分解為一系列可處理的步驟，從而有效連接非正式推理與形式化證明構(gòu)建。

· CoT vs. non-CoT

表1的實驗結(jié)果表明，在形式化數(shù)學推理中，CoT推理模式相比non-CoT模式具有顯著的性能優(yōu)勢。

這進一步驗證了CoT提示的有效性，它鼓勵將復雜問題分解為中間步驟，并證實了推理時擴展在形式化定理證明領(lǐng)域依然適用。

作為補充，表3提供了DeepSeek-Prover-V2在不同推理模式下生成的token數(shù)量的統(tǒng)計信息。

正如預(yù)期的那樣，CoT模式會生成明顯更長的輸出，反映了其復雜的推理過程。

有趣的是，在non-CoT設(shè)置下，671B模型生成的平均輸出長度比7B模型更長。

更仔細的分析表明，盡管non-CoT模式下沒有顯式推理提示，但較大規(guī)模的模型通常會在證明代碼中插入簡短的自然語言注釋，這些注釋類似于隱式推理步驟。

這表明，即使沒有顯式的CoT提示，高容量模型也可能在內(nèi)部和外部隱式地執(zhí)行中間推理。

本科水平基準測試結(jié)果

· ProofNet

ProofNet包含371道使用Lean 3編寫的題目，這些題目選自一系列流行的本科純數(shù)學教材，涵蓋了實分析、復分析、線性代數(shù)、抽象代數(shù)和拓撲等主題。

表4的結(jié)果顯示，相比于non-CoT設(shè)置，采用CoT推理時DeepSeek-Prover-V2的通過率得到了顯著提升。

盡管訓練數(shù)據(jù)主要源自高中數(shù)學，但該模型在更高級的大學數(shù)學問題上展現(xiàn)出了強大的泛化能力，代表著強大的形式推理能力。

· PutnamBench

PutnamBench基準測試集包含了1962年至2023年普特南數(shù)學競賽中的數(shù)學題。

它是美國和加拿大極負盛名的年度本科生數(shù)學競賽，涵蓋分析、線性代數(shù)、抽象代數(shù)、組合數(shù)學、概率論和集合論等多個大學領(lǐng)域的知識。

如表4所示，DeepSeek-Prover-V2-671B在PutnamBench中展現(xiàn)了增強的推理能力，解決了49道題目，并顯著優(yōu)于其non-CoT版本。

這說明，CoT推理方法已經(jīng)可以有效處理極有挑戰(zhàn)性的大學數(shù)學問題。

·RL實現(xiàn)的技能發(fā)現(xiàn)：7B勝過671B！

此外，團隊意外地發(fā)現(xiàn)：DeepSeek-Prover-V2-7B在PutnamBench數(shù)據(jù)集上采用non-CoT生成模式時，也表現(xiàn)出了卓越的性能。

更令人稱奇的是，這個較小的7B模型成功解決了DeepSeek-Prover-V2-671B仍未能解決的13道題！

這是為什么？

仔細分析模型的輸出后，團隊從中發(fā)現(xiàn)了一種獨特的推理模式——

7B模型經(jīng)常使用Cardinal.toNat和Cardinal.natCast_inj來處理涉及有限基數(shù)的問題，而671B模型生成的輸出中明顯缺少這種處理方式。

似乎就是這種技術(shù)，讓7B能有效解決需要精細操作基數(shù)值的問題。

組合問題測試結(jié)果

CombiBench是一個綜合性的基準測試集，其中包含了100道用Lean 4形式化表示的組合競賽題，配有自然語言描述。

團隊采用with-solution設(shè)置，此時正確的答案已嵌入在Lean代碼中，因此評估可以完全集中在證明過程的生成上。

對其中77道題進行評估后，模型成功解決了12道。

結(jié)果表明，盡管該Prover模型主要在數(shù)論和代數(shù)領(lǐng)域進行訓練，但在組合問題上也展現(xiàn)出了良好的泛化潛力，即使這些問題相當難。

ProverBench數(shù)據(jù)集

為了增強現(xiàn)有基準，團隊構(gòu)建了一個包含325道題目的基準數(shù)據(jù)集。

其中，15道題目來自AIME 24和25中的數(shù)論和代數(shù)題目，屬于極難的高中競賽級別題目。剩余的310道題目則來自精選的教科書例題和教學教程。

這就能更全面評估高中競賽和本科階段的數(shù)學水平。

· AIME題目形式化

美國數(shù)學邀請賽AIME 24&25中的題目，已成為評估LLM推理能力的常用基準。

為了彌合模型在形式化和非形式化數(shù)學推理能力評估上的差異，我們整理并形式化了AIME 24&25中的部分題目，并排除了幾何、組合和計數(shù)問題，因為它們在Lean中的表示較復雜。

最終，團隊選擇了15道題目，涵蓋了初等數(shù)論和代數(shù)中競賽級別的知識點。

結(jié)果顯示，DeepSeek-V3-0324成功解決了15道題中的8道題。

而DeepSeek-Prover-V2-671B在已知正確答案的前提下，能夠為15道題目中的6道構(gòu)建出有效的形式化證明。

這種表明，非形式化數(shù)學推理與形式化定理證明的性能差距正在顯著縮小，高級語言模型在語言理解和形式邏輯的嚴謹性上正日益接近。

· 教科書題目形式化

除了AIME 24&25之外，團隊還從高中競賽和本科課程教材中挑出題目來擴充基準測試集。

最終，他們形式化了310道題，難度范圍很廣，覆蓋了競賽級別的初等數(shù)學到本科常見的高級主題。

如表6所示，結(jié)果表明，采用CoT推理的DeepSeek-Prover-V2-671B始終優(yōu)于所有基線模型，與在其他基準測試中的表現(xiàn)一致。

在論文最后，團隊表示，未來的工作將著重于將范例擴展到類似AlphaProof的系統(tǒng)。

最終目標，就是解決代表自動定理證明領(lǐng)域前沿的IMO級數(shù)學難題！

快速開始

我們可以直接使用Hugging Face的Transformers庫進行模型推理。

以下是如何生成miniF2F數(shù)據(jù)集中問題證明的一個簡單示例：

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+時代，互聯(lián)網(wǎng)思想（wanging0123)，

第一必讀自媒體