DeepSeek新數學模型刷爆記錄！7B小模型自主發現671B模型不會的新技能

今天小編分享的科學經驗：DeepSeek新數學模型刷爆記錄！7B小模型自主發現671B模型不會的新技能，歡迎閱讀。

DeepSeek 放大招！新模型專注數學定理證明，大幅刷新多項高難基準測試。

在普特南測試上，新模型 DeepSeek-Prover-V2 直接把記錄刷新到49 道。

目前的第一名在 657 道題中只做出10 道題，為 Kimi 與合作成果 Kimina-Prover。

而未針對定理證明優化的 DeepSeek-R1 只做出1 道。

讓還沒發布的 R2 更令人期待了。

除測評結果之外，論文中特别報告了 " 通過強化學習發現新技能 " 現象。

正如 R1 帶來了 " 啊哈時刻 "，Prover-V2 也有令人意想不到的能力。

具體來說，在普特南測試中，參數量較小的 DeepSeek-Prover-V2-7B 用非 CoT 生成模式成功解決了 13 個 671B 模型未能解決的問題。

團隊仔細檢查該模型的輸出後發現，其推理方法存在一個獨特模式：7B 模型處理涉及有限基數的問題時，經常使用 Cardinal.toNat 和 Cardinal.natCast_inj，而 671B 模型生成的輸出中明顯沒有這些内容。

要注意，7B 模型是在 DeepSeek-Prover-V1.5-Base 模型基礎上，先使用 671B 模型在強化學習階段收集的數據微調，再執行強化學習得來的。

也就是說，7B 模型學會了 671B 模型沒有學會的新技能。

那麼，DeepSeeK-Prover-V2 如何煉成的呢？與前代相比又有哪些改進？

形式化和非形式化數學證明統一模型

DeepSeek 數學定理證明 DeepSeek-Prover 系列模型已推出 3 款：

2024 年 3 月的 DeepSeek-Prover（後簡稱為 Prover-V1）

2024 年 8 月的 DeepSeek-Prover-V1.5（後簡稱為 Prover-V1.5）

2025 年 5 月的 DeepSeek-Prover-V2（後簡稱為 Prover-V2）

Prover-V1 主要探索了通過大規模合成數據集微調 DeepSeek-Math-7B，來推進定理證明。

Prover-V1.5 在此基礎上增加了證明助手反饋的強化學習（RLPAF）和蒙特卡洛樹搜索方法。

Prover-V2 進一步提出 " 子目标分解的強化學習 "，并且基礎模型從 DeepSeek-Math-7B 更新到 DeepSeek-V3。

整合 DeepSeek-V3 的高上下文視窗和強大的自然語言推理能力，把形式化和非形式化數學證明統一到一個模型中。

Prover-V2 還繼承了 Prover-V1.5 提出的 CoT 和非 CoT 生成兩種模式。

接下來，詳細介紹 Prover-V2 的各主要環節。

通過遞歸證明搜索合成冷啟動推理數據

利用 DeepSeek-V3 作為子目标分解和形式化的統一工具構建冷啟動數據集，提示 DeepSeek-V3 将定理分解為高級證明草圖，同時在 Lean 4 中将這些證明步驟形式化，從而產生一系列子目标。

使用一個較小的 70 億參數模型來處理每個子目标的證明搜索，從而減輕相關的計算負擔。一旦一個具有挑戰性的問題的分解步驟得到解決，就将完整的逐步形式化證明與來自 DeepSeek-V3 的相應思維鏈進行配對，以創建冷啟動推理數據。

使用合成冷啟動數據進行子目标分解的強化學習

團隊精心挑選了一組具有挑戰性的問題，這些問題無法由 70 億參數量的證明器模型以端到端的方式解決，但所有分解後的子目标都已成功解決。

通過組合所有子目标的證明，為原始問題構建了一個完整的形式化證明。

然後，将此證明附加到 DeepSeek-V3 的思維鏈中，該思維鏈概述了相應的引理分解，從而實現了非形式化推理與後續形式化的有機結合。

在合成冷啟動數據上對證明器模型進行微調後進行強化學習階段，進一步增強其将非正式推理與形式化證明構建相銜接的能力。遵循推理模型的标準訓練目标，使用二元的正确或錯誤反饋作為獎勵監督的主要形式。

具體訓練細節

兩階段訓練：

DeepSeek-Prover-V2 分兩階段建立互補證明生成模式。

第一階段用高效非思維鏈（non-CoT）模式，聚焦快速生成 Lean 證明代碼，加快迭代和數據收集。

第二階段基于第一階段成果，采用高精度思維鏈（CoT）模式，闡述中間推理步驟，用冷啟動思維鏈數據強化學習，提升復雜問題推理能力。

專家迭代：

其中非 CoT 模式訓練遵循專家迭代範式，用最佳證明策略為難題生成證明嘗試，經 Lean 驗證，成功的納入監督微調（SFT）數據集。與之前版本相比，訓練問題分布有調整，引入了額外問題和子目标分解生成的問題。

監督微調：

對 DeepSeek-V3-Base-671B 做監督微調，訓練語料庫包含兩個互補來源的數據：

一是通過專家迭代收集的非 CoT 數據，這些數據生成的 Lean 代碼不包含中間推理步驟，主要用于強化模型在 Lean 定理證明生态系統中的形式驗證技能。

二是冷啟動 CoT 數據，這些數據将 DeepSeek-V3 的先進數學推理過程提煉為結構化的證明路徑，明确地模拟了将數學直覺轉化為形式證明結構的認知過程。

強化學習：

采用 GRPO 算法，與傳統的 PPO 不同，GRPO 無需單獨的裁判模型，它通過為每個定理提示采樣一組候選證明，并根據它們的相對獎勵來優化策略。

訓練過程中使用二元獎勵機制，即生成的 Lean 證明若被驗證正确則獲得獎勵 1，否則為 0。

為确保學習效果，精心挑選訓練提示，僅包含那些有足夠挑戰性但又能被監督微調後的模型解決的問題。

蒸餾 DeepSeek-Prover-V2 7B

将 DeepSeek-Prover-V1.5-Base-7B 上下文視窗擴展到 32768 個 token，用 DeepSeek-Prover-V2-671B 數據微調，融入非 CoT 證明數據，以便利用小模型生成簡潔的形式化輸出，提供一種經濟高效的證明選項。

此外，對 DeepSeek-Prover-V2-7B 執行與 671B 模型訓練中相同的強化學習階段，以進一步提升其性能。

ProverBench：AIME 和教科書問題的形式化

與 Prover-V2 一起推出 ProverBench，這是一個包含 325 個問題的基準數據集。其中，有 15 個問題是從近期美國數學邀請賽（AIME 24 和 25）的數論與代數題目中形式化而來，提供了真實的高中競賽水平挑戰。其餘 310 個問題則取自精心挑選的教科書示例和教學教程，構成了一套多樣化且基于教學需求的形式化數學問題集合。該基準旨在能夠對高中競賽問題和本科階段數學問題進行更全面的評估。