欧美精品,亚洲精品日韩传,欧洲grand老妇人bbw

Highlights數(shù)據(jù)

使用 DeepSeek-Coder-V2 合成自然語(yǔ)言思維鏈標(biāo)注數(shù)據(jù)，結(jié)合 Lean 證明器標(biāo)注的中間狀態(tài)信息，將模型的形式化證明能力與自然語(yǔ)言推理對(duì)齊，同時(shí)滿(mǎn)足程序驗(yàn)證的要求。訓(xùn)練：以 Lean 證明器的驗(yàn)證結(jié)果直接作為獎(jiǎng)勵(lì)信號(hào)，使用 GRPO 算法對(duì)模型進(jìn)行強(qiáng)化學(xué)習(xí)訓(xùn)練。蒙特卡洛樹(shù)搜索：引入 RMaxTS 算法，激勵(lì)探索行為以解決證明搜索中的獎(jiǎng)勵(lì)稀疏問(wèn)題，增強(qiáng)模型靈活生成多樣化證明的能力。實(shí)驗(yàn)結(jié)果：在高中水平的 miniF2F 和大學(xué)本科水平的 ProofNet 基準(zhǔn)測(cè)試中取得了新的 SOTA，顯著超越了主流數(shù)學(xué)模型。

論文和模型均已開(kāi)源：論文地址：https://arxiv.org/abs/2408.08152模型下載：https://huggingface.co/deepseek-aiGitHub 主頁(yè)：https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

模型訓(xùn)練

預(yù)訓(xùn)練在高質(zhì)量的數(shù)學(xué)和代碼數(shù)據(jù)上進(jìn)行進(jìn)一步的預(yù)訓(xùn)練，特別關(guān)注 Lean、Isabelle 和 Metamath 等定理證明語(yǔ)言，以提高模型在形式化數(shù)學(xué)領(lǐng)域的通用能力。有監(jiān)督微調(diào)已有工作大多聚焦于僅僅生成下一個(gè)證明步驟，而 DeepSeek-Prover-V1.5 則選擇了更為困難的完整證明生成的訓(xùn)練目標(biāo)。此外，在 DeepSeek-Prover-V1 合成的大規(guī)模定理證明數(shù)據(jù)的基礎(chǔ)上，利用 DeepSeek-Coder-V2 合成自然語(yǔ)言的思維鏈數(shù)據(jù)標(biāo)注，促使模型兼顧自然語(yǔ)言推理與形式化定理證明。強(qiáng)化學(xué)習(xí)抽取微調(diào)數(shù)據(jù)中的定理內(nèi)容作為輸入，使用微調(diào)后的模型生成多個(gè)完整的證明候選項(xiàng)，然后利用 Lean 證明器對(duì)其正確性進(jìn)行檢驗(yàn)。將驗(yàn)證結(jié)果作為二元獎(jiǎng)勵(lì)信號(hào)，強(qiáng)化學(xué)習(xí)訓(xùn)練進(jìn)一步增強(qiáng)了模型與驗(yàn)證系統(tǒng)形式規(guī)范的一致性。三階段模型權(quán)重均已開(kāi)源。

蒙特卡洛樹(shù)搜索

DeepSeek-Prover-V1.5 將定理證明中的蒙特卡洛樹(shù)搜索從單一證明預(yù)測(cè)推廣至完整證明生成，為此特別引入了“截?cái)?恢復(fù)”的機(jī)制來(lái)進(jìn)行樹(shù)節(jié)點(diǎn)的擴(kuò)展：（a）選擇一個(gè)節(jié)點(diǎn)進(jìn)行擴(kuò)展，追蹤其對(duì)應(yīng)的證明代碼前綴，其中包括文件頭、初始聲明以及所有祖先節(jié)點(diǎn)中已經(jīng)成功應(yīng)用的 tactics。（b）模型基于這個(gè)代碼前綴和 Lean 證明器返回的 tactic state 生成后續(xù)完整證明。（c） Lean 4 證明器驗(yàn)證組合后的證明代碼（前綴和新生成的代碼）。如果沒(méi)有發(fā)現(xiàn)錯(cuò)誤，樹(shù)搜索過(guò)程終止。如果檢測(cè)到錯(cuò)誤，我們?cè)诘谝粋€(gè)錯(cuò)誤消息處截?cái)嘈律傻拇a，丟棄后續(xù)代碼，并將成功部分解析為 tactics。（d）每個(gè) tactic 作為新節(jié)點(diǎn)添加到搜索樹(shù)中，在選定的節(jié)點(diǎn)之后擴(kuò)展出一串后繼節(jié)點(diǎn)。（e）完成樹(shù)節(jié)點(diǎn)擴(kuò)展后，選擇另一個(gè)候選節(jié)點(diǎn)并進(jìn)行下一輪擴(kuò)展。這個(gè)過(guò)程重復(fù)進(jìn)行，直到找到正確的證明或達(dá)到采樣數(shù)上限。此外，DeepSeek-Prover-V1.5 結(jié)合了一種新的蒙特卡洛樹(shù)搜索算法——RMaxTS，建立了內(nèi)在獎(jiǎng)勵(lì)機(jī)制以引導(dǎo)搜索流程中生成的證明產(chǎn)生多樣化的 tactic state，利用 Lean 證明器的反饋來(lái)幫助減少冗余生成，提高采樣效率。

模型表現(xiàn)

下表展示了各模型在 miniF2F-test 基準(zhǔn)測(cè)試中的表現(xiàn)。該基準(zhǔn)由高中水平的數(shù)學(xué)習(xí)題和競(jìng)賽題（如 AMC、AIME 和 IMO）在 Lean 定理證明語(yǔ)言中形式化而成。在直接生成完整證明的任務(wù)中，DeepSeek-Prover-V1.5 以 60.2% 的證明通過(guò)率顯著領(lǐng)先其他方法。當(dāng)結(jié)合 RMaxTS 樹(shù)搜索技術(shù)時(shí)，其性能更是提升至 63.5% 的通過(guò)率。

下表呈現(xiàn)了各模型在 ProofNet 基準(zhǔn)測(cè)試上的成績(jī)。該基準(zhǔn)精選了數(shù)學(xué)本科主流教材中的習(xí)題，涵蓋實(shí)分析、復(fù)分析、線(xiàn)性代數(shù)、抽象代數(shù)和拓?fù)鋵W(xué)等核心分支。在直接生成證明的任務(wù)中，DeepSeek-Prover-V1.5 再次以 22.6% 的通過(guò)率顯著超越其他方法。運(yùn)用 RMaxTS 樹(shù)搜索后，其表現(xiàn)進(jìn)一步提升至 25.3% 的通過(guò)率。

更多方法細(xì)節(jié)和分析實(shí)驗(yàn)見(jiàn)論文，閱讀原文即可獲取。

About Future

隨著人工智能技術(shù)的不斷進(jìn)步，數(shù)學(xué)定理證明領(lǐng)域正迎來(lái)一場(chǎng)革命。DeepSeek-Prover-V1.5的最新成果表明，AI能夠憑借其強(qiáng)大的邏輯推理能力獨(dú)立解決多步驟的復(fù)雜證明問(wèn)題。這一突破不僅展示了AI在數(shù)學(xué)定理證明中的巨大潛力，還為未來(lái)開(kāi)發(fā)能夠自主提出并證明完整數(shù)學(xué)理論的AI系統(tǒng)奠定了堅(jiān)實(shí)基礎(chǔ)。這些系統(tǒng)將有助于人類(lèi)數(shù)學(xué)家更深入地探索數(shù)學(xué)真理，推動(dòng)數(shù)學(xué)研究的前沿發(fā)展。

原文轉(zhuǎn)載自：https://mp.weixin.qq.com/s/O4aC9dvJC30sfSQyYgbcow