總部位於中國杭州的人工智慧 (AI) 公司DeepSeek週三發布了其 Prover 模型的更新版本。它被稱為 DeepSeek-Prover-V2，是一個高度專業化的模型，專注於證明形式數學定理。大型語言模型（LLM）使用Lean 4程式語言，透過獨立分析每個步驟來檢查數學證明是否邏輯一致。與中國公司先前發布的版本類似，DeepSeek-Prover-V2 是一個開源模型，可以從 GitHub 和 Hugging Face 等流行的儲存庫下載。
DeepSeek 推出以數學為中心的全新 AI 模型
該人工智慧公司在其 GitHub列表頁面上詳細介紹了新模型。它本質上是一個以推理為中心的模型，具有可見的思路鏈（CoT），在數學領域中發揮作用。它是基於 2024 年 12 月發布的 DeepSeek-V3 AI 模型構建並提煉的。
DeepSeek-Prover-V2 可以以多種方式使用。它可以解決高中到大學程度的數學問題，並發現和修復數學定理證明中的錯誤。它還可以用作教學輔助工具，對證明進行逐步解釋，並幫助數學家和研究人員探索新的定理並證明其有效性。
它有兩種模型大小——70 億參數大小和更大的 6,710 億參數大小。後者是在 DeepSeek-V3-Base 上進行訓練的，而前者則建立在 DeepSeek-Prover-V1.5-Base 之上，上下文長度高達 32,000 個標記。
在預訓練過程中，研究人員透過促使基礎模型分解複雜問題實現了冷啟動訓練系統。這些問題構成了一系列子目標。然後，將已解決子目標的證明添加到 CoT 中，並與基礎模型的推理相結合，為強化學習創建初始冷啟動。
值得注意的是，除了 GitHub 之外，該 AI 型號還可以從 DeepSeek 的 Hugging Face清單中下載。 Prover-V2 模型強調了 AI 模型訓練過程的迭代變化如何顯著提高其專業能力。與其他開源模型發布類似，有關核心架構或更大資料集的細節尚不清楚。
Picture Source
tldv.io