各位五一快樂(lè)！（順便星標(biāo)??一下本號(hào)，最近很多朋友反應(yīng)不能及時(shí)看到內(nèi)容更新，只有關(guān)注并且??才會(huì)第一時(shí)間收到更新）

讓 AI 理解并進(jìn)行嚴(yán)格的數(shù)學(xué)推理，尤其是形式化證明（就是用像 Lean、Coq 這樣的證明輔助語(yǔ)言寫(xiě)的、機(jī)器可驗(yàn)證的證明），一直是個(gè)挑戰(zhàn)。這不僅需要邏輯能力，還需要某種程度的“數(shù)學(xué)直覺(jué)”來(lái)分解復(fù)雜問(wèn)題。

今天DeepSeek 正式開(kāi)源了他們最新的DeepSeek-Prover-V2模型，專(zhuān)門(mén)用于Lean 4形式化定理證明。這次不僅僅是一次模型的迭代（對(duì)DeepSeek-Prover-V1.5），更帶來(lái)了一種結(jié)合大語(yǔ)言模型（LLM）的直覺(jué)和強(qiáng)化學(xué)習(xí)（RL）嚴(yán)謹(jǐn)性的新思路

DeepSeek這次開(kāi)源了兩個(gè)模型版本

DeepSeek-Prover-V2-671B：基于 DeepSeek-Prover-V1.5-Base 構(gòu)建，上下文長(zhǎng)度擴(kuò)展到 32K tokens

DeepSeek-Prover-V2-7B：基于 DeepSeek-V3-Base 訓(xùn)練，還附有詳細(xì)的論文，論文題目《DeepSeek-Prover-V2：通過(guò)強(qiáng)化學(xué)習(xí)推進(jìn)子目標(biāo)分解的形式數(shù)學(xué)推理》

性能 SOTA：DeepSeek-Prover-V2-671B模型，在標(biāo)準(zhǔn)測(cè)試集MiniF2F-test上達(dá)到了88.9%的通過(guò)率，這是目前的最佳水平

挑戰(zhàn)難題：在更難的PutnamBench（基于普特南數(shù)學(xué)競(jìng)賽題）上，它成功解決了49 個(gè)問(wèn)題（總共 658 個(gè)）。從圖表看，這個(gè)成績(jī)也顯著優(yōu)于之前的 BFS-Prover 7B、STP 7B 等模型

Hugging Face (模型下載):

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

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

論文鏈接:

https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf

核心思路：兩步走，聯(lián)通直覺(jué)與形式

DeepSeek-Prover-V2 的訓(xùn)練方法很有意思，可以概括為兩個(gè)關(guān)鍵階段：

一,冷啟動(dòng)數(shù)據(jù)合成：用大模型“拆解”問(wèn)題

他們先利用DeepSeek-V3這個(gè)強(qiáng)大的基礎(chǔ)模型。通過(guò)精心設(shè)計(jì)的 Prompt，讓 V3 同時(shí)做兩件事：

• ?分解定理：把一個(gè)復(fù)雜的證明目標(biāo)，拆解成一系列更小的、更容易處理的子目標(biāo)（Subgoals），并給出高級(jí)證明草圖（Proof Sketch）。這模擬了人類(lèi)數(shù)學(xué)家的“直覺(jué)”或“規(guī)劃”能力

• ?同步形式化：在分解的同時(shí)，嘗試將這些證明步驟形式化為 Lean 4 代碼片段，形成一系列子目標(biāo)

然后，他們用一個(gè)較小的 7B 參數(shù)模型（DeepSeek-Prover-V2-7B 或類(lèi)似模型）去搜索每個(gè)子目標(biāo)的具體形式化證明。這樣做的好處是，針對(duì)小目標(biāo)的搜索計(jì)算成本更低

一旦所有子目標(biāo)都被解決了，就把這些子目標(biāo)的證明組合起來(lái)，形成原始問(wèn)題的完整形式化證明。

最后，將這個(gè)完整的形式化證明與 DeepSeek-V3 最初生成的“分解思路+形式化草稿”（Chain-of-Thought）配對(duì)，構(gòu)成一份高質(zhì)量的“冷啟動(dòng)”訓(xùn)練數(shù)據(jù)。這份數(shù)據(jù)既包含了宏觀的解題策略，也包含了微觀的、嚴(yán)格的證明步驟

二，強(qiáng)化學(xué)習(xí)：用合成數(shù)據(jù)“教會(huì)”模型連接思路與證明

篩選出一部分“有挑戰(zhàn)性”的問(wèn)題：這些問(wèn)題是 7B 模型無(wú)法直接端到端解決，但其分解出的所有子目標(biāo)都能被成功證明的。用這些問(wèn)題對(duì)應(yīng)的“合成證明”（由子目標(biāo)證明拼接而成）和 DeepSeek-V3 的思路鏈，來(lái)構(gòu)建 RL 的初始數(shù)據(jù)

用這些合成數(shù)據(jù)對(duì) Prover 模型進(jìn)行微調(diào)

然后進(jìn)入強(qiáng)化學(xué)習(xí)階段。目標(biāo)是進(jìn)一步提升模型將非形式化推理（如 V3 給出的解題思路）轉(zhuǎn)化為形式化證明的能力。訓(xùn)練目標(biāo)很直接：對(duì)于模型生成的證明，系統(tǒng)反饋一個(gè)二元信號(hào)（正確或錯(cuò)誤）作為獎(jiǎng)勵(lì)，驅(qū)動(dòng)模型學(xué)習(xí)生成正確的證明

新基準(zhǔn)：ProverBench，更全面的評(píng)測(cè)

為了更全面地評(píng)估模型在不同數(shù)學(xué)領(lǐng)域和難度上的能力，DeepSeek 還推出了一個(gè)新的基準(zhǔn)測(cè)試集ProverBench。

組成：共325個(gè)問(wèn)題

• ?15 個(gè)來(lái)自近兩年的AIME（美國(guó)數(shù)學(xué)邀請(qǐng)賽）的數(shù)論和代數(shù)題，代表了真實(shí)的高中競(jìng)賽挑戰(zhàn)

• ?310 個(gè)來(lái)自精心挑選的教科書(shū)和教程，覆蓋了數(shù)論 (40), 初等代數(shù) (30), 線性代數(shù) (50), 抽象代數(shù) (40), 微積分 (90), 實(shí)分析 (30), 復(fù)分析 (10), 泛函分析 (10), 概率論 (10) 等多個(gè)本科及以上數(shù)學(xué)領(lǐng)域

目標(biāo)：提供一個(gè)能同時(shí)評(píng)估高中競(jìng)賽水平和本科基礎(chǔ)數(shù)學(xué)能力的、更多樣化、更貼近教育場(chǎng)景的評(píng)測(cè)平臺(tái)

快速上手：自己跑試試看

想自己跑跑看？很簡(jiǎn)單：

模型可以通過(guò) Hugging Face 的transformers庫(kù)直接加載使用

DeepSeek-Prover-V2-671B 與 DeepSeek-V3架構(gòu)相同，可以直接參考 DeepSeek-V3 在 Hugging Face 上的文檔

倉(cāng)庫(kù)里提供了一個(gè)基礎(chǔ)的 miniF2F 推理示例代碼：輸入形式化的定理描述，設(shè)置好 Prompt（要求模型先提供詳細(xì)證明計(jì)劃，再生成 Lean 4 代碼），模型就能輸出證明思路和代碼

# 示例代碼片段 (關(guān)鍵部分) from transformers import AutoModelForCausalLM, AutoTokenizer import torch model_id = "deepseek-ai/DeepSeek-Prover-V2-7B" # or 671B tokenizer = AutoTokenizer.from_pretrained(model_id) model = AutoModelForCausalLM.from_pretrained(model_id, ...) formal_statement = """ import Mathlib ... 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... """.strip() chat = [{"role": "user", "content": prompt.format(formal_statement)}] inputs = tokenizer.apply_chat_template(chat, ...) outputs = model.generate(**inputs, ...)

參考：

https://github.com/deepseek-ai/DeepSeek-Prover-V2

?星標(biāo)AI寒武紀(jì)，好內(nèi)容不錯(cuò)過(guò)?

用你的贊和在看告訴我～

求贊