對比閱讀DeepSeekMath-V2與V1的論文，筆者感覺V2是一次范式遷移，從追求“答案正確”轉向“過程正確”。

預處理

自然語言表述的數學問題作為輸入，將問題拆成“證明目標+前提或已知事實+約束”，序列化成prompt供生成器使用。

這樣可以把不同類型的數學任務歸一成“證明或推導任務”以便統一處理。

生成器

微調后的LLM生成模型作為“證明草稿生成器”，生成多條“逐步證明鏈”。

V1關注最終答案,而V2強制生成“逐步可檢驗”的中間證明步驟，以便于驗證器逐步檢驗。

驗證器

對每條候選證明進行逐步與整體連貫性的驗證，給出“是否通過”或“錯誤類型與定位”的判定。

驗證器是微調的LLM,不僅僅做二值判定，還會輸出“反例、缺失步驟、邏輯跳躍、錯誤應用的引理”等診斷信息，供生成器修正。

生成-驗證循環

可多輪驗證，即同一證明由多個驗證器實例或不同seed評估，用投票或置信度聚合結果，代價是compute增加。

驗證器的反饋作為訓練reward，或將通過驗證的證明作為正樣本，構造對比學習目標，促進生成器自我修正。

訓練與RL策略

訓練reward從V1“結果正確”轉為V2“步驟效用”。

為避免“生成器學會騙過驗證器”，需對驗證器做對抗訓練或多樣化，跨模型、跨seed、引入專家規則等。

測試時計算

在測試與推理時進行大規模采樣+并行驗證，使用篩選/聚合策略，例如合并相同結論的不同證明以增強置信。

??DeepSeek R1 & R2 技術原理???總結過，測試時計算能夠顯著提升高難度推理的成功率，但會消耗大量計算資源。

與Lean的差異

跟??DeepSeek-Prover??構建高質量的 Lean 證明語料庫，做形式化證明的思路不同，DeepSeekMath-V2 仍依賴概率語言模型，邏輯嚴謹性上可能存在盲區。

大量生成采樣與驗證提高置信，追求的仍然是統計上可靠，與Lean等形式化的語義級“機械”檢查，獲得可驗證、毫無歧義的證明，有本質不同。

技術走向預判

筆者覺得 V2之所以做出如此選擇，是出于強調可擴展的發現能力，在大規模數學語料和問題上自動生成候選，哲學上更接近數學家的實踐。

未來會不會探索中間路徑？比如先用V2發現并構造可能的證明路徑，再把被驗證器接受、結構良好的證明自動或半自動轉譯為proof script，

再由形式化內核做嚴格校驗，這樣可能把V2的探索能力與形式證明系統的最終可信度結合起來。

參考文獻，???https://github.com/deepseek-ai/DeepSeek-Math-V2/blob/main/DeepSeekMath_V2.pdf??

本文轉載自??清熙??，作者：王慶法