大模型上下文協議與Spring開發集成篇——mcp-spring-webmvc原理
使用 DeepSeek-Coder-V2 合成自然語言思維鏈標注數據，結合 Lean 證明器標注的中間狀態信息，將模型的形式化證明能力與自然語言推理對齊，同時滿足程序驗證的要求。訓練：以 Lean 證明器的驗證結果直接作為獎勵信號，使用 GRPO 算法對模型進行強化學習訓練。蒙特卡洛樹搜索：引入 RMaxTS 算法，激勵探索行為以解決證明搜索中的獎勵稀疏問題，增強模型靈活生成多樣化證明的能力。實驗結果：在高中水平的 miniF2F 和大學本科水平的 ProofNet 基準測試中取得了新的 SOTA，顯著超越了主流數學模型。
論文和模型均已開源：論文地址：https://arxiv.org/abs/2408.08152模型下載：https://huggingface.co/deepseek-aiGitHub 主頁：https://github.com/deepseek-ai/DeepSeek-Prover-V1.5
預訓練在高質量的數學和代碼數據上進行進一步的預訓練，特別關注 Lean、Isabelle 和 Metamath 等定理證明語言，以提高模型在形式化數學領域的通用能力。有監督微調已有工作大多聚焦于僅僅生成下一個證明步驟，而 DeepSeek-Prover-V1.5 則選擇了更為困難的完整證明生成的訓練目標。此外，在 DeepSeek-Prover-V1 合成的大規模定理證明數據的基礎上，利用 DeepSeek-Coder-V2 合成自然語言的思維鏈數據標注，促使模型兼顧自然語言推理與形式化定理證明。強化學習抽取微調數據中的定理內容作為輸入，使用微調后的模型生成多個完整的證明候選項，然后利用 Lean 證明器對其正確性進行檢驗。將驗證結果作為二元獎勵信號，強化學習訓練進一步增強了模型與驗證系統形式規范的一致性。三階段模型權重均已開源。
DeepSeek-Prover-V1.5 將定理證明中的蒙特卡洛樹搜索從單一證明預測推廣至完整證明生成，為此特別引入了“截斷-恢復”的機制來進行樹節點的擴展：（a） 選擇一個節點進行擴展，追蹤其對應的證明代碼前綴，其中包括文件頭、初始聲明以及所有祖先節點中已經成功應用的 tactics。（b） 模型基于這個代碼前綴和 Lean 證明器返回的 tactic state 生成后續完整證明。（c） Lean 4 證明器驗證組合后的證明代碼（前綴和新生成的代碼）。如果沒有發現錯誤，樹搜索過程終止。如果檢測到錯誤，我們在第一個錯誤消息處截斷新生成的代碼，丟棄后續代碼，并將成功部分解析為 tactics。（d） 每個 tactic 作為新節點添加到搜索樹中，在選定的節點之后擴展出一串后繼節點。（e） 完成樹節點擴展后，選擇另一個候選節點并進行下一輪擴展。這個過程重復進行，直到找到正確的證明或達到采樣數上限。此外，DeepSeek-Prover-V1.5 結合了一種新的蒙特卡洛樹搜索算法——RMaxTS，建立了內在獎勵機制以引導搜索流程中生成的證明產生多樣化的 tactic state，利用 Lean 證明器的反饋來幫助減少冗余生成，提高采樣效率。
下表展示了各模型在 miniF2F-test 基準測試中的表現。該基準由高中水平的數學習題和競賽題（如 AMC、AIME 和 IMO）在 Lean 定理證明語言中形式化而成。在直接生成完整證明的任務中，DeepSeek-Prover-V1.5 以 60.2% 的證明通過率顯著領先其他方法。當結合 RMaxTS 樹搜索技術時，其性能更是提升至 63.5% 的通過率。
下表呈現了各模型在 ProofNet 基準測試上的成績。該基準精選了數學本科主流教材中的習題，涵蓋實分析、復分析、線性代數、抽象代數和拓撲學等核心分支。在直接生成證明的任務中，DeepSeek-Prover-V1.5 再次以 22.6% 的通過率顯著超越其他方法。運用 RMaxTS 樹搜索后，其表現進一步提升至 25.3% 的通過率。
更多方法細節和分析實驗見論文，閱讀原文即可獲取。
隨著人工智能技術的不斷進步，數學定理證明領域正迎來一場革命。DeepSeek-Prover-V1.5的最新成果表明，AI能夠憑借其強大的邏輯推理能力獨立解決多步驟的復雜證明問題。這一突破不僅展示了AI在數學定理證明中的巨大潛力，還為未來開發能夠自主提出并證明完整數學理論的AI系統奠定了堅實基礎。這些系統將有助于人類數學家更深入地探索數學真理，推動數學研究的前沿發展。
原文轉載自：https://mp.weixin.qq.com/s/O4aC9dvJC30sfSQyYgbcow
