新智元報道
新智元報道
編輯：編輯部 JZH
【新智元導讀】就在剛剛，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, Autotokenizerimport torchtorch.manual_seed(30)model_id = "DeepSeek-Prover-V2-7B"# or DeepSeek-Prover-V2-671Btokenizer = Autotokenizer.from_pretrained(model_id)formal_statement = """import Mathlibimport Aesopset_option maxHeartbeats 0open 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 timestart = 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