DeepSeek開源Prover-V2強推理模型，網友：奧數從沒這麼簡單過

機器之心報道

編輯：大盤雞、澤南

DeepSeek R2 的前奏？

五一勞動節到了，DeepSeek 的新訊息可沒停下來。

前些天到處都在流傳著 DeepSeek-R2 即將釋出的傳言，DeepSeek 確實有新動作，不過大家沒等來 R2，等來的是 DeepSeek-Prover-V2，它當然也是開源的。

Prover-V2 在定理證明賽道上實現了業內最佳效能，在 MiniF2F 測試中達到了 88.9% 的透過率，在 AIME 24、25 上也有不錯的分數。

在 4 月 30 日晚，機器學習協作平臺 HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技術細節。

這次 DeepSeek 團隊釋出了兩個版本的 DeepSeek-Prover-V2 模型，引數規模分別為 7B 和 671B。

其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基礎上訓練而成，而 DeepSeek-Prover-V2-7B 則基於 DeepSeek-Prover-V1.5-Base 構建，並支援最長 32K tokens 的上下文長度擴充套件。

DeepSeek-Prover-V2-7B 連結：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
DeepSeek-Prover-V2-671B 連結：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

要一句話總結 DeepSeek-Prover-V2 到底是什麼？它是一款專為「數學 AI 程式語言」Lean 4 打造的開源大語言模型，專注於形式化定理證明。

它的初始化資料透過一個由 DeepSeek-V3 驅動的遞迴定理證明流程收集而來。在冷啟動訓練階段，首先透過提示 DeepSeek-V3 將複雜問題分解成一系列可以解決的子目標。每解決一個子目標就會將這些證明整合成「思維鏈」。並融合 DeepSeek-V3 的逐步推理軌跡，共同構建出用於強化學習的初始訓練資料。

這一策略的精妙之處在於：它能夠將非形式化和形式化的數學推理融合到一個統一的模型中，讓模型既能像人一樣靈活思考，也能像機器一樣嚴謹論證，真正實現了數學推理的一體化融合。

具體是如何實現的呢？DeepSeek 也釋出了 DeepSeek-Prover-V2 的技術報告，讓我們看看其中是怎麼說的：

技術概述

透過遞迴式證明搜尋生成冷啟動推理資料

為了構建冷啟動資料集，DeepSeek 團隊設計了一條簡潔高效的遞迴定理證明流程，使用 DeepSeek-V3 作為統一工具，既負責子目標的拆解，也負責推理步驟的形式化表達。其中具體的過程則是透過提示引導 DeepSeek-V3 將定理拆解為高層次的證明草圖，並在此過程中同時將這些推理步驟用 Lean 4 語言形式化，最終生成一系列結構清晰、邏輯嚴密的子目標。

DeepSeek-Prover-V2 使用冷啟動資料收集過程概覽。

降低計算開銷一直是 DeepSeek 團隊的強項，這次也不例外。他們使用一個更小的 7B 模型來完成每個子目標的證明搜尋，從而降低計算負擔。當複雜問題被拆解的各個步驟都成功解決後，他們將完整的形式化逐步證明與 DeepSeek-V3 生成的思維鏈相對應，組合成冷啟動推理資料。

何將分解的子目標轉化為一系列引理陳述的一個示例。

基於合成冷啟動資料的強化學習

DeepSeek 團隊挑選了一部分具有挑戰性的定理問題。7B 證明模型沒法雖然沒法兒將它們端到端的解決，但是能夠拿捏拆解出來的一系列子目標。

整合所有子目標的證明就可以構建出原始問題的完整形式化證明。隨後，將該正式證明附加到 DeepSeek-V3 所生成的思維鏈，這條思維鏈展示了對應的引理拆解過程，從而形成了一份將非形式化推理與後續形式化過程緊密融合的訓練資料。

在對證明模型進行合成冷啟動資料的微調後，研究團隊進一步引入強化學習階段，進一步提升模型將非形式化推理轉化為形式化證明的能力。在訓練過程中，遵循推理模型的通用目標，採用「對 / 錯」二值反饋作為主要的獎勵訊號。

最終得到的模型 DeepSeek-Prover-V2-671B 在神經定理證明任務中達到了當前最先進的效能，在 MiniF2F-test 上的透過率達到 88.9%，併成功解決了 PutnamBench 資料集中 658 道題中的 49 道。DeepSeek-Prover-V2 在 miniF2F 資料集上生成的所有證明已整理為 ZIP 檔案，開放下載。

下載連結：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip

訓練細節、實驗結果

DeepSeek-Prover-V2 經歷了兩階段訓練，這一過程建立了兩種互補的證明生成模式：

1. 高效非思維鏈（non-CoT）模式：此模式針對快速生成正式的 Lean 證明程式碼進行最佳化，專注於生成簡潔的證明，沒有顯式的中間推理步驟。

2. 高精度思維鏈（CoT）模式：此模式系統地闡述中間推理步驟，強調透明度和邏輯進展，然後構建最終的正式證明。

與 DeepSeek-Prover-V1.5 一致，這兩種生成模式由兩個不同的引導提示控制。在第一階段採用專家迭代，在課程學習框架內訓練一個非 CoT 證明模型，同時透過基於子目標的遞迴證明合成難題的證明。選擇非 CoT 生成模式是為了加速迭代訓練和資料收集過程。

在此基礎上，第二階段利用了冷啟動鏈式思維（CoT）資料，透過將 DeepSeek-V3 複雜的數學推理模式與合成形式證明相結合而生成。CoT 模式透過進一步的強化學習階段得到增強，遵循了通常用於推理模型的標準訓練流程。

DeepSeek-Prover-V2 的非 CoT 模式訓練過程遵循專家迭代的正規化，這是開發形式化定理證明器廣泛採用的框架。在每次訓練迭代中，當前最佳證明策略用於生成那些在先前迭代中未解決的難題的證明嘗試。這些成功的嘗試經由 Lean 證明助手驗證後，被納入 SFT 資料集以訓練改進的模型。這一迭代迴圈不僅確保模型能夠從初始演示資料集中學習，還能提煉出自己的成功推理軌跡，逐步提高其解決更難問題的能力。總體訓練過程與 DeepSeek-Prover-V1 的訓練過程大致一致，僅對訓練問題的分佈進行了兩項修改。

首先，Prover-V2 引入了來自自動形式化和各種開源資料集的額外問題，擴大了訓練問題領域的覆蓋範圍。其次，新模型透過子目標分解生成的問題來擴充資料集，旨在解決 MiniF2F 基準測試有效劃分中的更多挑戰性例項。

研究人員在 DeepSeek-V3-Base-671B 上使用恆定的學習率 5e-6，在 16384 個 token 的上下文中進行監督微調。訓練語料庫由兩個互補來源組成：1）透過專家迭代收集的非 CoT 資料，生成無需中間推理步驟的 Lean 程式碼；2）第 2.2 節中描述的冷啟動 CoT 資料，將 DeepSeek-V3 的高階數學推理過程提煉為結構化的證明路徑。非 CoT 元件強調精益定理證明器生態系統中的形式驗證技能，而 CoT 示例明確地建模了將數學直覺轉化為形式證明結構的認知過程。

Prover-V2 採用 GRPO 強化學習演算法，與 PPO 不同，GRPO 透過為每個定理提示取樣一組候選證明並根據它們的相對獎勵最佳化策略，消除了對單獨批評模型的需求。訓練使用二元獎勵，每個生成的 Lean 證明如果被驗證為正確則獲得 1 個獎勵，否則為 0。為了確保有效學習，研究人員精心挑選訓練提示，僅包括那些對監督微調模型具有足夠挑戰性但可解決的問題。模型在每次迭代中取樣 256 個不同的問題，為每個定理生成 32 個候選證明，最大序列長度為 32768 個 token。

最後是模型的蒸餾。研究人員把 DeepSeek-Prover-V1.5-Base-7B 的最大上下文長度從 4096 個 token 擴充套件到了 32768 個，並使用 DeepSeek-Prover-V2-671B 強化學習階段收集的 rollout 資料對這個擴充套件上下文模型進行微調。除了 CoT 推理模式外，研究人員還整合了專家迭代過程中收集的非 CoT 證明資料，以實現一種成本效益高的證明選項，該選項能夠生成簡潔的形式化輸出，並且模型規模較小。此外，7B 模型也採用了與 671B 模型訓練相同的強化學習階段以提升效能。

研究人員對 DeepSeek-Prover-V2 在形式定理證明的各種基準資料集上進行了系統評估，涵蓋了高中競賽題目和本科水平的數學問題。實驗表明，671B 版的模型實現了前所未有的準確率，且與業內其他先進模型相比效率也更高。

在 miniF2F 測試資料集上與最先進模型的比較。

DeepSeek-Prover-V2-671B 在 miniF2F 基準上解決的問題。

ProofNet – 測試和 PutnamBench 的實驗結果。

ProverBench：AIME 與教材題目的形式化基準資料集

這次，DeepSeek 還發布了 ProverBench，這是一個包含 325 道題目的基準資料集。其中，15 道題來自最近兩屆 AIME 數學競賽（AIME 24 和 25）中的數論與代數題目，經過形式化處理，具備真實的高中競賽難度。其餘 310 道題則精選自教材示例和教學教程，覆蓋內容多樣，具有良好的教學基礎。

ProverBench 連結：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

該資料集旨在支援對模型在高中競賽題和本科數學題兩個層面的綜合評估。