DeepSeek釋出DeepSeek-Prover-V2：利用遞迴證明搜尋和新基準推進神經定理證明

DeepSeek AI宣佈釋出DeepSeek-Prover-V2，這是一個專為Lean 4環境中的形式定理證明設計的開源大型語言模型。該模型基於先前工作，引入了一種創新的遞迴定理證明管道，利用DeepSeek-V3生成高質量的初始化資料。最終模型在神經定理證明中達到了最先進水平，並同時推出了ProverBench，這是一個用於評估數學推理能力的新基準。

開創性的冷啟動推理資料生成

DeepSeek-Prover-V2的一個關鍵創新在於其獨特的冷啟動訓練過程。該過程首先提示強大的DeepSeek-V3模型將複雜數學定理分解為一系列更易處理的子目標。同時，DeepSeek-V3在Lean 4中形式化這些高階證明步驟，有效建立了子問題的結構化序列。

為了處理每個子目標的計算密集型證明搜尋，研究人員使用了較小的7B引數模型。一旦一個挑戰性問題的所有分解步驟都成功證明，完整的逐步形式證明將與DeepSeek-V3相應的思維鏈推理配對。這種巧妙的方法使模型能夠從整合了非正式高階數學推理和嚴格形式證明的綜合資料集中學習，為後續強化學習提供了強大的冷啟動。

用於增強推理的強化學習

在合成冷啟動資料的基礎上，DeepSeek團隊挑選了一組具有挑戰性的問題，這些問題7B證明器無法端到端解決，但所有子目標都已成功處理。透過結合這些子目標的形式證明，構建了原始問題的完整證明。然後將此形式證明與DeepSeek-V3關於引理分解的思維鏈概述連結，建立了一個統一的訓練示例，包含非正式推理和形式化。

證明器模型隨後在此合成資料上進行微調，隨後進入強化學習階段。該階段利用二元正確/錯誤反饋作為獎勵訊號，進一步最佳化模型彌合非正式數學直覺與精確形式證明構建之間差距的能力。

最先進的效能

這一創新訓練過程的成果是DeepSeek-Prover-V2–671B，一個擁有6710億引數的模型。該模型取得了顯著成果，在神經定理證明中展示了最先進的效能。它在MiniF2F測試中達到了88.9%的透過率，併成功解決了PutnamBench中658個問題中的49個。DeepSeek-Prover-V2為miniF2F資料集生成的證明可公開下載，以供進一步審查和分析。

引入ProverBench：新的評估標準

除了模型釋出，DeepSeek AI還推出了ProverBench，這是一個包含325個問題的新基準資料集。該基準旨在提供對不同難度級別數學推理能力的更全面評估。

ProverBench包括15個來自最近AIME（美國邀請數學考試）競賽（AIME 24和25）的形式化問題，提供了高中競賽級別的真實挑戰。其餘310個問題來自精選的教科書示例和教育教程，提供了涵蓋多個領域的多樣化且教學上合理的形式化數學問題集合。

ProverBench旨在促進對神經定理證明器在挑戰性競賽問題和基礎本科水平數學上的更全面評估。

可用性

DeepSeek AI以兩種模型規模釋出DeepSeek-Prover-V2，以適應不同的計算資源：7B引數模型和更大的671B引數模型。DeepSeek-Prover-V2–671B建立在DeepSeek-V3-Base的穩健基礎上。較小的DeepSeek-Prover-V2–7B建立在DeepSeek-Prover-V1.5-Base上，並具有高達32K令牌的擴充套件上下文長度，使其能夠處理更長更復雜的推理序列。

DeepSeek-Prover-V2的釋出和ProverBench的引入標誌著神經定理證明領域向前邁出了重要一步。透過利用遞迴證明搜尋管道並引入具有挑戰性的新基準，DeepSeek AI正在賦能社群開發和評估更復雜、更強大的形式數學AI系統。