DeepSeek-Prover-V2：專為 Lean 4 定理證明設計的開放原始碼大型語言模型 (https://github.com/...

Hacker News Active + 100 繁體中文

DeepSeek-Prover-V2 是一款開放原始碼大型語言模型，專注於 Lean 4 定理證明。其訓練流程採用 DeepSeek-V3 輔助遞迴式證明搜尋，先行拆解複雜問題為子目標(subgoals)，結合 DeepSeek-V3 的心智鏈 (chain-of-thought) 與形式化步驟產生 cold-start 資料，用以進行強化學習 (Reinforcement Learning)，將非形式化與形式化數學推理統整於一體。

訓練階段分為兩步：一是使用 7B 參數模型處理拆解後的子目標以降低運算成本，藉此合成完整證明與心智鏈，構建 cold-start 推理資料

二是在整理出一組微調後仍無法端對端解決但子目標皆已定式化的挑戰題後，將子目標證明串連成原題完整證明，並以二元正確或錯誤回饋作為獎勵函數進行強化學習

在 Hacker News 討論中，多位使用者認為 DeepSeek-Prover-V2 的子目標拆解機制直觀有助於複雜任務分解，並預見未來大型語言模型 (LLM) 或將演進為多個「專家」模型，各司其職並由封裝層 (wrapper) 調度；有回覆指出混合專家模型 (mixture-of-experts) 已有類似概念，也有人提到路由技術如 RouteLLM 或 OpenRouter 早已允許在不同域專家間切換