Deepseek 放出了 DeepSeek-Prover-V2 的詳細論文

藏師傅做了 DeepSeek-Prover-V2 一圖流幫你了解這個模型

詳細總結分析一下：

Prover-V2 是一個專為 Lean 4 形式化定理證明設計的開源大型語言模型。
其核心目標是利用強化學習進行子目標分解，從而提升形式化數學推理能力。

核心方法與創新：

1??遞歸定理證明流水線:
利用通用的 DeepSeek-V3 模型將復雜問題分解為一系列子目標
DeepSeek-V3 同時生成自然語言的證明草圖 和對應的 Lean 4 形式化語句框架。

2??子目標解決與合成 :
使用一個較小的 7B 參數的 Prover 模型遞歸地解決由 DeepSeek-V3 分解出的子目標。
將已解決的子目標證明組合起來，構建原始復雜問題的完整形式化證明。

3??冷啟動數據生成:
將 DeepSeek-V3 生成的鏈式思考過程與最終合成的完整形式化證明配對。
這種方法生成了高質量的、結合了非形式化推理和形式化證明的初始訓練數據。

4??強化學習:
在冷啟動數據微調的基礎上，使用 GRPO 算法進行強化學習。
獎勵機制：主要使用二元獎勵（證明正確為 1，錯誤為 0）。在早期訓練中加入一致性獎勵，鼓勵模型生成的證明結構與 CoT 中的子目標分解保持一致。

5??課程學習:
利用分解出的子目標生成不同難度的定理，逐步增加訓練任務的難度，引導模型學習。

模型與訓練：

主要模型: DeepSeek-Prover-V2-671B (6710億參數)
小型模型: DeepSeek-Prover-V2-7B (70億參數，通過蒸餾 671B 模型的 RL 數據得到)
基礎模型: DeepSeek-V3 (用于初始分解和 CoT)
訓練流程:
第一階段 (非 CoT 模式): 使用專家迭代 (Expert Iteration) 和課程學習訓練非 CoT 模型，側重于快速生成簡潔的 Lean 代碼，同時通過子目標分解解決難題并收集數據。
第二階段 (CoT 模式): 使用合成的冷啟動 CoT 數據進行監督微調 ，然后進行強化學習，重點提升模型的推理過程和最終證明能力。

項目地址：github.com/deepseek-ai/DeepSeek-Prover-V2