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