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系統。