DeepSeek推出了DeepSeek-Prover-V2，這是一款開源大型語言模型 (LLM)，專為 Lean 4 框架內的形式化定理證明這一複雜領域所精心打造。這款新模型利用遞迴定理證明流程，充分利用 DeepSeek 最新的 DeepSeek-V3 基礎模型的力量。Lean 4 是 Lean 定理證明器的最新版本，是由 Microsoft Research 開發的互動式證明助理。這種複雜的函數式編程語言和互動式定理證明系統使數學家和計算機科學家能夠構建具有無與倫比的機器檢查驗證的形式化證明。
該項目標誌著在彌合形式和非形式數學推理之間的差距方面邁出了重要一步。透過充分利用通用 LLM 的固有能力，它旨在有效地解決形式化定理證明的結構化領域。 DeepSeek 研究團隊認為，他們創新的方法反映了人類數學家在構建證明時所採用的認知過程，將複雜的定理精確地分解為更易於管理和理解的組成部分。
擴展評估框架：引入 ProverBench
為了提高研究的嚴謹性，DeepSeek 團隊採取了一項重要舉措，透過推出 ProverBench 來顯著擴展其評估框架，ProverBench 是一個全新的基準集合，專為全面評估形式化定理證明能力而精心設計。這個全面的集合可作為評估 LLM 在形式數學環境中表現的寶貴資源。
「除了傳統的基準之外，我們自豪地推出 ProverBench，這是一個精心策劃的包含 325 個形式化問題的集合，旨在豐富我們的評估過程。該集合包括 15 個精心挑選的問題，這些問題直接來自最近的美國邀請數學考試 (American Invitational Mathematics Examination, AIME) 競賽，特別是來自 24-25 年，」研究人員詳細說明。
在 ProverBench 資料集中包含 AIME 問題尤其值得注意，因為它引入了一組具有挑戰性且廣為人知的數學問題，這些問題在數學界得到廣泛認可。這為評估 DeepSeek-Prover-V2 的表現並將其與其他方法進行比較提供了標準化和嚴格的依據。
有希望的初步結果：解決 AIME 問題
對這些具有挑戰性的 AIME 問題進行嚴格測試所產生的初步結果顯示，他們精心設計的專用定理證明模型表現出了非常出色的性能。 DeepSeek 團隊自豪地報告說，DeepSeek-Prover-V2 透過成功解決了提交給它的 15 個 AIME 問題中的 6 個，展現了它的實力。相比之下，通用 DeepSeek-V3 模型在使用多數投票技術時成功解決了 8 個問題。
這些發現突顯了專用和通用 LLM 在解決複雜數學問題方面的潛力。雖然通用模型在這個特定基準中表現出略高的成功率，但專用定理證明模型展示了其在形式數學推理方面的能力。
模仿人類證明建構：一種思維鏈式方法
「鑑於通用模型在嘗試產生完整的 Lean 證明時經常遇到的眾所周知的挑戰，我們策略性地指示 DeepSeek-V3 僅產生高階證明草圖，故意省略複雜的細節。由此產生的思維鏈最終會產生一個 Lean 定理，該定理由一系列 have 語句組成，每個語句都以一個 sorry 佔位符作為結論，有效地指示需要解決的子目標。這種創新的方法優雅地模仿了人類的證明建構風格，在這種風格中，複雜的定理被逐步簡化為一系列更易於管理的引理，」DeepSeek 團隊詳細說明。
這種產生高階證明草圖的創新方法與數學家通常解決複雜證明的方式一致。透過專注於整體結構和關鍵步驟，該模型可以有效地指導後續的細化和完成證明。
有條不紊的策略：個別解決每個證明組成部分
然後，該系統有條不紊地採用一種有條理且結構化的策略來解決證明的每個單獨組成部分。這種系統化的方法確保嚴謹地考慮證明的每個方面，並以一種邏輯和一致的方式加以解決。該系統創建了一種高度結構化的定理證明方法，在先前建立的結果之上構建，以確保每個後續步驟都有堅實的基礎。
「利用 DeepSeek-V3 產生的子目標，我們採用遞迴求解策略來系統地解決每個中間證明步驟。我們從 have 語句中提取子目標表達式，以將它們替換為給定問題中的原始目標，然後將前面的子目標作為前提納入。這種結構使後續子目標能夠使用早期步驟的中間結果來解決，從而促進更局部化的依賴結構並促進更簡單引理的開發，」研究人員詳細說明。
遞迴求解策略是該系統處理複雜證明能力的一個關鍵方面。透過將問題分解為更小、更易於管理的子目標，該系統可以有效地將其推理能力應用於每個單獨的組成部分。
優化計算資源：一個專用的 7B 參數模型
為了有效地優化計算資源並確保高效處理，該系統策略性地採用一個較小的、高度專用的 7B 參數模型來處理分解的引理。這種方法對於有效管理與廣泛證明搜索相關的計算需求至關重要，確保系統能夠高效運行，而不會被搜索空間的複雜性所淹沒。當所有分解步驟都成功解決時，該方法最終會自動導出完整的證明。
「該演算法框架分兩個不同的階段運行，利用兩個互補的模型：DeepSeek-V3 用於引理分解，一個 7B 證明器模型用於填寫相應的形式證明細節，」研究人員描述說。
這種兩階段方法允許系統利用大型通用模型和較小專用模型的優勢。大型模型用於產生高階證明草圖，而較小模型用於填寫細節並完成形式證明。
合成形式推理數據：一條自然的途徑
這種精心設計的架構有效地建立了一條自然且直觀的途徑，用於合成形式推理數據，將高階數學推理與形式驗證的嚴格要求無縫融合。這種整合對於確保系統結果的可靠性和可信度至關重要。
「我們策劃了一個具有挑戰性的問題子集，這些問題無法由 7B 證明器模型以端到端的方式解決，但所有分解的子目標都已成功解決。透過組合所有子目標的證明，我們為原始問題構建了一個完整的的形式證明，」研究人員解釋說。
這種方法允許系統從錯誤中學習，並提高其解決複雜問題的能力。透過識別出導致困難的特定子目標，系統可以將其努力集中在提高其在這些領域的表現上。
疑慮和挑戰：實施細節受到審查
儘管 DeepSeek-Prover-V2 展示了不可否認的技術成就，但該領域的一些專家對某些實施細節提出了相關疑慮。Epoch AI 的一位備受尊敬的首席數學家 Elliot Glazer 指出了值得進一步調查的潛在問題。
對於 DeepSeek-Prover-V2 論文的一些疑慮。可能存在錯誤形式化的例子，而且關於 Lean zulip 的討論表明 PutnamBench 證明是無稽之談，並使用了一個隱含的 sorry (可能隱藏在 apply? tactic 中)，這並沒有在他們的 read-eval-print-loop 中報告。
這些疑慮生動地突出了形式驗證領域中固有的持續挑戰，即使是最微小和看似微不足道的實施細節也會對結果的總體有效性和可靠性產生不成比例的巨大影響。形式驗證過程需要毫不動搖地關注細節，並嚴格遵守既定標準。
PutnamBench 證明中存在錯誤形式化的例子以及可能隱藏的 "sorry" 策略，這些都引發了關於驗證過程的嚴謹性和完整性的重要問題。這些疑慮突顯了繼續審查和獨立驗證結果的必要性。
可用性和資源：普及形式定理證明的途徑
DeepSeek 提供了兩種不同模型大小的 Prover-V2，以滿足各種計算資源和研究目標的需求。第一個版本是一個建立在他們之前的 Prover-V1.5-Base 之上的 7B 參數模型，具有擴展的上下文長度，最多可達 32K 個 token。第二個版本是一個大得多的 671B 參數模型，基於 DeepSeek-V3-Base 進行訓練。現在，這兩個模型都可以在 HuggingFace 上輕鬆訪問，HuggingFace 是一個領先的共享和協作機器學習模型的平台。
除了模型本身之外，DeepSeek 還在 HuggingFace 上提供了完整的 ProverBench 資料集，其中包含 325 個精心形式化的問題，用於評估目的。這個全面的資料集為研究人員和開發人員提供了一種寶貴的資源，用於評估其模型的表現並將其與 DeepSeek-Prover-V2 進行比較。
透過免費提供這些資源，DeepSeek 正在普及形式定理證明技術的途徑，並促進研究社群內的協作。這種開源方法可能會加速該領域的進展，並帶來自動推理和驗證方面的新突破。
此版本為研究人員和開發人員提供了深入研究此技術的功能和限制所需的資源。DeepSeek 透過開放訪問模型和 ProverBench 資料集，鼓勵進一步的探索和協作努力，以解決該領域專家提出的疑慮。這種協作方法是解開形式定理證明的複雜性並鞏固這些突破性進展的可靠性的關鍵。