就在剛剛，DeepSeek-Prover-V2正式發(fā)布。

此次DeepSeek-Prover-V2提供了兩種模型尺寸：7B和671B參數(shù)。

DeepSeek-Prover-V2-671B：在DeepSeek-V3-Base基礎(chǔ)上訓(xùn)練，推理性能最強(qiáng)。

DeepSeek-Prover-V2-7B：基于DeepSeek-Prover-V1.5-Base構(gòu)建，上下文長度擴(kuò)展至高達(dá)32Ktoken。

圖片

圖片

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

GitHub：https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main

同時(shí)，技術(shù)報(bào)告也放出了。

圖片

論文鏈接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf

昨天，DeepSeek突然在Hugging Face上開源了671B模型，果然很快就有后續(xù)了。

圖片

數(shù)學(xué)證明大提升

此次DeepSeek-Prover-V2的訓(xùn)練核心，就是靠「遞歸+強(qiáng)化學(xué)習(xí)」。

首先，DeepSeek-V3會(huì)拆解復(fù)雜定理，生成一系列子目標(biāo)和推理思路。隨后，GRPO算法就會(huì)從多種候選方案中自動(dòng)學(xué)習(xí)如何選出最優(yōu)解。

對于這次放出的技術(shù)，網(wǎng)友盛贊說，這將導(dǎo)致超越人類的數(shù)字AI，極大地推動(dòng)AI研究。

方法可以總結(jié)如下：

· 優(yōu)化算法，以實(shí)現(xiàn)更快、更智能的模型 

· 揭示AI「黑盒」行為的洞見

· 設(shè)計(jì)更好的架構(gòu)，無需無盡的試錯(cuò) 

· 加速數(shù)據(jù)分析，以實(shí)現(xiàn)更快的突破

因此，這就導(dǎo)致我們通向AGI，產(chǎn)生超級智能。幾年內(nèi)，AI就將產(chǎn)生人類無法理解的高級數(shù)學(xué)。

圖片

具體來說，DeepSeek-Prover-V2專門用于Lean 4中的形式化定理證明。

其中，初始化數(shù)據(jù)是通過DeepSeek-V3驅(qū)動(dòng)的遞歸定理證明流程來收集的。

冷啟動(dòng)訓(xùn)練過程中，會(huì)首先提示DeepSeek-V3將復(fù)雜問題分解為一系列子目標(biāo)，然后將已解決子目標(biāo)的證明合成為思維鏈過程，并結(jié)合DeepSeek-V3的逐步推理，為強(qiáng)化學(xué)習(xí)提供了一個(gè)初始冷啟動(dòng)。

通過這個(gè)過程，非正式和正式的數(shù)學(xué)推理就能集成到一個(gè)統(tǒng)一的模型中。

圖片

總結(jié)來說，亮點(diǎn)如下。

• 生成冷啟動(dòng)推理數(shù)據(jù)：遞歸證明搜索方法

為構(gòu)建冷啟動(dòng)數(shù)據(jù)集，團(tuán)隊(duì)開發(fā)了一個(gè)簡單而有效的遞歸定理證明流程，利用 DeepSeek-V3作為統(tǒng)一工具，進(jìn)行子目標(biāo)分解和形式化。

DeepSeek-V3會(huì)被提示，將定理分解為高層次的證明草圖。同時(shí)，在Lean 4中形式化這些證明步驟，從而產(chǎn)生一系列子目標(biāo)。

首先使用一個(gè)較小的 7B 模型來處理每個(gè)子目標(biāo)的證明搜索，以此降低計(jì)算負(fù)擔(dān)。

一旦具有挑戰(zhàn)性的問題的分解步驟得到解決，就將完整的逐步形式化證明與DeepSeek-V3產(chǎn)生的相應(yīng)思維鏈過程相結(jié)合，從而生成冷啟動(dòng)推理數(shù)據(jù)。

• 基于合成冷啟動(dòng)數(shù)據(jù)的強(qiáng)化學(xué)習(xí)

團(tuán)隊(duì)精心挑選了一個(gè)具有挑戰(zhàn)性的問題子集——它們無法通過7B prover以端到端的方式解決，但分解后的所有子目標(biāo)都已成功解決。

通過整合所有子目標(biāo)的證明，團(tuán)隊(duì)為原始問題構(gòu)建了一個(gè)完整的形式化證明。

然后，將此證明附加到DeepSeek-V3的思維鏈中，該思維鏈概述了相應(yīng)的引理分解，從而將非正式推理與后續(xù)形式化過程有機(jī)結(jié)合。

在合成冷啟動(dòng)數(shù)據(jù)上微調(diào)prover模型后，團(tuán)隊(duì)執(zhí)行了強(qiáng)化學(xué)習(xí)階段，以進(jìn)一步增強(qiáng)其連接非正式推理與形式化證明構(gòu)建的能力。

根據(jù)推理模型的標(biāo)準(zhǔn)訓(xùn)練目標(biāo)，采用二元正確/不正確反饋?zhàn)鳛橹饕莫?jiǎng)勵(lì)監(jiān)督形式。

最終，模型DeepSeek-Prover-V2-671B在神經(jīng)定理證明方面實(shí)現(xiàn)了當(dāng)前最優(yōu)的性能，在MiniF2F-test上達(dá)到了88.9%的通過率，并解決了PutnamBench中658個(gè)問題中的49個(gè)。

DeepSeek-Prover-V2為miniF2F數(shù)據(jù)集生成的證明：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip

• ·針對AIME與教科書題目的形式化數(shù)據(jù)集ProverBench

ProverBench是一個(gè)包含325道題目的基準(zhǔn)數(shù)據(jù)集。

其中，15道題目源自最近AIME競賽（AIME 24&25）中的數(shù)論和代數(shù)題目，提供了極具挑戰(zhàn)性的高中競賽級別題目。

剩余的310道題目則來自精選的教科書例題和教學(xué)教程，構(gòu)建了一個(gè)多樣化的、具有教學(xué)意義的形式化數(shù)學(xué)題目集合。

因此，這項(xiàng)基準(zhǔn)更全面地評估高中競賽和本科階段的數(shù)學(xué)水平。

圖片

DeepSeek-Prover-V2

在論文中，團(tuán)隊(duì)構(gòu)建了用于子目標(biāo)分解的推理模型，利用合成的冷啟動(dòng)數(shù)據(jù)和大規(guī)模強(qiáng)化學(xué)習(xí)技術(shù)來提升其性能。

通過子目標(biāo)分解實(shí)現(xiàn)遞歸式證明搜索

將復(fù)雜定理的證明過程拆解為一系列較小的引理，作為中間步驟，是人類數(shù)學(xué)家普遍采用的一種高效策略。

近年來，分層式方法在神經(jīng)定理證明領(lǐng)域得到了廣泛應(yīng)用。它的核心思路是借助現(xiàn)代大型語言模型（LLM）擅長的非形式化推理能力，來提升定理證明搜索的效率。

這部分包括3階段：從自然語言推理到形式化證明草圖、子目標(biāo)的遞歸求解、基于子目標(biāo)的定理證明中的課程學(xué)習(xí)。

首先提示DeepSeek-V3，同時(shí)生成自然語言形式的證明草圖，并將其形式化為Lean語言中的定理陳述，其中對于尚未證明的部分使用sorry占位。

接著，7B證明模型用于遞歸地求解被分解出的各個(gè)子目標(biāo)。通過組合這些子目標(biāo)的證明內(nèi)容，團(tuán)隊(duì)可以構(gòu)建出原始復(fù)雜問題的完整形式化證明。

冷啟動(dòng)數(shù)據(jù)收集流程概覽

DeepSeek利用子目標(biāo)來擴(kuò)展可用于模型訓(xùn)練的形式化定理范圍。

他們生成了兩種類型的子目標(biāo)定理：一種包含前序子目標(biāo)作為前提條件（對應(yīng)圖 3(b)），另一種則不包含前提條件（對應(yīng)圖 3(a)）。

這兩種類型的子目標(biāo)都被納入到專家迭代階段，形成一個(gè)漸進(jìn)式的課程體系，引導(dǎo)證明模型逐步掌握解決精選難題的方法。

這一流程的核心思想與AlphaProof 在測試階段采用的強(qiáng)化學(xué)習(xí)策略類似：生成目標(biāo)問題的多種變體，提升模型解決高難度的IMO級別問題的能力。

圖片

將分解后的子目標(biāo)轉(zhuǎn)化為一系列引理（lemma）陳述

首先執(zhí)行步驟 (a)：將原始目標(biāo)狀態(tài)替換為當(dāng)前子目標(biāo)。

接著進(jìn)行步驟 (b)：將之前的子目標(biāo)作為前提條件納入當(dāng)前引理中。

類型 (b) 的陳述用于遞歸求解復(fù)雜問題，而類型 (a) 和 (b) 的陳述都被納入課程學(xué)習(xí)流程中，用于訓(xùn)練模型逐步掌握推理能力。

最后，將這個(gè)組合后的正式證明附加到 DeepSeek-V3最初生成的「思維鏈」之上，形成高質(zhì)量的冷啟動(dòng)訓(xùn)練數(shù)據(jù)，用于支持形式化數(shù)學(xué)推理的學(xué)習(xí)。

統(tǒng)一非形式化推理與形式化證明

算法框架包括兩個(gè)階段，分別依賴兩個(gè)互補(bǔ)模型：用于引理分解的 DeepSeek-V3，以及用于補(bǔ)全具體形式化證明細(xì)節(jié)的7B證明模型。

這種方法巧妙地融合了高層次的自然語言推理和低層次的精確證明過程，為構(gòu)建可用于訓(xùn)練的形式化推理數(shù)據(jù)提供了重要基礎(chǔ)。

· 用合成數(shù)據(jù)實(shí)現(xiàn)冷啟動(dòng)

在研究過程中，DeepSeek挑選出一些特別難解決的問題。

這些問題很棘手，即便用7B證明模型，也沒辦法從頭到尾直接解決。

不過有意思的是，把這些問題拆解成一個(gè)個(gè)小目標(biāo)后，每個(gè)小目標(biāo)都能被成功證明。就像拼拼圖一樣，把這些小目標(biāo)的證明過程按順序組合起來，就能得到原始難題的完整證明，而且這個(gè)證明是非常嚴(yán)謹(jǐn)、規(guī)范的形式化證明。

圖片

接著，DeepSeek把這個(gè)完整的證明，添加到 DeepSeek-V3 生成的 「思維鏈」 里。

這里的 「思維鏈」 就像是解題的思路草稿，詳細(xì)記錄了把難題分解成小目標(biāo)的過程。

這樣一來，DeepSeek就得到了一份特殊的證明樣本，它既有像日常思考那樣的非形式化推理過程，又有嚴(yán)謹(jǐn)?shù)男问交C明步驟，兩者完美結(jié)合。

通過這種方式，團(tuán)隊(duì)成功收集到了幾百條高質(zhì)量的數(shù)據(jù)。

它們非常重要，是訓(xùn)練 DeepSeek-Prover-V2模型的基礎(chǔ)。

這里方法的核心是把日常語言描述的證明過程，直接轉(zhuǎn)化成有邏輯結(jié)構(gòu)的形式化框架。

· 用強(qiáng)化學(xué)習(xí)提升推理能力

用冷啟動(dòng)合成數(shù)據(jù)對證明模型進(jìn)行初步優(yōu)化后，就進(jìn)入了強(qiáng)化學(xué)習(xí)階段。

強(qiáng)化學(xué)習(xí)階段目的是讓模型更好地把日常語言的推理過程，轉(zhuǎn)化成嚴(yán)謹(jǐn)?shù)男问交C明。

在這個(gè)過程中，按照標(biāo)準(zhǔn)的推理模型訓(xùn)練要求，用 「正確」 或 「錯(cuò)誤」 這兩種簡單的反饋，作為主要的獎(jiǎng)勵(lì)監(jiān)督信號。也就是說，如果模型給出的證明是對的，就獎(jiǎng)勵(lì)它；如果錯(cuò)了，就不給獎(jiǎng)勵(lì)。

但訓(xùn)練有個(gè)問題：模型生成的證明結(jié)構(gòu)，經(jīng)常和 「思維鏈」 里分解問題的思路對不上。

為了解決這個(gè)問題，在訓(xùn)練剛開始的時(shí)候，團(tuán)隊(duì)就加入了一種新的獎(jiǎng)勵(lì)機(jī)制，專門用來懲罰那些和分解結(jié)構(gòu)不一致的輸出結(jié)果。

在實(shí)際訓(xùn)練中，這個(gè)保證結(jié)構(gòu)一致的方法效果非常好，大大提高了證明的準(zhǔn)確率。尤其是在證明那些需要很多步驟、特別復(fù)雜的定理時(shí)，優(yōu)勢更加明顯。

訓(xùn)練細(xì)節(jié)

DeepSeek-Prover-V2的訓(xùn)練采用了兩階段策略，建立了兩種互補(bǔ)的證明生成模式：

• 高效率非思維鏈（non-CoT）模式：優(yōu)化用于快速生成Lean形式化代碼，重點(diǎn)在于輸出簡潔、高效的證明，不包含顯式的中間推理步驟
• 高精度思維鏈（CoT）模式：注重系統(tǒng)化表達(dá)推理過程，逐步構(gòu)建邏輯清晰的中間步驟，最后生成完整的形式化證明

這兩個(gè)生成模式的設(shè)計(jì)延續(xù)了DeepSeek-Prover-V1.5的思路，區(qū)別在于不同的提示模板。

在第一階段中，團(tuán)隊(duì)結(jié)合課程學(xué)習(xí)框架和專家迭代機(jī)制，訓(xùn)練non-CoT證明模型，并通過子目標(biāo)分解遞歸地合成復(fù)雜問題的證明。

由于non-CoT模式推理速度快、驗(yàn)證成本低，因此非常適合快速迭代與數(shù)據(jù)采集。

在此基礎(chǔ)上，第二階段引入了冷啟動(dòng)的思維鏈數(shù)據(jù)，這些數(shù)據(jù)整合了DeepSeek-V3的高級數(shù)學(xué)推理能力與合成的形式化證明。

CoT模式隨后進(jìn)入強(qiáng)化學(xué)習(xí)階段，以進(jìn)一步提升模型在推理和形式化構(gòu)造之間的銜接能力。

專家迭代（Expert Iteration）

DeepSeek-Prover-V2的non-CoT模型訓(xùn)練采用了「專家迭代」方法，這是目前形式化定理證明系統(tǒng)中廣泛使用的訓(xùn)練范式。

圖片

論文鏈接：https://arxiv.org/abs/2009.03393

每輪訓(xùn)練中，當(dāng)前性能最好的模型會(huì)嘗試解決前幾輪未成功證明的難題。

成功的證明結(jié)果經(jīng)Lean系統(tǒng)驗(yàn)證后被加入監(jiān)督微調(diào)（SFT）數(shù)據(jù)集中，用于訓(xùn)練下一代更強(qiáng)的模型。

這個(gè)過程不僅讓模型持續(xù)從初始演示數(shù)據(jù)中學(xué)習(xí)，還能提煉自身的成功推理路徑，不斷優(yōu)化解決難題的能力。

DeepSeek-Prover-V2整體訓(xùn)練流程與V1和V1.5保持一致，只在訓(xùn)練問題的分布上做了兩處改進(jìn)：

• 加入更多來自自動(dòng)形式化和開源數(shù)據(jù)集的題目，擴(kuò)大訓(xùn)練覆蓋范圍
• 加入基于子目標(biāo)分解生成的題目，尤其針對MiniF2F基準(zhǔn)數(shù)據(jù)集中驗(yàn)證集的高難度問題

監(jiān)督微調(diào)（Supervised Fine-tuning）

團(tuán)隊(duì)在DeepSeek-V3-Base-671B的基礎(chǔ)上進(jìn)行微調(diào)，學(xué)習(xí)率設(shè)置為常數(shù)5e-6，最大上下文長度為16,384 token。

訓(xùn)練數(shù)據(jù)來自兩個(gè)來源：

• non-CoT數(shù)據(jù)：由專家迭代生成，強(qiáng)調(diào)高效生成Lean代碼，但不包含推理過程
• 冷啟動(dòng)CoT數(shù)據(jù)：來自DeepSeek-V3的高階數(shù)學(xué)推理，通過形式化草圖展現(xiàn)清晰的推理路徑

non-CoT數(shù)據(jù)強(qiáng)化模型在Lean生態(tài)中的形式驗(yàn)證能力，而CoT數(shù)據(jù)則更強(qiáng)調(diào)將數(shù)學(xué)直覺轉(zhuǎn)化為結(jié)構(gòu)化形式證明的過程。

強(qiáng)化學(xué)習(xí)（Reinforcement Learning）

DeepSeek采用了Group Relative Policy Optimization（GRPO）作為強(qiáng)化學(xué)習(xí)算法。

GRPO不需要單獨(dú)的價(jià)值評估模型，而是通過對每道題采樣多個(gè)候選證明，并基于相對獎(jiǎng)勵(lì)進(jìn)行策略優(yōu)化。

訓(xùn)練時(shí)，我們使用二元獎(jiǎng)勵(lì)機(jī)制Lean驗(yàn)證成功則得分1，失敗則為0。

為了確保訓(xùn)練有效性，團(tuán)隊(duì)精心挑選了具有挑戰(zhàn)性但又可解的題目作為訓(xùn)練提示。

在每輪訓(xùn)練中，隨機(jī)選取256道不同題目，每道題生成32個(gè)候選證明，最大序列長度為32,768 token。

蒸餾與小模型訓(xùn)練（Distillation）

團(tuán)隊(duì)將DeepSeek-Prover-V1.5-Base-7B的最大上下文長度從4,096擴(kuò)展到32,768 token，并利用在671B模型強(qiáng)化學(xué)習(xí)階段采集的rollout數(shù)據(jù)對模型進(jìn)行微調(diào)。

在CoT模式之外，團(tuán)隊(duì)還加入了專家迭代期間采集的non-CoT數(shù)據(jù)，旨在讓小模型具備成本更低的證明能力，能夠快速輸出精煉的形式化結(jié)果。

此外，團(tuán)隊(duì)也在7B小模型上執(zhí)行與671B模型相同的強(qiáng)化學(xué)習(xí)流程。

實(shí)驗(yàn)結(jié)果

MiniF2F基準(zhǔn)測試結(jié)果

MiniF2F包含488個(gè)形式化的題目，來源包括AIME、AMC和IMO等競賽，以及MATH數(shù)據(jù)集，涵蓋了初等數(shù)學(xué)的核心領(lǐng)域，如代數(shù)、數(shù)論和歸納法。

這些題目被分為兩個(gè)大小相等的子集，即miniF2F-valid和miniF2F-test，每個(gè)子集包含244道題目，并且在各個(gè)學(xué)科領(lǐng)域具有相同的分布。

如表1所示，實(shí)驗(yàn)結(jié)果表明，DeepSeek-Prover-V2-671B在miniF2F-test基準(zhǔn)上取得了SOTA性能，當(dāng)采用CoT生成策略時(shí)，僅用32個(gè)樣本便達(dá)到了前所未有的82.4%的準(zhǔn)確率。

值得注意的是，參數(shù)效率更高的DeepSeek-Prover-V2-7B也展現(xiàn)出了很強(qiáng)的競爭力，超越了現(xiàn)有文獻(xiàn)中的所有開源定理證明器。

他們還發(fā)現(xiàn)了一個(gè)明顯的規(guī)律：隨著樣本預(yù)算從1增加到8192，7B和671B模型之間的性能差距顯著擴(kuò)大，更大規(guī)模的模型展現(xiàn)出更高的樣本效率和更快的性能提升。

圖片

• 子目標(biāo)引導(dǎo)的課程學(xué)習(xí)在難題證明中的應(yīng)用

表2詳細(xì)展示了DeepSeek-Prover-V2在miniF2F基準(zhǔn)測試中的解題情況，其在驗(yàn)證集和測試集上分別取得了91.0%和88.9%的高通過率。

值得注意的是，團(tuán)隊(duì)提出了子目標(biāo)引導(dǎo)的課程學(xué)習(xí)框架，將通用模型DeepSeek-V3與輕量級專用7B prover相結(jié)合，在miniF2F-valid上實(shí)現(xiàn)了90.2%的成功率，與DeepSeekProver-V2-671B的性能幾乎持平。

這些發(fā)現(xiàn)表明，SOTA的通用LLM不僅能進(jìn)行自然語言理解，還能有效支持復(fù)雜的形式推理任務(wù)。

通過巧妙的子目標(biāo)分解，模型便可將難題分解為一系列可處理的步驟，從而有效連接非正式推理與形式化證明構(gòu)建。

圖片

CoT vs. non-CoT

表1的實(shí)驗(yàn)結(jié)果表明，在形式化數(shù)學(xué)推理中，CoT推理模式相比non-CoT模式具有顯著的性能優(yōu)勢。

這進(jìn)一步驗(yàn)證了CoT提示的有效性，它鼓勵(lì)將復(fù)雜問題分解為中間步驟，并證實(shí)了推理時(shí)擴(kuò)展在形式化定理證明領(lǐng)域依然適用。

作為補(bǔ)充，表3提供了DeepSeek-Prover-V2在不同推理模式下生成的token數(shù)量的統(tǒng)計(jì)信息。

正如預(yù)期的那樣，CoT模式會(huì)生成明顯更長的輸出，反映了其復(fù)雜的推理過程。

有趣的是，在non-CoT設(shè)置下，671B模型生成的平均輸出長度比7B模型更長。

更仔細(xì)的分析表明，盡管non-CoT模式下沒有顯式推理提示，但較大規(guī)模的模型通常會(huì)在證明代碼中插入簡短的自然語言注釋，這些注釋類似于隱式推理步驟。

這表明，即使沒有顯式的CoT提示，高容量模型也可能在內(nèi)部和外部隱式地執(zhí)行中間推理。

圖片

本科水平基準(zhǔn)測試結(jié)果

• ProofNet 

ProofNet包含371道使用Lean 3編寫的題目，這些題目選自一系列流行的本科純數(shù)學(xué)教材，涵蓋了實(shí)分析、復(fù)分析、線性代數(shù)、抽象代數(shù)和拓?fù)涞戎黝}。

表4的結(jié)果顯示，相比于non-CoT設(shè)置，采用CoT推理時(shí)DeepSeek-Prover-V2的通過率得到了顯著提升。

盡管訓(xùn)練數(shù)據(jù)主要源自高中數(shù)學(xué)，但該模型在更高級的大學(xué)數(shù)學(xué)問題上展現(xiàn)出了強(qiáng)大的泛化能力，代表著強(qiáng)大的形式推理能力。

• PutnamBench

PutnamBench基準(zhǔn)測試集包含了1962年至2023年普特南數(shù)學(xué)競賽中的數(shù)學(xué)題。

它是美國和加拿大極負(fù)盛名的年度本科生數(shù)學(xué)競賽，涵蓋分析、線性代數(shù)、抽象代數(shù)、組合數(shù)學(xué)、概率論和集合論等多個(gè)大學(xué)領(lǐng)域的知識。

如表4所示，DeepSeek-Prover-V2-671B在PutnamBench中展現(xiàn)了增強(qiáng)的推理能力，解決了49道題目，并顯著優(yōu)于其non-CoT版本。

這說明，CoT推理方法已經(jīng)可以有效處理極有挑戰(zhàn)性的大學(xué)數(shù)學(xué)問題。

圖片

• RL實(shí)現(xiàn)的技能發(fā)現(xiàn)：7B勝過671B！

此外，團(tuán)隊(duì)意外地發(fā)現(xiàn)：DeepSeek-Prover-V2-7B在PutnamBench數(shù)據(jù)集上采用non-CoT生成模式時(shí)，也表現(xiàn)出了卓越的性能。

更令人稱奇的是，這個(gè)較小的7B模型成功解決了DeepSeek-Prover-V2-671B仍未能解決的13道題！

這是為什么？

仔細(xì)分析模型的輸出后，團(tuán)隊(duì)從中發(fā)現(xiàn)了一種獨(dú)特的推理模式——

7B模型經(jīng)常使用Cardinal.toNat和Cardinal.natCast_inj來處理涉及有限基數(shù)的問題，而671B模型生成的輸出中明顯缺少這種處理方式。

似乎就是這種技術(shù)，讓7B能有效解決需要精細(xì)操作基數(shù)值的問題。

組合問題測試結(jié)果

CombiBench是一個(gè)綜合性的基準(zhǔn)測試集，其中包含了100道用Lean 4形式化表示的組合競賽題，配有自然語言描述。

團(tuán)隊(duì)采用with-solution設(shè)置，此時(shí)正確的答案已嵌入在Lean代碼中，因此評估可以完全集中在證明過程的生成上。

對其中77道題進(jìn)行評估后，模型成功解決了12道。

結(jié)果表明，盡管該P(yáng)rover模型主要在數(shù)論和代數(shù)領(lǐng)域進(jìn)行訓(xùn)練，但在組合問題上也展現(xiàn)出了良好的泛化潛力，即使這些問題相當(dāng)難。

ProverBench數(shù)據(jù)集

為了增強(qiáng)現(xiàn)有基準(zhǔn)，團(tuán)隊(duì)構(gòu)建了一個(gè)包含325道題目的基準(zhǔn)數(shù)據(jù)集。

其中，15道題目來自AIME 24和25中的數(shù)論和代數(shù)題目，屬于極難的高中競賽級別題目。剩余的310道題目則來自精選的教科書例題和教學(xué)教程。

這就能更全面評估高中競賽和本科階段的數(shù)學(xué)水平。

• AIME題目形式化

美國數(shù)學(xué)邀請賽AIME 24&25中的題目，已成為評估LLM推理能力的常用基準(zhǔn)。

為了彌合模型在形式化和非形式化數(shù)學(xué)推理能力評估上的差異，我們整理并形式化了AIME 24&25中的部分題目，并排除了幾何、組合和計(jì)數(shù)問題，因?yàn)樗鼈冊贚ean中的表示較復(fù)雜。

最終，團(tuán)隊(duì)選擇了15道題目，涵蓋了初等數(shù)論和代數(shù)中競賽級別的知識點(diǎn)。

結(jié)果顯示，DeepSeek-V3-0324成功解決了15道題中的8道題。

而DeepSeek-Prover-V2-671B在已知正確答案的前提下，能夠?yàn)?5道題目中的6道構(gòu)建出有效的形式化證明。

這種表明，非形式化數(shù)學(xué)推理與形式化定理證明的性能差距正在顯著縮小，高級語言模型在語言理解和形式邏輯的嚴(yán)謹(jǐn)性上正日益接近。

• ·教科書題目形式化

除了AIME 24&25之外，團(tuán)隊(duì)還從高中競賽和本科課程教材中挑出題目來擴(kuò)充基準(zhǔn)測試集。

最終，他們形式化了310道題，難度范圍很廣，覆蓋了競賽級別的初等數(shù)學(xué)到本科常見的高級主題。

如表6所示，結(jié)果表明，采用CoT推理的DeepSeek-Prover-V2-671B始終優(yōu)于所有基線模型，與在其他基準(zhǔn)測試中的表現(xiàn)一致。

圖片

在論文最后，團(tuán)隊(duì)表示，未來的工作將著重于將范例擴(kuò)展到類似AlphaProof的系統(tǒng)。

最終目標(biāo)，就是解決代表自動(dòng)定理證明領(lǐng)域前沿的IMO級數(shù)學(xué)難題！

快速開始

我們可以直接使用Hugging Face的Transformers庫進(jìn)行模型推理。

以下是如何生成miniF2F數(shù)據(jù)集中問題證明的一個(gè)簡單示例：

from transformers import AutoModelForCausalLM, Autotokenizer
import torch
torch.manual_seed(30)
model_id = "DeepSeek-Prover-V2-7B"  # or DeepSeek-Prover-V2-671B
tokenizer = Autotokenizer.from_pretrained(model_id)
formal_statement = """
import Mathlib
import Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
/-- What is the positive difference between $120\%$ of 30 and $130\%$ of 20? Show that it is 10.-/
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 outlining the main proof steps and strategies.
The plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.
""".strip()
chat = [
  {"role": "user", "content": prompt.format(formal_statement)},
]
model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
inputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors="pt").to(model.device)
import time
start = time.time()
outputs = model.generate(inputs, max_new_token=8192)
print(tokenizer.batch_decode(outputs))
print(time.time() - start)

參考資料：https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main