比GPT-4更懂數學？中國首個形式數學推理大模型發佈，DeepSeek-Prover-V2攻破高階數學推理壁壘

在 LLM 能力迅猛擴展的今天，語言模型在對話、程式碼、文字生成中已展現出驚人的表現。然而，“能說”並不等於“能證”。尤其在數學這個對邏輯鏈條嚴絲合縫要求極高的領域，AI 是否具備真正的“思考能力”，依然是未解之問。

近日，DeepSeek 團隊發佈了其全新模型 DeepSeek-Prover-V2，向這個問題給出了一個具有里程碑意義的答案。這是一款專門為 形式化數學證明（Formal Theorem Proving）而設計的大模型，支援 Lean 4 系統的嚴謹語法，借助 DeepSeek-V3 強大的自然語言推理能力，實現了“自然語言 + 形式證明”的聯動，首次在複雜推理任務中達到了接近人類解題者的水平。

01 為什麼數學難？

一場關於AI 數學家的冷啟動實驗

傳統的大模型在處理數學問題時面臨兩個困境：

• 自然語言理解不等於嚴謹推理：大模型雖擅長語言生成，但在嚴格定義、公理體系下的形式推導上常常出錯。
• 資料稀缺：真實的數學證明語料非常稀缺，尤其是 Lean 4 這種形式語言的資料難以收集。

生成式 AI 的最大瓶頸之一，不再是畫得好不好，而是畫得對不對。這背後，本質是 AI 圖像生成模型“缺乏空間理解能力”，無法基於使用者意圖精準地構圖和佈局。

形式化數學與語言模型的鴻溝

為什麼數學難？數學問題的難點不在於知識本身，而在於它對邏輯的嚴謹性提出了極高要求。傳統大模型可以“模糊應答”，但在 Lean 等形式化語言系統中，每一步推理都必須滿足：

• 明確的前提；
• 完整的中間演繹；
• 可復現、可驗證的形式語法。

換句話說，僅靠語言建模能力，並不能實現有效的自動數學證明。

02 創新路徑

從子目標分解到強化學習的全流程範式

DeepSeek-Prover-V2 的成功，歸功於其極具創新性的技術架構，引入了 “子目標分解 + 強化學習” 的新範式，整體流程如下：

1）冷啟動資料建構：融合自然語言與形式邏輯

目標：建構可用於訓練的高品質推理樣本

• 首先利用 DeepSeek-V3 提出 子目標分解（Subgoal Decomposition），將複雜定理拆解為多個易於處理的推理單元；
• 同時生成每一步推理的自然語言解釋（Chain-of-Thought）；
• 利用 Lean 4 語言形式化這些推理過程，確保每一步可驗證、可執行；
• 通過呼叫 7B 較小模型完成子目標的自動形式證明，建構成完整“非形式 + 形式”資料對，組成冷啟動訓練集。

這一階段最大貢獻是：首次系統性地建構出語言-邏輯對應的高品質數學資料集。最終，整個流程構成了一條新穎的“遞迴式數學證明生成管線”，既保留了大模型的推理靈活性，又建構了形式語言的邏輯嚴謹性。

2）強化學習階段：從“能模仿”走向“能思考”

目標：最佳化模型的綜合推理能力，提升生成證明的完整性

在建構完冷啟動資料後，DeepSeek-Prover-V2 進入第二階段：強化學習訓練。

這一階段的關鍵在於：

• 對於一類“整體難以一次證明，但子目標均已解決”的問題，通過拼接所有子目標的證明，生成原問題的完整證明；
• 將完整證明過程與 DeepSeek-V3 的推理鏈（即“人類思路”）相結合，作為訓練樣本；
• 採用二分類獎勵機制（正確 vs 錯誤）進行強化學習微調，逐步提高模型解決“推理盲點”的能力。

最終產出的DeepSeek-Prover-V2-671B同時具備語言理解能力和形式推理能力。

👉快速嘗試示例：

03 模型性能

性能要求不低，但本地運行無壓力

在數學推理最具代表性的兩個測試集上，DeepSeek-Prover-V2 交出了亮眼答卷：

PutnamBench 是從美國著名數學競賽 Putnam Exam 中抽取的高難度題目，代表著大學數學的上限挑戰。能解決其中的近 50 題，標誌著模型已具備攻克非套路性數學難題的能力。此外，模型還在高階數學科目上展現了跨學科遷移能力，包括抽象代數、泛函分析、實變函數、機率論等。

ProverBench：首個“競賽 + 教材”雙源 Lean 評測集

為更系統地評估模型的泛化能力，團隊還同步發佈了 ProverBench 資料集，包含 325 道數學題目，覆蓋高中競賽與本科課程：

• AIME 24&25：真實中學生數學競賽題；
• 教材/教學題：涵蓋代數、微積分、數論、分析等核心科目。

這標誌著 Lean 語言首次擁有兼具教學性與挑戰性的公開測試集，為下一階段的AI 數學能力排名打下基礎。

開放生態：模型、資料與 API 全部開放

• 支援最長 32K 上下文輸入，適用於多步鏈式推理任務；
• 可直接呼叫 Huggingface 介面進行推理，也可通過 OpenRouter 實現 API 快速接入。

此外，模型所用程式碼全部開源，適合二次研究與跨場景遷移（如程式碼形式驗證、合約安全等）。

04 寫在最後

從數學到自動程式設計的通路是否已開啟？

DeepSeek-Prover-V2 的發佈，揭示出一種 未來 AI 推理的新範式：

• 自然語言 → 子目標結構化 → 形式語言驗證；
• 結合強化學習，實現“AI 自主建構邏輯世界”。

這意味著，在教育領域，它可用於打造新一代 AI 數學助教；在科研領域，它為複雜定理驗證提供自動化工具；在工程實踐中，它的框架可遷移至自動程式設計、合約驗證等高邏輯場景。潛在應用包括：

• 🎓 教育：AI 數學助教、作業自動批改；
• 🧮 科研：複雜定理的形式驗證、證明輔助；
• 🧑‍💻 工業：程式碼正確性驗證、形式合約系統建模；
• 🧠 認知建模：研究人類如何構造推理鏈條與分解問題。

DeepSeek-Prover-V2 是中國團隊在基礎模型領域的一次重大突破，也是對“AI 是否能真正理解數學”的有力回應。在大模型“模仿語言”的時代逐漸過渡到“建構邏輯”的新紀元，DeepSeek 給出的答案，是用推理和形式語言架起橋樑。 (Frank的神經網路)