首頁 科技週邊 人工智慧 DeepSeek開源數學大模型,高中、大學定理證明新SOTA

DeepSeek開源數學大模型,高中、大學定理證明新SOTA

Aug 19, 2024 am 04:26 AM
產業 DeepSeek

DeepSeek-Prover-V1.5 透過結合強化學習和蒙特卡洛樹搜索,顯著提升了證明生成的效率和準確性。

AI 技術與數學發現的進展,正前所未有地交織在一起。

前段時間,著名數學家陶哲軒在牛津數學公開講座中做了主題為「AI 在科學和數學中的潛力」的主題分享。他指出,將 AI 整合到數學領域將使形式化證明的編寫速度超過人類證明(人類證明容易出錯)。這將成為一個關鍵轉折點,意味著形式化證明的使用將不僅限於驗證現有的證明,還將用於創造新的數學知識。這將透過廣泛的人類數學家與 AI 數學家之間的協作來實現。我們將迎來一個「大數學」時代!
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
正如陶哲軒所說,將 AI 應用於形式化定理證明已成為數學家的日常操作。在另一頭,AI 科學家們也在努力提高 AI 在形式化定理證明中的表現和效率,例如 DeepSeek 剛推出的新模型 ——DeepSeek-Prover-V1.5。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
DeepSeek-Prover-V1.5 是一個 70 億參數的開源模型。它透過結合強化學習(基於證明助手回饋的強化學習,RLPAF)和蒙特卡羅樹搜尋(特別是提出的 RMaxTS 變體),顯著提升了證明生成的效率和準確性。 DeepSeek-Prover-V1.5 在 Lean 4 的形式定理證明方面優於所有開源模型。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
以下是技術報告的詳細內容。

技術報告概述
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
  • 報告標題:DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
  • 報告連結:https://arxiv.org/pdf/ 2408.08152
GitHub 連結:https://github.com/deepseek-ai/DeepSeek-Prover-V1.5



近年來,在大型語言模型領域的進展極大地推動了人工智慧在數學推理和定理證明方面的發展。但語言模型在形式化定理證明上仍面臨重大挑戰。例如,使用 Lean 和 Isabelle 這類系統進行證明時,需要進行嚴格的推導,以滿足驗證系統的形式規範。即便是像 GPT-4 這樣的先進模型,在處理複雜的形式證明時也顯得力不從心,這凸顯了形式化證明中編碼和數學推理的複雜性。一個高效的形式化定理證明模型不僅需要理解 Lean 證明助手等形式化系統的語法和語義,還需要將抽象的數學推理與精確的形式化表達方式結合。

在形式化定理證明中,語言模型通常採用兩種策略:證明步驟產生(proof-step generation)和完整證明產生(whole-proof generation)。

證明步驟生成通過預測並驗證每一個策略,利用形式化驗證器獲取當前策略狀態的更新信息,並常結合樹搜索技術來構建有效的證明。而完整證明生成則在計算上更為高效,它基於定理陳述一次生成整個證明代碼,減少了證明模型與形式化定理驗證器之間協調所需的通信量。 儘管 DeepSeek-Prover-V1 在 Lean 4 中通過完整證明生成取得了 SOTA 成果,但這種方法也有其獨特的挑戰。它需要在沒有中間策略狀態資訊的情況下進行長期序列預測,而未來的策略依賴這些隱藏的結果。在 Lean 的策略模式中,證明是透過一系列改變證明狀態的策略來建構的。這種順序性可能導致錯誤累積,一個小的誤差就可能使證明偏離正確的路徑。具體來說,自迴歸模型在產生長證明時可能會對中間策略狀態有錯誤的認知。 為了在不犧牲完整證明產生的簡便性和計算效率的同時,無縫地整合中間策略狀態,研究者在DeepSeek-Prover-V1.5 中開發了一種統一方法。這種方法透過截斷和重新開始(truncate-and-resume)機制,結合了證明步驟產生和完整證明產生的優勢。

過程從標準的完整證明產生開始,語言模型根據定理陳述前綴完成證明代碼,然後由 Lean 證明器進行驗證。如果證明正確無誤,流程就此結束。如果發現錯誤,就從第一個錯誤訊息截斷程式碼,並丟棄後續程式碼。然後,使用成功產生的證明程式碼作為提示,產生下一個證明段。

為了提高模型新完成部分的準確性,研究者在提示的末尾添加了 Lean 4 證明器的最新狀態作為註釋。值得注意的是,該方法並不局限於從上次成功應用的策略中重新開始。研究者將截斷和重新開始機制整合到了蒙特卡羅樹搜尋(MCTS)中,由樹搜尋策略來安排截斷點。此外,他們提出了一種新的無獎勵(reward-free)探索演算法,用於解決證明搜尋中的獎勵稀疏問題。他們賦予樹搜尋智慧體內在的驅動力,也就是好奇心,以廣泛探索策略狀態空間。這些演算法模組擴展了他們的完整證明生成模型,使其成為一個靈活的互動式定理證明工具,能夠有效利用證明助手的回饋,產生多樣化的解決方案。

核心貢獻

研究者提出了一個全面的框架,用於開發基於語言模型的形式化數學證明工具,他們整合了幾個關鍵組件:大規模數學預訓練、形式化數學語料庫的構建和增強、基於證明助手反饋的在線強化學習,以及用於定理證明長期規劃的樹搜尋方法論。預訓練模型、監督微調模型、強化學習模型以及蒙特卡洛樹搜尋演算法的程式碼都公開提供,以便進一步研究和應用。

1、預訓練

研究者透過進一步在高品質數學和程式碼資料上預先訓練,增強了基礎模型在形式化定理證明和數學推理方面的能力,重點關注Lean、Isabelle 和Metamath 等廣泛用於證明助手的形式語言。

2、監督微調

研究者透過實現兩種資料增強技術,改進了Lean 4 程式碼補全數據集。首先,他們使用 DeepSeek-Coder V2 236B 在 Lean 4 程式碼旁註釋 CoT(chain-of-thought)評論,將形式化定理證明與自然語言推理對齊。其次,他們在 Lean 4 證明程式碼中插入中間策略狀態訊息,使他們的模型更有效地利用編譯器回饋。然後,他們使用這個資料集對預訓練模型進行微調。

3、強化學習

研究者採用GRPO 演算法對監督微調模型進行RLPAF(inforcement learning proreinforcement learning pro assistant feedback,基於證明助手回饋的強化學習)。 Lean 證明器的驗證結果作為獎勵監督,增強了模型與驗證系統的形式規範的一致性。

4、蒙特卡洛樹搜尋

研究者透過引入一種新的抽象和相應的搜尋演算法,推進了形式化定理證明中的樹搜尋方法。他們的截斷和重新開始機製作為狀態 - 動作抽象,將樹搜尋過程無縫整合到完整證明生成框架中。他們展示了 RMaxTS,這是一種創新的蒙特卡羅樹搜尋演算法,利用 RMax 策略來解決證明搜尋問題中稀疏獎勵的探索挑戰。透過分配內在獎勵,這種演算法鼓勵證明智能體產生多樣化的規劃路徑,從而促進對證明空間的廣泛探索。

評估與量測

1、高中程度資料集🎜>

在單通道法完整證明生成設定中,DeepSeek-Prover-V1.5 在miniF2F 的測試集上達到了60.2% 的通過率,比DeepSeek-Prover-V1 的50.0 % 提高了10.2 個百分點。結合樹搜尋技術後,通過率進一步提升,達到了 63.5% 的新 SOTA。

2、大學本科程度ProofNet 資料集

DeepSeek-Prover-V1.5 在ProofNet 的單通道法完整證明生成設定中也展現出強大的效能,在驗證集上通過率為21.6%,在測試集上為23.7%。結合樹搜尋技術之後,這些結果被進一步增強,在驗證集上達到了 25.4% 的新 SOTA,在測試集上達到了 25.3%。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
模型訓練

為了提高語言模型生成形式證明和透過數學語言進行數學語言進行推理的能力,研究者對基礎模型進行了進一步預訓練,並將這個改進的模型命名為DeepSeek-ProverV1.5-Base。

接著文章探討了 DeepSeek-Prover-V1.5 的監督微調 (SFT) 所涉及的方法和流程。具體來說,研究者透過添加詳細的解釋性註釋來擴充 DeepSeekProver-V1 的證明資料集。此增強旨在改善自然語言描述與 Lean 4 代碼之間的一致性,從而促進更好的形式數學推理。此外,研究者將中間策略狀態資訊作為輔助預測任務納入其中,以支援蒙特卡羅樹搜尋過程中使用的截斷和重新開始機制,並將生成的模型稱為 DeepSeek-ProverV1.5-SFT。

基於證明助手回饋的強化學習

為了進一步提高DeepDeep V1.5-SFT 的表現,該研究引入了一個強化學習階段,從而得到了DeepSeek-Prover-V1.5-RL 模型。此階段利用強化學習(RL)根據 Lean 4 證明器的驗證回饋來提升效能。以下是該 RL 過程的具體細節。

訓練提示。在強化學習階段,研究使用監督微調資料集的部分定理陳述作為訓練提示。經過篩選保留了大約 4,500 個獨特的定理陳述。每個定理都帶有 CoT 和非 CoT 引導提示,以增強模型在這兩種模式下的證明生成能力。 

獎勵。當透過 RL 訓練 LLM 時,訓練好的獎勵模型通常會提供回饋訊號。相較之下,形式化定理證明受益於證明助手對生成的證明的嚴格驗證,從而提供了顯著的優勢。具體來說,如果驗證正確,則每個生成的證明將獲得 1 的獎勵,否則將獲得 0 的獎勵。雖然這種二元獎勵訊號是準確的,但它也很稀疏,尤其是對於那些對監督微調模型具有挑戰性的定理而言。為了緩解這種稀疏性,研究者選擇了對監督微調模型具有挑戰性但可實現的訓練提示,如上所述。

強化學習演算法。該研究採用組相對策略優化(GRPO)作為本文的 RL 演算法,與 PPO 相比,該演算法顯示出更高的有效性和效率。具體而言,GRPO 為每個定理提示抽取一組候選證明,並根據組內輸出的相對獎勵來最佳化模型。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
評估。圖 3 給出了 miniF2F 和 ProofNet 資料集上每個訓練階段的比較分析。在大多數設定中,CoT 模式始終優於非 CoT 模式。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
面向探索的蒙特卡洛樹搜尋

為了在整體證明生成設定中實作樹搜尋方法,該研究引入了證明樹抽象化來定義定制的狀態和動作空間,並利用了截斷和重新開始機制。研究者首先將不完整的證明分解為與各個證明步驟相對應的樹節點序列,然後利用儲存在這些樹節點中的部分內容繼續證明生成過程。圖 4 說明了從整體證明產生建構證明搜尋樹的過程。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
截斷:該研究在策略層級建立證明搜尋樹,其中每條樹邊代表策略狀態的單一轉換步驟。首先,該研究將模型產生的整個證明提交給 Lean 證明器,並將其解析為策略。然後在最早的驗證錯誤處截斷證明,確保所有後續策略代碼都可以成功應用,以將證明推進到所需的定理。策略程式碼被分割成幾個程式碼片段,每個程式碼片段包含一個有效的策略程式碼及其相關的思維鏈註釋,對應於代表策略狀態轉換的單一樹邊。透過這種抽象,每個策略程式碼被轉換為一系列樹節點,形成從根到特定節點的路徑。

重新開始:在Lean 4 中,不同的策略可以導致相同的策略狀態,這意味著證明樹中的每個節點可能對應多種能夠實現相同結果的策略代碼。為了解決這個問題,研究者在每個節點中儲存一組這些等效的策略代碼。當樹搜尋智能體展開一個節點時,它會隨機選擇一個策略作為語言模型的提示。

蒙特卡洛樹搜尋的內在獎勵

接下來文章介紹了內在文章介紹了內在獎勵驅動的探索演算法- 應用於樹搜尋的RMax(RMax applied to Tree Search,RMaxTS),將無獎勵探索納入證明搜尋問題。

RMax 應用於 MCTS。該研究採用 RMax 這個經典探索機制來建立蒙特卡羅樹搜尋的內在獎勵。在證明搜尋的上下文中,證明完成之前不提供外部獎勵,此演算法過程類似於 ZeroRMax ,其中智能體的探索僅由內在獎勵驅動,即設定DeepSeek開源數學大模型,高中、大學定理證明新SOTA。樹擴展步驟的內在獎勵取決於是否向搜尋樹中添加新節點
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
這種啟發式方法可以潛在地減少冗餘生成並提高樣本效率。

實驗結果

在本節中,研究者使用他們使用兩個基準來評估DeepSeek-Prover-V1.5 的定理證明能力。前者包括高中程度的練習和競賽問題,後者則涉及本科程度的定理。

為了確保一致性,研究者使用了與評估中相同的訓練模型和推理配置,展示了完整證明生成和蒙特卡洛樹搜尋方法的結果。

首先,論文介紹了 DeepSeek-Prover-V1.5 與之前的一些 SOTA 模型的對比分析,重點展示了其性能和進步。

  • 一般模型


COPRA 促進了這些模型在形式定理證明中的評估,它是一個上下文學習智能體,利用這些大語言模型提出戰術應用。

此外,研究者還討論了 Llemma,這是一系列在廣泛的通用數學語料庫上訓練的語言模型,通常用作形式定理證明的基礎模型。

  • 形式化數學的專用模型


Hypertree Proof Search 利用 Lean 探討了蒙特卡羅樹搜尋在形式定理證明中的應用。同期的 InternLM2-Math 和 InternLM2-StepProver 也表現出卓越的性能。

然後,研究者將這些模型與 DeepSeek-Prover-V1.5 進行了比較。

miniF2F 上的結果

各種定理證明方法在miniF2F 測試資料集上的比較分析。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
在單通道完整證明生成設定中,DeepSeekProver-V1.5-RL 的通過率最高,達到60.2%,比DeepSeek-Prover-V1 的50.0% 提高了10.2 個百分點。 DeepSeek-Prover-V1.5-RL 將採樣預算限制在 128 次嘗試,證明了 51.6% 的問題,明顯優於其他 whole-proof 生成方法,與領先的樹搜尋方法不相上下。在樹搜尋方法類別中,DeepSeek-Prover-V1.5-RL + RMaxTS 以 62.7% 的通過率遙遙領先,確立了新的 SOTA 水平,與現有方法拉開了很大差距。

值得注意的是,DeepSeek-Prover-V1.5-RL 只需要3200 次完整證明採樣就能達到54.9% 的通過率,超過了InternLM2-StepProver先前的SOTA 水平,後者需要執行64 × 3200 次樹搜尋才能達到54.5% 的通過率。

ProofNet 上的結果

表2 證明方法列出了各種定理證明方法在ProofNet 資料集上的比較分析。 DeepSeek-Prover-V1.5-RL 在整個 ProofNet 資料集上的通過率分別達到了 22.6% 和 25.3%。這些結果超過了現有的 SOTA 方法 ReProver(13.8%)和 InternLM2-StepProver(18.1%)。當完整證明產生嘗試次數限制為 3200 次時,DeepSeek-Prover-V1.5 也證明了 21.7% 的定理,比之前最先進的 InternLM2-StepProver 提高了 3.6%。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
重新檢視訓練策略在大規模取樣中的效果

研究者審視了多個訓練模組在大規模採樣環境中的效果,重點是單通道完整證明生成和蒙特卡羅樹搜尋。

表3 比較了兩種生成模式,即非CoT 和CoT 在miniF2F-test 資料集上的效能,顯示隨著樣本預算的增加,CoT 相對於非CoT 模式的優勢被放大。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA
消融實驗

在消融實驗中,研究者檢驗了RMaxRTS 的演算法設計。實驗是在 miniF2F 測試資料集上使用 DeepSeek-Prover-V1.5-RL 以 CoT 模式進行的。如圖 5 所示,左側顯示了 6400 個生成樣本內 Pass@K 準確率的曲線,右側顯示了樣本量更大時的結果。
DeepSeek開源數學大模型,高中、大學定理證明新SOTA

以上是DeepSeek開源數學大模型,高中、大學定理證明新SOTA的詳細內容。更多資訊請關注PHP中文網其他相關文章!

本網站聲明
本文內容由網友自願投稿,版權歸原作者所有。本站不承擔相應的法律責任。如發現涉嫌抄襲或侵權的內容,請聯絡admin@php.cn

熱AI工具

Undress AI Tool

Undress AI Tool

免費脫衣圖片

Undresser.AI Undress

Undresser.AI Undress

人工智慧驅動的應用程序,用於創建逼真的裸體照片

AI Clothes Remover

AI Clothes Remover

用於從照片中去除衣服的線上人工智慧工具。

Clothoff.io

Clothoff.io

AI脫衣器

Video Face Swap

Video Face Swap

使用我們完全免費的人工智慧換臉工具,輕鬆在任何影片中換臉!

熱門文章

熱工具

記事本++7.3.1

記事本++7.3.1

好用且免費的程式碼編輯器

SublimeText3漢化版

SublimeText3漢化版

中文版,非常好用

禪工作室 13.0.1

禪工作室 13.0.1

強大的PHP整合開發環境

Dreamweaver CS6

Dreamweaver CS6

視覺化網頁開發工具

SublimeText3 Mac版

SublimeText3 Mac版

神級程式碼編輯軟體(SublimeText3)

熱門話題

Laravel 教程
1605
29
PHP教程
1511
276
深度求索deepseek官網入口 深度求索deepseek官網入口 Mar 12, 2025 pm 01:33 PM

2025年開年,國產AI“深度求索”(deepseek)驚艷亮相!這款免費開源的AI模型,性能堪比OpenAI的o1正式版,並已在網頁端、APP和API全面上線,支持iOS、安卓和網頁版多端同步使用。深度求索deepseek官網及使用指南:官網地址:https://www.deepseek.com/網頁版使用步驟:點擊上方鏈接進入deepseek官網。點擊首頁的“開始對話”按鈕。首次使用需進行手機驗證碼登錄。登錄後即可進入對話界面。 deepseek功能強大,可進行代碼編寫、文件讀取、創

deepseek服務器繁忙怎麼解決 deepseek服務器繁忙怎麼解決 Mar 12, 2025 pm 01:39 PM

DeepSeek:火爆AI遭遇服務器擁堵,如何應對? DeepSeek作為2025年開年爆款AI,免費開源且性能媲美OpenAIo1正式版,其受歡迎程度可見一斑。然而,高並發也帶來了服務器繁忙的問題。本文將分析原因並提供應對策略。 DeepSeek網頁版入口:https://www.deepseek.com/DeepSeek服務器繁忙的原因:高並發訪問:DeepSeek的免費和強大功能吸引了大量用戶同時使用,導致服務器負載過高。網絡攻擊:據悉,DeepSeek對美國金融界造成衝擊,

deepseek怎麼轉換pdf deepseek怎麼轉換pdf Feb 19, 2025 pm 05:24 PM

DeepSeek 無法直接將文件轉換為 PDF。根據文件類型,可以使用不同方法:常見文檔(Word、Excel、PowerPoint):使用微軟 Office、LibreOffice 等軟件導出為 PDF。圖片:使用圖片查看器或圖像處理軟件保存為 PDF。網頁:使用瀏覽器“打印成 PDF”功能或專用的網頁轉 PDF 工具。不常見格式:找到合適的轉換器,將其轉換為 PDF。選擇合適的工具並根據實際情況制定方案至關重要。

deepseek怎麼本地微調 deepseek怎麼本地微調 Feb 19, 2025 pm 05:21 PM

本地微調 DeepSeek 類模型面臨著計算資源和專業知識不足的挑戰。為了應對這些挑戰,可以採用以下策略:模型量化:將模型參數轉換為低精度整數,減少內存佔用。使用更小的模型:選擇參數量較小的預訓練模型,便於本地微調。數據選擇和預處理:選擇高質量的數據並進行適當的預處理,避免數據質量不佳影響模型效果。分批訓練:對於大數據集,分批加載數據進行訓練,避免內存溢出。利用 GPU 加速:利用獨立顯卡加速訓練過程,縮短訓練時間。

Deepseek官網入口:快速訪問與使用指南(2025最新版) Deepseek官網入口:快速訪問與使用指南(2025最新版) Feb 19, 2025 pm 04:21 PM

Deepseek 是一款功能強大的在線工具,可輕鬆訪問和導航。通過訪問其官網 https://www.deepseek.com/,用戶可以註冊賬戶並充分利用其文本生成、翻譯、摘要、對話和圖像生成等主要功能。 Deepseek 旨在提供高質量的內容,並為用戶提供清晰的提示和指南,以確保最佳的使用體驗。本首段摘要概括了 Deepseek 官網的輕鬆訪問、註冊和使用過程,以及其主要功能和常見問題的解答。

deepseek網頁版官方入口 deepseek網頁版官方入口 Mar 12, 2025 pm 01:42 PM

國產AI黑馬DeepSeek強勢崛起,震撼全球AI界!這家成立僅一年半的中國人工智能公司,憑藉其免費開源的大模型DeepSeek-V3和DeepSeek-R1,在性能上與OpenAI等國際巨頭比肩,甚至在成本控制方面實現了突破性進展,贏得了全球用戶的廣泛讚譽。 DeepSeek-R1現已全面上線,性能媲美OpenAIo1正式版!您可以在網頁端、APP以及API接口體驗其強大的功能。下載方式:支持iOS和安卓系統,用戶可通過應用商店下載;網頁版也已正式開放! DeepSeek網頁版官方入口:ht

安卓首家接入DeepSeek背後:看見女性力量 安卓首家接入DeepSeek背後:看見女性力量 Mar 12, 2025 pm 12:27 PM

中国女性科技力量在AI领域的崛起:荣耀与DeepSeek合作背后的女性故事女性在科技领域的贡献日益显著。中国科技部数据显示,女性科技工作者数量庞大,在AI算法开发中展现出独特的社会价值敏感性。本文将聚焦荣耀手机,探究其率先接入DeepSeek大模型背后的女性团队力量,展现她们如何推动科技进步,重塑科技发展价值坐标系。2024年2月8日,荣耀正式上线DeepSeek-R1满血版大模型,成为安卓阵营首家接入DeepSeek的厂商,引发用户热烈反响。这一成功背后,女性团队成员在产品决策、技术攻坚和用户

DeepSeek怎麼實時翻譯 DeepSeek怎麼實時翻譯 Feb 19, 2025 pm 04:33 PM

DeepSeek實時翻譯的能力取決於“實時”的嚴格定義。雖然沒有翻譯軟件能做到絕對實時,但DeepSeek等軟件追求極低延遲,通過神經機器翻譯(NMT)模型理解語言含義,以近乎同步速度提供翻譯。然而,NMT模型對計算資源要求高,設備性能不足或網絡不穩定會影響實時翻譯質量。另外,影響實時翻譯的因素還包括:輸入語音清晰度、語言對質量、模型更新頻率。因此,建議在使用DeepSeek時確保網絡穩定、設備性能足夠,且保持對翻譯結果的警惕,避免因追求“實時”而忽視翻譯準確性和流暢性。

See all articles