大家好，我是 Ai 學習的老章

DeepSeek 一貫的作風，先敲不作聲放出模型文件，隨后才公布技術細節。

1 小時前，DeepSeek 在其 GitHub 賬號放出了部分技術文檔和論文

項目地址：https://github.com/deepseek-ai/DeepSeek-Prover-V2論文：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/DeepSeek_Prover_V2.pdf

1. 引言：形式化推理的挑戰與 DeepSeek 的方案

DeepSeek-Prover-V2 是一個開源的大型語言模型，專為 Lean 4 形式化定理證明而設計。該模型的初始化數據是通過 DeepSeek-V3 驅動的遞歸定理證明流程收集而來。其冷啟動訓練過程始于提示 DeepSeek-V3 將復雜問題分解為一系列子目標。已解決子目標的證明被合成為思維鏈過程，結合 DeepSeek-V3 的逐步推理，為強化學習創建初始冷啟動。這一過程使我們能夠將非形式化和形式化數學推理整合到一個統一的模型中。

DeepSeek-Prover-V2 正是為了應對這一挑戰而生，其核心創新在于：

• 結合非形式化與形式化推理：利用強大的基礎模型 (DeepSeek-V3) 進行初始的非形式化推理（如生成證明思路、分解問題），然后將其與嚴謹的形式化證明步驟相結合。

• 強化學習優化：通過強化學習，特別是利用子目標分解的策略，進一步提升模型在形式化證明構建中的能力。

DeepSeek-Prover-V2 的訓練過程獨具特色，主要包含兩個階段：

a) 冷啟動數據合成 (Synthesize Cold-Start Reasoning Data)

• 遞歸證明流水線：團隊開發了一個簡潔有效的遞歸定理證明流水線。首先，利用 DeepSeek-V3 將復雜的定理分解為高級別的證明草圖（Proof Sketches）和一系列子目標（Subgoals）。

• 子目標證明：為了降低計算成本，使用一個較小的 7B 參數模型來處理每個子目標的證明搜索。

• 數據合成：當一個復雜問題的所有子目標都被解決后，將完整的、逐步的形式化證明（由子目標證明組合而成）與 DeepSeek-V3 生成的相應思維鏈（Chain-of-Thought, CoT，包含高級證明思路和引理分解）配對，形成用于模型初始訓練的“冷啟動”推理數據。這一過程巧妙地將非形式化的解題思路與形式化的證明步驟融為一體。

b) 基于合成數據的強化學習 (Reinforcement Learning with Synthetic Cold-Start Data)

• 篩選挑戰性問題：選取一部分對于 7B 模型來說端到端無法解決、但其所有分解子目標都已被成功證明的難題。

• 數據增強：將這些難題的完整形式化證明（由子目標證明拼接而成）附加到 DeepSeek-V3 對應的 CoT 后面，生成更豐富的訓練數據。

• 強化學習微調：在冷啟動數據上進行初步微調后，采用強化學習進一步優化模型。獎勵信號主要采用二元反饋（證明正確或錯誤），目標是增強模型連接非形式化推理和形式化證明構建的能力。

DeepSeek-Prover-V2 發布了兩個尺寸的模型：

• DeepSeek-Prover-V2-7B:基于 DeepSeek-Prover-V1.5-Base 構建，上下文長度擴展至 32K tokens。

• DeepSeek-Prover-V2-671B:基于 DeepSeek-V3-Base 訓練。

性能方面，DeepSeek-Prover-V2-671B表現出色，達到了當前神經定理證明領域的 SOTA (State-of-the-Art) 水平：

• 在MiniF2F-test數據集上達到88.9%的通過率。

• 解決了PutnamBench數據集中 658 個問題中的49個。

團隊還公開了模型在 miniF2F 數據集上生成的證明，可供下載研究：minif2f-solutions.zip[1]

模型文件：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

4. ProverBench: 新的基準測試集

為了更全面地評估模型在不同難度數學問題上的能力，團隊還推出了ProverBench基準測試集，包含 325 個問題：

• 15 個 AIME 問題：來自近兩年的美國數學邀請賽 (AIME 24, 25) 的數論和代數題目，代表了真實的高中競賽水平挑戰。

• 310 個教科書/教程問題：來自精選的教科書案例和教育教程，提供了多樣化且具有教學意義的形式化數學問題。

ProverBench 旨在覆蓋從高中競賽到本科水平的數學問題，為形式化推理模型的評估提供了更豐富的視角。

ProverBench 數據集地址：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench[2]

5. 如何開始使用 DeepSeek-Prover-V2

用戶可以直接通過 Hugging Face 的transformers庫來使用 DeepSeek-Prover-V2 進行推理。

• 模型下載：

• • 7B 模型： https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B [3]

  • 671B 模型： https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B [4]

• 架構說明：DeepSeek-Prover-V2-671B 與 DeepSeek-V3 共享相同架構，詳細信息可參考 Hugging Face 上的 DeepSeek-V3 文檔 [5] 。

制作不易，如果這篇文章覺得對你有用，可否點個關注。給我個三連擊：點贊、轉發和在看。若可以再給我加個，謝謝你看我的文章，我們下篇再見！

參考資料

minif2f-solutions.zip: https://github.com/deepseek-ai/DeepSeek-Prover-V2/raw/master/minif2f-solutions.zip

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

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B

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

[5]

Hugging Face 上的 DeepSeek-V3 文檔: https://github.com/huggingface/transformers/blob/main/docs/source/en/model_doc/deepseek_v3.md