MLNLP

社群是國內外知名的機器學習與自然語言處理社群，受眾覆蓋國內外NLP碩博生、高校老師以及企業研究人員。

社群的願景是促進國內外自然語言處理，機器學習學術界、產業界和廣大愛好者之間的交流和進步，特別是初學者同學們的進步。

來源 | AI科技評論

作者丨王悅

編輯丨陳彩嫻

在 DeepSeek 能夠破圈而出的一眾原因中，完全摒棄傳統的監督微調（SFT）、轉而採用大規模強化學習（RL）的創新之處是關鍵所在，這使得模型推理能力在質上取得顯著突破，更證明了強化學習在提升大語言模型推理能力方面的巨大潛力。

近幾年，學界和業界關於 RL 和 LLM 也湧現出了頗多具備開創性意義的研究成果。在 AI 智慧體推理與決策研討會（AIR 2025）上，來自倫敦大學學院、加州大學伯克利分校、普林斯頓大學、華盛頓大學、卡內基梅隆大學、Meta、華為等多位學術界和工業界的研究人員圍繞強化學習、推理決策、AI 智慧體展開討論，回答了諸多問題，例如：

AI 系統如何模擬類人推理和決策過程？
最新的演算法、框架和工具如何支援在不確定性下進行穩健的決策？
如何確保 AI 的決策過程是道德的、透明的且公正的?
……

從一系列前沿的推理決策研究中，可以看到 DeepSeek 的影子。2023 年，來自華盛頓大學的 Hanna Hajishirai 教授團隊釋出了一項關於大語言模型推理的開放訓練方法的工作，研究強調，為了從預訓練模型發展到最終模型，需要經歷了三個階段：指令微調、偏好微調以及具有可驗證獎勵的強化學習。而這一方法也是 DeepSeek 所採用的推理開放訓練方法。

Meta GenAI 的田淵棟教授系統總結了當下應對大語言模型侷限的解決方式，除了 Scaling Law 之外還有 Test-time Scaling（測試時擴充套件），即使用更大的模型加工具或思維鏈，使用不同的策略，最終可能會找到一個比單純的大型模型更好的解決方案。田淵棟教授也分享了透過使用梯度上升（gradient ascent）對神經網路進行訓練的方式，從而試圖將符號結構與神經網路表示統一起來，但這一方法還處於非常初級的階段，並不確定未來是否能成為主流。

俄亥俄州立大學的 Huan Sun 教授從隱式推理出發，探討了資料集中的兩種事實：原子事實與推斷事實，並提出了一個與主流不相同的研究發現：泛化速度與絕對資料量並沒有關係，而是與關鍵資料分佈、特別是推斷事實與原子事實的比例密切相關，且比例越高，泛化速度就越快。

同時，也有研究圍繞 AI for Math 這一主流的推理能力應用領域。普林斯頓大學的金馳教授團隊開發了Goedel-Prover 這一開源的大模型，透過將自然語言數學問題翻譯成形式語言（如Lean 4），並生成形式化證明，從而解決形式化數學陳述和證明稀缺的問題，這一模型在自動定理證明方面達到了當前世界範圍內的最佳效能水平。

更有實用性較強的 AI 智慧體研究。卡內基梅隆大學的 Graham Neubig 教授團隊提出了一個混合 Agents 方案，這種 Agents 能夠交替執行瀏覽和 API 呼叫操作，並且在每一步中，它會選擇與人類溝通、生成自然語言、執行Python程式碼（包括API呼叫）以及執行網頁瀏覽操作。

AIR2025 由倫敦大學學院汪軍、Meta GenAI 田淵棟等教授聯合主辦，致力於推動智慧系統的發展，使其能夠自主、適應性強且負責任地執行（會議詳情及註冊可訪問官網：https://ai-agent-reasoning.com）。本次會議特別鳴謝來自加州大學伯克利分校的博士後研究員顧尚定。

這是一篇圍繞 DeepSeek 的過去、當下與未來所展開的對人工智慧的精彩討論。AI 科技評論擷取會議部分精彩內進行編譯，以下為核心內容的演講實錄：

DeepSeek 的語言模型推理開放訓練方法

華盛頓大學的 Hanna Hajishirai 教授做了主題為“Open Training Recipes for Reasoning in Language Models”的演講，探討了語言模型推理的開放訓練方法。

為了從預訓練模型發展到最終模型，我們經歷了三個階段：指令微調、偏好微調以及具有可驗證獎勵的強化學習。這是我們 2023 年論文中引入的新內容。這基本上也是 DeepSeek 所採用的方法，後來我們發現 DeepSeek 也引入了同樣的方法。

我們先來談談指令微調。指令微調中，人們也把它稱為 SFT，即監督式微調。其核心思想是，你拿一個預訓練的語言模型，然後向模型輸入各種不同型別的任務指令，接著對模型進行微調，教會它如何遵循這些指令。

我們團隊在這個方向上已經投入了很長時間。我們在 2022 年開始專注於語言模型的指令微調，當時主要關注的是自然語言處理（NLP）標籤等語言測試。

2023 年，我們引入了一個自我指導框架（self-instruct framework），在這個框架下，我們教會模型合成生成越來越多的資料，以便我們能夠獲得更好的、更多的資料用於監督式微調。

這種正規化在 2023 年得到了廣泛的關注，我們看到在工業界和學術界都有很多工作基於自我指導框架展開，並設計了像 Alpaca、Vicuna 等模型。這些模型都大量使用了合成生成的指令資料進行訓練。

下一步就是在監督式微調中進行偏好微調。這裡有一個非常重要的步驟，就是資料整理。這和我剛才提到的合成數據生成是一樣的，但同時也是一個很好的資料混合設定，因為當我們關注一組任務和我們試圖最佳化的目標技能時，當我們增加一組任務的提示和完成內容時，我們可能會在其他組上失去準確性和改進。

比如，如果你在監督式微調中添加了大量數學提示和數學型別的資料，你可能會在知識回憶方面表現下降，因為你總是希望生成越來越長的思考鏈。所以，資料混合是構建一個好的微調模型中非常重要的一步。

剛才我們一直在講資料，但現在我想聚焦於什麼樣的資料才真正有助於推理。這裡所說的“推理”，舉個例子，比如一個數學問題：一家商店正在進行襯衫促銷，每件襯衫售價 25 美元，現在我們想買 7 件襯衫，總共要花多少錢？我們可以很容易地標註出答案是 125 美元，但僅僅用這種問題和金額答案作為監督式微調資料是不夠的。

大家已經認識到，真正重要的是處理這種逐步推理的輸出，它能一步步告訴我們發生了什麼。這種資料可以成為監督式微調的優質來源。

這其實並不是一個新想法，它在自然語言處理（NLP）領域的語義解析、語義理解和推理方面已經被研究很久了。但現在它又在語言模型中重新受到關注，因為如今我們可以處理這種既包含語言又包含形式化表達的推理鏈。

在早期的研究中，我們只能依賴於形式化的推理圖或推理思路。但現在面臨的巨大挑戰是：

這種逐步推理的標註雖然很好，能夠幫助模型處理複雜的多步驟問題，也能揭示模型在預訓練過程中所獲得的推理過程，甚至因為有了這些標註，我們還能發現推理鏈中間可能出現的錯誤，比如答案是125，但推理過程中可能有錯誤，這有點類似於人類的思維過程。標註這種型別的推理提示非常困難。它成本高昂、耗時費力，而且不夠多樣化。

我們的方法是做混合資料策劃，即：檢視現有的資源，然後將其與合成數據生成相結合。事實上，我們採用了這篇非常有趣的論文中介紹的方法，用於合成地生成資料，但針對不同的使用者角色。這為什麼重要呢？因為它增加了生成提示的多樣性。而且，它還使我們能夠不斷擴大這種思維鏈條以及這種很難收集的推理資料的規模。

論文連結：https://arxiv.org/abs/2406.20094

這是如何運作的呢？我們會給模型設定不同的使用者角色，比如“這是一個化學動力學研究人員”，然後讓模型以這個角色生成資料和數學問題。接下來，我們再給它設定一個不同的角色，讓它生成一個邏輯推理問題，就可以得到這樣的結果。

我們給模型提供了許多不同型別的使用者角色。事實上，我們使用了25萬種角色，包括計算機科學家、化學教授、五歲小孩等等。然後，我們讓模型根據這些角色生成數學問題。透過這種方式，我們收集了 15 萬道硬體數學題和 5 萬道小學數學題。

我們還讓模型生成程式設計問題，這主要是 Python 程式碼生成以及精確指令的遵循，貫穿於這些角色之中。在收集完這些提示後，我們使用了像 GPT-4o 或 Claude 這樣的大模型來為我們生成思維鏈條資料。然後，它們生成了逐步的解決方案。

我們來看一下這是否有所幫助。我們已經在這些設定下進行了評估，查看了一個公開的資料集，例如在數學領域，有一些由社群驅動的公開開源資料集，這些資料集是由其他團隊、朋友和學術界生成或策劃的。然後，我們開始引入一些我們基於角色生成的合成數學問題。

這些曲線展示了在不同百分比下整合角色資料的情況，32 和 69 是我們不包含任何角色資料時在數學和 GSM8K 上的結果。而最後一列則顯示了逐步增加角色生成資料的數量。

在數學領域，我們在 GSM8K 或高年級數學問題上取得了顯著的提升。相比之下，我們在小學數學（GSM with K）上的提升較小，但仍然很有趣。

在生成合成資料時，一個重要的問題就是結果的質量。你可能會說：“好吧，你們生成了這些數學資料，然後讓GPT-4為這些生成內容做標註，那麼這些標註的質量高不高呢？”

為了提高資料的質量，我們做了以下工作：我們讓 GPT-4 生成多個例項或者多條思維鏈條，然後進行了多數投票，並保留了那些大多數情況下答案正確的例項。

透過這種方式，我們刪除了很多資料。我們基本上只保留了 60% 的資料。好訊息是，即使只使用了 60% 的資料，我們在數學領域的準確率仍然相似，GSM8K 上甚至略有提升。

在整個通用方案中，我們不僅僅侷限於數學，而是涉及許多不同型別的資料。

這是我們早期的混合方案，比如用於 Tulu 2 的。隨著時間的推移，我們嘗試了許多不同型別的混合方式，最終我們的混合方案給出了最佳的平均效果。正如你在中間看到的，例如，有些混合方案在安全性方面表現更好，而在其他方面表現稍差。但最終，我們希望在平均意義上達到一種平衡，於是我們最終選擇了這種最終方案。

這是監督式微調階段的結果。現在我們進入下一個階段：偏好微調。

那麼，偏好微調的作用是什麼呢？它的想法是，我們將比較同一個提示的不同完成結果，並選擇我們認為更強的那個。通常，這在風格和聊天評估中非常有用。比如它會告訴我們：“這個結果可能更符合人類的偏好。”但我們也發現，它甚至在推理測試中也有所提升。

我們將使用基於強化學習的方法來根據這種反饋、這種偏好資料進行最佳化。

在最佳化步驟中，我們將最佳化一個獎勵，這個獎勵是受到人類偏好的啟發。同時，我們希望確保不會偏離原始語言模型太遠。因此，我們加入了一個 KL 散度懲罰項。

我們如何進行最佳化？有哪些不同的演算法可以用於最佳化這種形式化問題？通常，人們會使用 PPO（近端策略最佳化）。然後，去年還引入了一種更簡單的演算法，稱為直接近端偏好最佳化（Direct Proximal Preference Optimization）。而我們的問題是：這兩種演算法中，哪一種更好？

在直接近端偏好最佳化（DPO）中，它就像是一種非常簡單的基於學習的演算法，與機器學習中的排序演算法非常相似。而在近端策略最佳化（PPO）中，它是一種真正的強化學習方法，你有一個獎勵模型，然後我們希望對策略模型進行最佳化。

在最近的研究中，我們決定從理論和實證的角度更深入地研究這個問題，以瞭解這些演算法中哪一個更好。我們發現PPO（近端策略最佳化）始終優於DPO（直接近端偏好最佳化）。然而，PPO 的實現要複雜得多。它需要大量記憶體，因為我們希望同時將獎勵模型和策略模型保留在記憶體中進行最佳化。而當我們處理更大的模型時，這會變得更加困難，吞吐量也會顯著降低。

論文連結：https://arxiv.org/abs/2406.09279

這些是關鍵的發現。我們在比較這兩種演算法時注意到，有很多不同的變數在起作用。因此，我們開始分別對它們進行消融研究。比如說，這是我的初始監督微調結果，這些是我的平均效能，以及它們在一組任務——大量任務中的變化情況。

我們首先想研究資料的作用。我們最初加入了較弱的偏好資料，效果並不太強，所以只有一點點提升。當我們提高了偏好資料的質量時，我們看到了一個很大的跳躍。我們使用完全相同的資料，只是替換了演算法，結果 PPO 帶來了更好的提升。

當我們引入更大的獎勵模型時，這是非常直觀的——當我們有一個更大的獎勵模型時，我們期望PPO能取得更好的結果，但實際的提升並沒有達到我們的預期。我們原本以為，有了更大的獎勵模型，我們應該會看到一個很大的跳躍，但結果卻只是這麼多。我們並沒有看到太多提升，這讓我們感到非常驚訝。

現在讓我更具體地談談特定的推理測試，在一些數學推理測試上看到了幾乎完全相同的趨勢。但有趣的部分是，當我們將其與PPO結合時，我們實際上看到了一個更大的提升，尤其是在引入更大的獎勵模型時。這非常有趣。當我們開始引入更具體的數學提示時，我們在這裡看到了一個很大的跳躍。

因此，我們意識到，當我們專注於推理的提示時，情況就是這樣。這也是我們在偏好微調階段看到改進的方式。比如我們希望整合更多特定領域的數學問題。

我們把所有的發現彙總起來，然後設計了我們 2.3 模型中的偏好微調階段：

首先，我們非常謹慎地選擇提示詞。我們使用了在監督微調階段已經引入模型的一部分提示詞。我們引入了新的提示，專注於像推理領域這樣的特定領域，我們希望在這些領域看到更大的改進。同時，我們也引入了一些領域外的提示，並且發現這實際上也非常有幫助。

我們收集這些提示詞，並從一個非常大的模型集合中檢視偏好響應，比如從 70 億引數的模型到像 GPT-4o 這樣非常強大的模型。我們開始比較它們之間的偏好，看看哪一個更好，這樣你的模型就會逐漸得到改進。我們還確保包含未請求的資料，確保將 Tulu 38B 和 70B 資料納入其中，因為這是符合策略的。

然後，我們使用 GPT-4o、LLaMa 這樣的模型作為評判，來為我們對這些四個維度（幫助性、指令遵循性、真實性、誠實性）的偏好進行排序。我們也嘗試了不同的 LLM 作為評判，但結果差異不大。它們的結果幾乎都差不多。

研究發現，我們在使用所有模型時看到了很大的提升。我們展示出，與之前的偏好資料混合集相比，我們看到了一個巨大的進步。同樣，我們進行了大量的資料混合分析，研究應該從監督微調（SFT）中引入多少初始提示，以及應該引入多少新的提示。這經過了大量的實驗，以確定最佳的混合比例。

我想在這裡強調一點，對於 2.3 版本，我們決定在這個階段再次使用 DPO（直接近端偏好最佳化），因為我們還想訓練更大的模型，我們認為它的實驗速度更快，而且很有幫助。因此，我們對 DPO 做了很多改進，比如我們讓它進行了長度歸一化等。我們進行了大量的超引數調整，最終發現，這真的效果很好，尤其是在這裡使用 DPO。

但對於我們的 2.3 版本，我們實際上引入了一種新演算法。我們將其稱為“可驗證獎勵的強化學習”。當我們觀察偏好微調時，我們實際上是在訓練一個獎勵模型，這是一個為模型的某種輸出分配分數的神經網路。

我們的想法是，如果我們使用一個更簡單的設定，僅僅使用一個驗證機制，會怎麼樣呢？也就是說，如果我們生成的內容與標準答案等價，就返回 1，否則返回 0。所以它只是一個基於規則的、非常簡單的獎勵模型。

然後，我們訓練這個非常簡單、非常基礎的強化學習框架，訓練資料以提示的形式輸入。如果生成的結果非常好，我們就最佳化並改進我們的策略。

它對於這類推理任務非常有用，因為我們在一開始就已經提到，為複雜的數學問題標註思維鏈條是非常困難的。然而，在很多情況下，最終答案就足夠了。得出一個最終答案相對容易。或者我們處理的是一些生物學相關任務。對於所有這些任務，我們只需要兩種標註：原始提示和最終答案。然後我們就可以進行驗證。

我們甚至可以將其用於精確指令的遵循，如果給出一個非常複雜的指令，讓模型生成一些內容。然後，我想了解滿足的約束條件的百分比是多少，所以我們可以將這種驗證擴充套件到不同的階段。

這並不是一個全新的想法。但變化在於，現在的基礎模型，或者是在監督微調階段結束時的模型，已經得到了很大的改進。如今，我們能夠生成相對較好的思維鏈條，並將其與真實情況相對比，從而判斷它是否足夠好，是否不好，等等。

這就是我們的最終方案。我們使用最終答案或可驗證的約束來進行驗證。我們並不是在訓練中間的思維鏈條，而是讓模型自己生成思維鏈條。我們採用了經典的強化學習實現，特別是這裡我們使用了 PPO 演算法，並且我們嘗試了三個資料集。

結果是好的。以下展示是與這些資料集的基準對比，包括一些模型，比如DeepSeek V3、GPT-4o以及我們模型的不同版本，這些版本分別來自監督微調（SFT）、直接近端偏好最佳化（DPO）和可驗證獎勵的強化學習（RLV）。

這裡有一個非常有趣的觀察：當我們處理一個更大的模型，比如 405B 模型時，我們在強化學習驅動的推理（RLDR）階段看到了更大的提升。所以，這條綠色的線顯示了在自動驗證強化（Auto VR）階段的不同輪次中，我們的數學推理能力提升了多少，而粉色的線則顯示了我們在處理 70B 引數模型時提升了多少。

這也與 DeepSeek V3 的發現非常一致，他們發現在處理更大模型時，強化學習帶來的改進更為顯著。這實際上是一個非常有趣的觀察。這也引出了我們在本次討論開始時提到的觀點，即如果基礎模型變得更好，那麼我們對強化學習微調（RFM）的期望也會更高。

我們最近做了一個很小的改動，就是把 PPO 換成了 GRPO。我們借鑑了 DeepSeel 的想法，嘗試將強化學習的實現從 PPO 遷移到 GRPO，並將其應用於一個更好的基礎模型——QwenMath。我們在數學推理方面看到了顯著的提升。

我們在一個非常大的任務集合上進行了評估，這些任務涵蓋了推理、知識回憶、安全性等方面，且在所有這些方面都保持了良好的平衡，結果如下：

最後，我在這裡提到的所有內容都與訓練有關，即如何從基礎模型發展到能夠進行推理的真實且良好的模型。我們在最近的一篇論文中，還沒有將其整合到 Tulu 配方中，但我們目前正在做這項工作，我們開始專注於數學類任務，即數學推理任務。

然後我們開始收集非常高質量的推理資料和更復雜的數學問題。我們最初收集了 6 萬個樣本，然後進行了大量的質量篩選，最終得到了 1000 個多樣化的樣本。然後我們生成了這種深度思考的推理鏈條，透過從 Gemini 思考模型中提煉出深度思考的標記。不久前，我們將其替換為DeepSeek R1推理模型。到目前為止，我們只進行了簡單的監督微調（SFT），結果非常好。

然後我們採用了一種非常簡單但令人驚訝的推理時擴充套件方法，得到了一個非常有趣的結果。我們允許模型在生成結果時有一定數量的標記預算，然後我們將這個標記預算從 512 調整到 2048，或者對於 GPQA 來說，調整到 496 等等。

如果模型沒有用完它的標記預算，我們就新增一種延續標記，後讓模型再思考一會兒。透過這種方式，我們發現模型現在能夠生成更好、更深入的推理路徑，這非常有趣。還有一個更有趣的事實：當我們沒有新增任何標記，只是簡單地讓模型生成更多內容時，我們並沒有看到這種效果。

領悟的 Transformer 是隱式推理器

俄亥俄州立大學的 Huan Sun 教授做了主題為“Understanding Reasoning in LLMs and Agents:From Grokking of lmplicit Reasoning to Test-Time Scaling with Verifiers”的演講，探討了從隱式推理的領悟到測試時透過驗證器進行的擴充套件。

首先來談談什麼是隱式推理。

論文連結：https://arxiv.org/abs/2405.15071

當模型已經掌握了原子效應，我們希望模型能夠推理出多跳查詢，比如“奧巴馬妻子的生日”或者“比較年齡屬性值後，預測誰更年輕”等問題。我們希望模型能夠直接預測答案，而不是在模型內部進行語言化的思考，也不需要語言化地表達中間步驟。

CoT（思維鏈）現在非常流行。那麼，為什麼“隱性”的推理很重要呢？

首先，大規模訓練或預訓練的預設模式大多數情況下是不需要 CoT 的，所有資料都是可用的。實際上，為訓練提供推理器可能會非常昂貴。而且，從根本上來說，我認為這決定了語言模型從資料中學習事實和規則結構的能力。如果一個模型能夠在內部進行思考，那麼它在壓縮和整合資訊方面可能會更強大。

我們對這樣的結果感到好奇，想要了解其中的原因，於是我們開始了探索之旅，試圖回答以下問題：

Transformer 是否能夠學會隱式推理呢？又或者，是否存在一些根本性的限制，阻礙了模型獲得這種能力？
哪些因素會影響這種能力的獲取？是資料、技能、分佈，還是模型架構？

這個資料集非常有趣。我們使用合成數據設定來控制研究，以便得出嚴謹的結論。

在我們的資料集中有兩種事實：一種被稱為原子事實（atomic facts），另一種被稱為推斷事實（infer factor）。

原子事實就像是知識圖譜中的每個邊，是單一關係，單一關係不能再進一步拆分，這就是原子事實。

而對於推斷事實，你可以將它們視為由原子事實組合而成的多跳關係。在這裡，我們專注於兩種組合。例如，將“母親”這一關係和“出生地”結合起來，模型應該能夠回答這樣的問題：當提到母親的出生地是阿拉巴馬州時，模型能夠推斷出答案。這就是我們所說的推斷事實。

模型的目標是能夠歸納並應用潛在的規則。為了使模型能夠歸納出潛在規則，我們在訓練過程中提供了一種混合的原子效應和推斷事實。我們希望模型在訓練中能夠學會這些潛在規則，比如如何應用這些原子效應來推匯出多跳事實。

例如，現在給定一個新的查詢，比如關於哈勃望遠鏡的查詢，我們希望模型在測試時能夠應用這些歸納出的規則，並正確回答這個新的多跳查詢。

但更有趣的是，我們有 ID 和 OOD 兩種設定，基本上涵蓋了分佈內和分佈外的所有情況。這意味著我們將所有的原子效應分成兩組：一組用於 ID 設定，另一組用於 OOD 設定。

對於用於 ID 設定的原子效應，我們會將這個集合中的所有原子事實進行組合，並將推斷出的事實劃分為訓練集和測試集。在這個測試設定中，我們稱之為 ID 測試集。對於另一組原子效應，我們會對這個集合中的原子事實進行組合，而這些推斷出的事實將被用作測試。

所以，你可以這樣理解：如果一個多跳查詢，比如（h，r1）、（h，r2）屬於 ID 設定，這意味著它們涉及的原子事實已經在訓練中與其他原子效應組合過。但如果這個多跳查詢屬於 OOD 設定，那麼這些原子效應雖然在訓練中出現過，但它們與其他任何因素的組合在訓練中都沒有出現過。

我們在訓練集上訓練這個模型，並測試其在 ID 的表現。現在，我們先來看一下這兩個任務的學習曲線，可以觀察到，模型能夠達到完美的分佈內泛化效能，但是，這需要在過擬合之後進行更長時間的訓練。

對於這兩個任務，正如你所看到的，過擬合大致發生在這裡，這意味著模型在這一點上傾向於完美地擬合訓練效能，但它需要經過更多步驟的最佳化，才能使分佈內泛化效能趕上並達到完美的表現。這種延長的訓練週期就是我們所說的“阻塞期”。

第二個發現是，我們來看一下藍色曲線。可以觀察到，在組合性任務中，Transformer 並沒有實現完全的泛化。所以，分佈內泛化效能從未提升，但相比之下，它最終趕上並達到了完美的表現。

我們還發現，泛化速度與絕對資料量並沒有關係，而是與關鍵資料分佈、特別是推斷事實與原子事實的比例密切相關。也就是說，比例越高，泛化速度就越快。

這似乎與之前的研究結果相矛盾，他們認為存在一個臨界資料量的概念，即所謂的“突破現象”。但我們認為實際上起決定作用的是推斷事實與原子事實之間的比例。

然而，仍有一些更重要的問題有待進一步探討。例如，泛化過程中發生了什麼？為什麼會出現泛化？為什麼不同任務之間的泛化水平會有所不同？

這就需要我們進行更多的分析，以剖析在泛化過程中模型內部的工作機制。在這部分，我們使用了來自機制可解釋性文獻中的一些標準技術，稱為 Logit lens。

我們可以利用 logit 鏡頭將模型的內部狀態投影回輸入空間。例如，你可以看到這裡的標記 r1 是最大的成分之一，我們將其視為代表 r1 關係的隱藏狀態。這是一個高層次的想法。因果歸因（Causal Attribution）的目的是衡量一個隱藏狀態與另一個狀態之間的因果關係。在這裡，我們關注的是 r1 在第四層的隱藏狀態與目標預測之間的差異。

具體操作如下：在正常的執行過程中，我們輸入一個常規的查詢，然後生成最終的預測結果。這個過程是在模型已經過擬合之後進行的，因此模型總是能夠預測出目標。關鍵在於，我們還會進行一種干擾實驗，即用隨機取樣的 r1' 替換 r1，然後透過網路獲取 r1' 的隱藏表示，並用它替換正常執行中 r1 的隱藏表示，觀察這一變化如何影響最終的預測結果。我們會多次重複這個過程，透過取樣許多不同的隨機實體，觀察最終預測結果的改變頻率。

在那之後，你可以將整個神經網路視為一個從輸入到輸出傳播資訊的計算圖。基於連線的強度，我們可以在那些連線非常弱的邊上進行剪枝。在經過阻塞或者在阻塞的最後階段，我們在模型檢查點（checkpoint）上進行機制分析。我們發現了我們所說的“泛化電路”，用於這兩個任務。讓我帶你看看這個，這對我們來說非常有趣。

對於組合任務，這個泛化電路是這樣的：它看起來像一個順序的或分階段的電路。你可以看到，在前四層，模型試圖檢索第一個事實。然後在最後四層，模型試圖檢索第二個事實。在前四層，也就是底層，模型試圖同時並行地檢索這兩個實體的屬性級別，這就是為什麼我們稱其為並行的。然後在上層，模型試圖進行比較操作，並得出結論，比如 a 是否大於或小於 b。

我們還透過 Logit lens 檢查每個隱藏狀態代表的輸入 token。我們發現，這個隱藏表示實際上代表標記 B，它是橋接實體（bridge entity），也是 r1 的目標，並且這個隱藏表示還代表關係 r2。基本上，兩個關係確實被保留了，上層確實正在執行第二階段的知識檢索。

我們想要深入瞭解在 grokking（領悟）過程中發生了什麼。因此，我們在 grokking 期間對許多檢查點進行了類似的分析，並跟蹤隱藏狀態與目標預測之間的因果聯絡。這些特徵實際上展示了隱藏狀態與最終預測之間的因果關係。兩者之間的差異被稱為在阻塞期間的變化。

同時，我們還跟蹤了 r1 在第五層的隱藏表示，以及 r2 在第五層的隱藏表示。我們透過大量樣本檢查橋接實體（bridge entity）的排名，以及 r2 在這些成分中的關係。這些特徵非常密集。

總結一下這裡的關鍵發現：首先，我們觀察到 r1 在第五層的隱藏狀態與最終預測之間的因果聯絡顯著增強，這種變化在阻塞期間非常明顯。另一個有趣的現象是，r2 在第五層的隱藏表示逐漸出現，這意味著 r2 關係在阻塞期間得到了保留。此外，r1 在第五層的隱藏狀態始終是橋接實體，這表明原子效應在過擬合之前已經被記憶。因此，橋接實體始終存在，只是它與最終預測之間的因果強度在不斷增強。

基於這些證據，我們認為這表明模型在阻塞期間逐漸形成了操作。在 grokking 之前，模型很可能只是在進行記憶化操作，即將查詢直接與目標關聯。

那麼，為什麼會出現“grokking”現象？我們認為，在我們的模型訓練初期，會形成一個記憶化電路，它直接將輸入與目標預測關聯起來，而無需經過中間步驟。然而，在訓練的後期，隨著模型逐漸泛化，會形成一個泛化路線，這個泛化路線是從記憶化路線中分化出來的。

那麼，為什麼會出現這種分化呢？或者，為什麼記憶化路線會在訓練後期被泛化路線取代？

這是因為在最佳化過程中，模型被激勵去變得更高效。從記憶化到泛化的轉變，我們可以從效率的角度來理解：記憶化路線需要儲存大量的事實，而泛化路線需要支援的事實數量要少得多。

此外，我們還可以從最佳化過程中的權重調整來理解這一點。在 grokking 階段，當模型達到完美的訓練效能後，模型開始最佳化權重，其中權重項會顯著減小。這表明模型試圖找到一種更簡潔的方式來保持相同的訓練精度。

那麼，為什麼這兩個任務並沒有總是實現 OOD 泛化呢？更根本的原因是，Transformer 架構的非遞迴設計阻礙了跨層的記憶共享，從而限制了模型在 OOD 任務中的泛化能力。

我們還嘗試了一個小規模的實驗環境：我們在模型的不同部分共享引數，比如前四層和後四層使用相同的引數，然後我們重新進行訓練，結果發現泛化效能有了顯著提升。但我們沒有等到它完全收斂，就像一個生成器達到完美效能那樣。我們認為這種引數共享的方式能夠解鎖更好的泛化效能，但這只是潛在的一種方法，還有其他方式可以改進架構。

統一符號結構與神經網路表示

Meta GenAI 的田淵棟教授做了主題為“Towards a unified framework of Neural and Symbolic Decision Making”的演講，探討了邁向神經與符號決策的統一框架。

今天，我們仍然能看到大語言模型（LLM）存在一系列問題，關於這一問題有幾種不同的方法可以解決：

首先，當然你可以將越來越多的資料輸入到模型中，希望能夠透過資料量的增加來幫助模型更好地學習；

第二，我們希望利用測試時擴充套件（test time scaling）。也就是說，我們可以使用更大的模型加上工具，或者更大的模型加上思維鏈。透過這種測試時擴充套件，使用不同的策略，我們最終可能會找到一個比單純的大模型更好的解決方案。

最後，我會簡要介紹我們最近的一些理論研究，這些研究試圖將符號結構與神經網路表示統一起來。實際上，透過使用梯度上升（gradient ascent）對神經網路進行訓練，我們可以發現符號結構逐漸出現。透過這種方式，我們實際上看到了符號表示和神經表示在同一框架內的統一。但目前這還處於非常初級的階段，希望未來它能成為主流，但我們還不確定。

就像在第一種選擇中，我們需要大量的計算資源、大量的資料，而且這非常昂貴。所以，我們不確定這種方法是否適用。

第二種選擇是測試時擴充套件。接下來，我會稍微講一下這兩個部分：第一部分是工具的使用，第二部分是使用某種思維鏈。

對於工具的使用，我們實際上可以呼叫外部工具來解決推理問題。以旅行規劃問題為例，我們並不是讓使用者直接向模型提問，而是讓模型首先將使用者的需求轉化為符號形式。這個符號形式能夠準確地描述使用者的需求。然後，結合來自外部的航班和酒店資訊，將這些資訊整合成一個大型的最佳化問題，並透過混合整數線性規劃（一種組合求解器）來解決。

這個求解器會給出最優行程的符號表示，然後你可以透過現有的大模型將其翻譯回自然語言，從而得到由 Agents提供的答案。透過這種方式，你可以得到一個有保證的解決方案。同時，這個過程並不慢。如果你走完整個流程，它實際上是非常快的。

我們基於這個思路構建了一個演示，在兩到三秒內，就能得到一個保證正確的解決方案。當然，這是在使用者請求被準確翻譯的前提下，大模型的翻譯是相當準確的。你可以看到有一個兩秒的延遲，但整個演示仍然可以很好地執行。此外，我們還讓人類標註員進行了測試，他們對結果非常滿意。

當然，如果你考慮到旅行規劃，我們也會希望讓 Agents提出澄清性的問題，也就是說，我們希望 Agents 能夠真正思考使用者請求中缺少的細節，並且判斷 Agents 是否可以提出越來越多的問題來澄清這些細節，以確保他們理解使用者的需求。

這促使我們開展了一項後續研究，探討如何構建多輪對話，以便 Agents 能夠更有效地與人類互動。

我們基本上是透過要求 Agents 遵循 Agents 章程來構建的。也就是說， Agents 需要根據幾項標準進行評估。有些標準是非常客觀的，而有些則是比較主觀的。所謂客觀，是指 Agents 最終需要得到一個準確的答案。同時， Agents 還需要積極主動地針對特定人物提出正確的問題。因此，Agents 在進入實際解決方案之前，還需要高效地完成所有問題的提問和回答。

我們基本上以一種有指導的方式進行了這種直觀的 DPO（可能是某種最佳化方法）和專案取樣，並且我們已經展示了，透過這種方式訓練的 AB 模型在多輪對話的多個方面，相比沒有經過這種訓練的原始 700 億引數模型要好得多。

第一部分是我們實際上可以利用工具來解決複雜的規劃問題。第二部分，我會稍微講一下更大的模型加上思維鏈，以及如何構建思維鏈來解決這些棘手的規劃問題。

為了開始這個話題，讓我們從第一篇論文開始，這篇論文的標題是“Searchformer”。在這篇論文中，我們利用現有的組合求解器的軌跡來構建思維鏈。

當我們思考導航問題時，我們有一個起點和一個終點，然後我們要求模型找出從起點到終點的最短路徑。在任何階段，我們既可以要求人工，標註也可以要求符號求解器對問題進行建模，並透過符號搜尋來解決問題。A*演算法（啟發式搜尋演算法）會開啟一個優先順序表，這個表基本上會找到搜尋中需要探索的下一個正確狀態。

然後，按照探索的方式，我們最終會找到通往目的地的路徑，並且它會保證給你一個最優的軌跡。因此，按照A*演算法的搜尋過程，我們可以構建如下所示的思維鏈。我們從一個提示開始，這個提示是問題規範的表示。

然後，我們可以透過像轉儲整個A搜尋過程一樣來構建一個軌跡。每次A搜尋器在搜尋空間中建立一個新節點時，我們實際上就在軌跡中插入一個建立操作；每次A*搜尋器關閉一個節點時，我們在軌跡中插入一個關閉操作。因此，我們基本上會得到一個很長的軌跡，然後一旦開始找到目標，我們就會插入一個計劃，這個計劃輸出最終的最優軌跡。

這基本上為你提供了一個搜尋增強模型的基本框架。我們有一個作為輸入的提示，同時我們還要求模型生成軌跡和計劃。這與僅輸出解決方案的模型形成了對比。在那些模型中，我們從一個提示開始，然後直接要求它們輸出計劃。

當然，生成的標記（token）數量會有很大不同。這篇論文是在 2024 年年初發表的，那時候，人們還沒有充分意識到使用非常長的思維鏈來解決複雜規劃問題的強大能力。但現在，我認為每個人都已經意識到這一點了，人們開始接受使用非常長的軌跡來解決問題。

我們發現，使用這種帶有軌跡增強的搜尋增強模型時，情況會有所不同。我們看到，如果你只使用僅輸出解決方案的模型，那麼你需要 100 萬樣本才能達到接近 100% 的準確率。但如果你使用搜索增強模型，你實際上只需要十分之一的資料量，同時，你也只需要十分之一的引數量，就能達到類似的效能。所以，搜尋增強模型不僅更簡單高效，而且在引數使用上也更加高效。

這種情況也適用於其他型別的規劃任務，比如讓 Agents 將箱子推到目的地，這需要非常謹慎的規劃。因為如果箱子被推到角落，就沒有回頭路了。

一旦我們有了這些操作模型——這些模型基本上是透過模仿學習實現的——我們可以透過在這些搜尋增強模型的基礎上進行微調來做得更好。具體來說，我們可以透過微調這些原始模型，使其生成更短的軌跡，但仍然保持最優的計劃。這其實是一個非常典型的強化學習任務，因為目標是明確的，但我們不知道如何實現這個目標。所以，我們讓強化學習 Agents 去探索並找到解決方案。

透過“Searchformer”，我們發現最終得到的模型比原始的 A* 搜尋模型更好，因為它具有更短的搜尋軌跡。這是由於採用了“直觀地址取樣”（Intuitive Address Sampling），這是一種簡化的強化學習版本。

從資料上看，我們發現減少後的軌跡與原始A*軌跡之間的比例越來越高，這意味著從數值上來看，這種情況確實存在。

不僅如此，我們還發現，不僅軌跡變得更短，而且經過微調後的效能也在不斷提高。每次迭代後，解決方案達到最優的比例越來越高。在這種情況下，你已經可以看到，擁有 45M 個引數的模型——這裡的引數指的是模型的引數數量——實際上可以與用 700M 個引數訓練的模型相媲美，而後者是用一個更大的資料集進行訓練的。

這非常有趣，我相信這是最早展示在測試時間和訓練推理資料上存在某種“皮膚法則”（可能是指某種最佳化或提升效能的規律）的少數論文之一，這種法則有可能提高閱讀任務的效能。

我們還有一篇論文叫作“DualFormer”。在這篇論文中，我們嘗試減少用於訓練的軌跡的大小和長度。你可以隨機地丟棄一些搜尋軌跡中的token。

論文連結：https://arxiv.org/abs/2410.09918

這種丟棄 token 的方式可以有很多種。例如，你可以丟棄所有帶有成本的子句，甚至你還可以直接丟棄整個軌跡。這意味著我們實際上是在解決方案資料和搜尋增強資料的混合體上進行訓練。

這種訓練方式非常有趣，最終得到的模型也非常強大。因此，我們最終得到了這種雙模式模型，它可以自動在快速模式（即直接給出答案）和慢速模式（即透過思維鏈給出答案）之間切換。也就是說，你可以擁有一個同時具備這兩種能力的模型，並且它在兩種模式下都比單一模式的專用模型表現更好。

我們在兩種模式之間切換方式非常簡單——你只需要讓雙模式模型的第一個生成標記要麼是搜尋開始標記，要麼是計劃標記，這樣模型就會直接給出最優答案。也就是說，你只需要固定第一個標記，模型的行為就會大不相同，它會表現出快速模式或慢速模式的效能。

經過訓練，我們發現這種模式比單獨的快速模式更好，也比單獨的慢速模式更好。這是一個非常有趣的發現。

我們還注意到，DeepSeek 也表現出類似的行為。在 DeepSeek 的同步模式中，有一些技巧。如果你有兩個空格，在同步 token 之後，模型生成的同步序列往往會更長一些。如果你在同步 token 之後只有一個返回，那麼模型生成的內容往往會更短一些。

我認為這可能是因為他們用來訓練模型的資料具有這種特定的結構，而模型在學習過程中會捕捉到這些結構，從而作為一種副作用來控制模型的行為。我們很高興看到這種行為也出現在最先進的大型模型中。

我們也將雙模式模型應用於數學問題，基線模型會有一個非常長的思維鏈。但一旦你隨機丟棄一些句子，並用這些資料進行微調，會非常驚訝地發現，序列的長度會基本保持不變，同步標記會變得非常短，而且短得多。同時，生成的內容仍然是合理的，並且能給出正確的答案。

這種行為挺有意思的。我們是在基礎模型上進行這種大規模微調。這些是基礎模型，它們並不是針對特定任務最佳化的，所以效能並不算出色。但即便如此，你仍然會看到效能有所提升。

基於 API 的網路智慧體

卡內基梅隆大學的 Graham Neubig 教授做了主題為“LLM Agents that Learn from Experience”的演講，展示了其近期一項名為“Beyond Browsing: API-based Web Agents”的研究工作。

論文連結：https://openreview.net/forum?id=TPiJKs7ccR

我們實現了一個基礎的瀏覽 Agent。它基於無障礙功能樹執行，能夠在簡單佈局的網頁上合理地導航並填寫表單。這就是我們的基線模型，也是我們在“Agents工作流記憶”論文中所使用的基線模型。

但挑戰在於無障礙功能樹結構的複雜性，許多語言模型對此並不熟悉。當內容並非立即可見時，導航也會變得棘手，因為你需要滾動頁面、切換頁面，以及其他類似的操作。

一個失敗的例子是詢問：“Saptaks 對 Allyproject 做了多少次提交？”於是， Agents嘗試進行瀏覽，它試圖訪問 GitLab.com，使用憑據登入，點選專案，點選提交記錄，然後不斷向下滾動、向下滾動……最終，它耗盡了時間，並得出結論說沒有找到任何提交記錄，因此它認為沒有提交發生，提交次數為零。

另一方面，我們還有另一種與環境互動的介面。這可以是像呼叫API這樣的方式。它為機器與網路服務之間的通訊提供了一個直接的介面，減少了操作複雜性，並且理想情況下，我們會得到更好的結果。

如果我們看看 API，它們是預定義的端點，允許計算機高效地執行任務，並透過 GET、POST、PUT 等請求實現互動，返回結構化資料，比如 JSON。有趣的是，我們在標準基準測試（比如 Web）中使用的許多網站已經提供了 API，所以在許多情況下，這些 API 已經存在。如果我們能夠恰當地使用它們，我們就可以透過 API 與這些網站進行互動。

在許多情況下，我們已經這樣做了。但有時，雖然有API，但文件並不完善。不過幸運的是，這也是語言模型擅長的事情。你可以直接讓語言模型為 API 生成文件。

這是一個例子，在一個 API 文件中，它會告訴你屬性的型別、屬性的描述，以及 API 的輸出會是什麼，以及你可以如何執行呼叫。API呼叫本質上是透過呼叫程式碼實現的。你可以使用requests.get這樣的請求，而這就是一個響應的例子。

我們考察的是，如果我們把傳統上由瀏覽 Agent 解決的任務，讓 AI Agents 透過 API 來完成，會怎麼樣呢？

這是我們基於 API 的 Agents。我們的實現方式是使用我們 Agents 框架中的標準編碼 Agents（OpenHands），並以我接下來會講的方式，為它提供對 API 的訪問。

在過去，我們需要在網站上一步步地操作，執行許多不同的步驟，以及其他類似的操作。但在這種情況下，你只需要用三行 Python 程式碼就能解決任務。

那麼，問題來了，你知道的鑑於 API 呼叫的好處，我們應該完全拋棄網頁瀏覽嗎？當然，答案是否定的。如果我們檢視一百個隨機抽樣的任務的錯誤分佈，當我們將 API 提供給模型時，會發現其中大約三分之一的任務實際上是正確的，但 WebArena 的驗證器卻判定它們是錯誤的，而另外 50% 的任務根本無法透過 API 解決。

原因在於，並非所有網站都提供全面的 API 支援。它們並非都有完善的 API 文件，而且網站的深度複雜性也是一個問題。

因此，我們提出的一個解決方案是建立一個混合 Agent。這種 Agent 能夠交替執行瀏覽和 API 呼叫操作，並且在每一步中，它會選擇與人類溝通、生成自然語言、執行 Python 程式碼（包括API呼叫）以及執行網頁瀏覽操作。

我們根據當前可用的 API 的質量來選擇操作：

我們提示 Agent，如果存在足夠的 API，就應該嘗試使用 API。但如果足夠的 API 不存在，它就可以回到瀏覽模式。在其執行軌跡的最後，當它完成了所有需要做的事情後，我們要求 Agent 訪問一個能夠為使用者提供答案的網頁。這樣做的想法是，它可能會使用 API 呼叫，但最終會將結果展示在網頁上。這也符合 WebArena 評估的要求，即需要訪問特定的 URL。

我們在 WebArena 上評估了我們的 Agents框架。我們使用了 OpenHands，這是我們正在開發的一種兼具編碼和瀏覽功能的 Agent。

如果你檢視 Agent 的效能，我們在多個網站類別上對其進行了評估，發現在某些特定類別上轉向使用 API 後，效能有了顯著提升。例如，在 GitLab 和地圖上，轉向使用 API 後效能大幅提升；而在 Reddit 和管理類網站上，轉向使用 API 後效能提升較小，但當我們切換到使用混合 Agent 時，效能有了更大的提升。

那麼，問題可能就來了，為什麼會這樣呢？其中一個原因是 API 的質量很重要。GitLab 和地圖的 API 非常好，它們允許你完成在這些網站上需要做的大多數事情。而購物和管理類網站的 API 還算可以，但在 Reddit 風格的任務中，API 的覆蓋範圍非常差，這導致了在 Reddit 上使用 API 的效果不佳。

我們所做的就是查看了所有的 API，並且編寫了一些新的 API。雖然數量並不多，但我們手動編寫了幾個，這使得在 Reddit 上使用 API 的 Agent 的準確率翻了一番。所以，擁有高質量的 API 對於網站來說是很重要的。

但就這項工作的未來方向而言，其中之一是獲取或生成合適的 API。那麼，我們如何能夠自動生成網站的 API，以便我們能夠呼叫一個函式，而無需 Agent 事先具備該函式、以及改進端點的檢索和利用？我們可能會有非常豐富的 API，如何從中篩選出我們需要的部分呢？

未來需要我們繼續探索，探索的方向如下：

AI 新前沿：形式化數學推理

加州大學伯克利分校的 Dawn Song（宋曉冬）教授做了主題為“Formal Mathematical Reasoning: A New Frontierin Al”的演講，探討了 AI 的新前沿——形式化數學推理。

論文連結：https://arxiv.org/abs/2412.16075

AI 在形式化數學中有廣泛應用。事實上，我們可以利用各種經過形式化驗證的工具，比如定理證明器等。而且，實際上存在許多不同型別的定理證明系統。

例如，在 Lean 中，當我們使用 AI 進行形式化時，本質上有一個工作流程。一旦我們有了形式化的定理陳述，我們就希望使用定理證明器來生成形式化證明。

在這一過程中，這一步是 AI 可以自動化的步驟之一。然後，生成的形式化證明和經過驗證的定理可以被納入形式化數學庫。

此外，我們可以使用自動形式化（auto formalization）將非形式化的數學內容轉換為形式化的數學陳述。

在這個工作流程中， AI 可以在多個步驟中提供幫助。其中一個關鍵步驟是，給定一個定理陳述，我們需要進行證明搜尋，以遍歷證明樹，最終找到一個有效的證明。我們希望利用 AI ，特別是利用這些大語言模型，能夠構建出 Proof Agents，從而使這一證明搜尋步驟自動化。

此外， AI 還可以幫助自動形式化，即將自然語言中的非形式化數學陳述轉換為形式化的數學定理陳述。例如，最新的研究和模型已經展示瞭如何利用大型語言模型（如 Goedel-Prover）將自然語言數學問題翻譯成形式語言（如 Lean 4），並自動生成完整的證明。這種自動形式化技術為數學形式化推理提供了新的可能性，顯著提升了數學問題的形式化和證明效率。

近期 AI 在形式化數學領域也取得了許多進展。例如，谷歌 DeepMind 的 AlphaGeometry 2 在解決國際數學奧林匹克競賽（IMO）幾何問題上取得了接近金牌水平的成績。此外，Goedel-Prover 作為開源的形式化推理模型，透過將自然語言數學問題翻譯成形式語言（如 Lean 4），並自動生成完整的證明，顯著提升了形式化數學問題的解決效率。

儘管整個社群已經取得了非常顯著的進展，但我現在想簡要介紹一下一些開放性挑戰和未來發展方向。

首先就是資料問題。

一般來說，在數學領域，尤其是形式化數學中，我們面臨資料稀缺的問題。例如，對於訓練Code Llama，其訓練資料集大約有 5000 億個 token，但當我們看這些證明時，可用的證明資料量卻遠遠少於這個規模，甚至相差幾個數量級。因此，對於這些領域，開發各種方法來解決資料稀缺問題顯得尤為重要。

為了解決形式化資料的稀缺問題，幸運的是，我們確實有一些很有前景的方向，可以提升這些形式化資料的可用性。

首先是透過自動形式化來建立資料。這種自動形式化本質上是訓練大型語言模型，使其能夠將非形式化的數學內容自動轉換為形式化的數學陳述。

鑑於我們有大量的非形式化數學內容，比如教科書和其他各種材料，透過成功的自動形式化，我們可以自動地生成這些形式化的數學陳述。我們最近在利用反饋迴圈來改進大型語言模型的自動形式化方面，已經看到了令人興奮的進展。

另外，最近我也瞭解到，AlphaGeometry 能夠支援形式化步驟，生成大約 1 億個形式化問題陳述。這也顯著促進了它在最近的國際數學奧林匹克競賽（IMO）中取得的成功。

此外，AlphaGeometry 在 IMO 中的成功還歸功於它生成合成資料的另一種方式。它通過幾何規則生成了 1 億個合成定理和證明，從而幫助它成功解決了 IMO 中具有挑戰性的幾何問題。這也為解決資料稀缺問題提供了一個很好的例子。

解決資料稀缺問題的另一個有前景的方向是合成數據生成，我們稱之為“神經猜想”（neuro conjecturing）。

其核心思想是，可以開發模型來為定理和引理生成猜想，然後利用定理證明器嘗試自動證明這些猜想。如果成功生成了證明，那麼這些經過驗證的猜想就成為了定理和引理，並可以被新增到陳述和證明的庫中。

這可以幫助產生額外的資料，進一步幫助訓練模型，使其在生成更好的猜想和證明方面表現得更好。到目前為止，我們已經在相對簡單的引理和定理上看到了這方面的進展，因此未來我們可以在這方面努力，顯著提高能夠猜想和證明的定理的可擴充套件性和難度水平。

在這一領域，我們需要解決許多不同的演算法挑戰。例如，對於自動形式化，我們該如何擴充套件自動形式化？我們如何高效且有效地進行證明搜尋？我們如何利用理論改進中的層次結構，以及如何真正學習數學抽象？此外，我們如何利用現有的數學知識，以及如何調和專家型和通才型方法？

首先是，我們如何真正實現大規模的自動形式化？在進行自動形式化時，實際上存在許多挑戰。

因為我們進行自動形式化時，並沒有後續的驗證步驟，所以我們無法確切知道其他形式化的陳述是否真正正確。我們需要對它們進行評估，並且需要開發良好的指標來評估這些形式化的陳述。

此外，我們還需要能夠自動驗證這些自動形式化的陳述，理想情況下是利用改進的形式化步驟等。因此，我們的期望是，對於複雜的自動形式化任務，我們實際上可以將其分解為更小的步驟，然後與形式化系統進行互動以提供幫助。

對於評估自動形式化的陳述，有幾個原因使其相當具有挑戰性。首先，我們不能依賴人工評估，因為這種方法無法擴充套件。而對於其他形式化的陳述，通常存在不同的形式，即存在多種正確的方式來完成形式化，而自動等價性檢查本身其實並不簡單。

因此，為了應對這一挑戰，我們需要利用像以太坊證明器這樣的正式驗證系統。我們希望藉助定理證明器的反饋，迭代式地改進自動形式化。

另一個挑戰是如何更高效、更有效地進行證明搜尋。這當然是使用 AI 進行形式化數學的一個關鍵目標。對於理論改進，有許多不同的方面和組成部分。我們可以做的是，從本質上提升證明搜尋的能力。

推理時間計算的擴充套件（即擴大推理時的計算量）對提升這些模型的通用推理能力非常有幫助。我們希望，增加測試時的計算量也能幫助加速證明搜尋，這本身也是非常自然的契合。

此外，我們還希望開發更好的價值模型，以幫助評估和優先排序不同的證明目標，以及證明搜尋樹的不同部分。同時，我們希望系統地評估模型和搜尋演算法，並設定引數，以便能夠開發出更適合證明搜尋的模型。

到目前為止，我們已經看到，擴大測試時的計算量對於提升模型的推理能力非常有效。比如在 AlphaGeometry 和 AlphaProof 等專案中，理論改進是一個非常自然的方向。透過在證明搜尋過程中增加計算量，我們可以幫助提升模型的證明搜尋能力。

另一個重要話題是我們如何引導並更好地優先排序研究。特別是，我們需要開發更好的價值模型，以幫助評估和優先排序證明目標。因此，一個關鍵的挑戰和未來方向是如何更好地訓練價值模型，以及我們如何獲取更好的資料並利用獎勵模型（RM）來幫助解決這些問題。

目前在形式化數學中使用 AI 的方法，例如 DeepSeek Prover 等工具，通常是直接生成完整的證明，而沒有充分利用證明搜尋。這種方法雖然在某些情況下有效，但缺乏對不同搜尋演算法（如蒙特卡洛樹搜尋、最佳優先搜尋等）的整合。因此，我們希望對這些不同的演算法進行系統性評估，以開發出更好的解決方案。

另一個開放性挑戰和正式的研究方向是，我們希望更好地利用定理證明中的層次結構。特別是在理論證明中，當你面對一個複雜的定理時，通常即使是數學家手動證明時，也會將這些複雜定理分解為一些不同層次的高階證明目標，以及一些不同的高階引理等。然後，這些複雜的定理會被進一步分解為更小的目標，依此類推。

這很重要——正如我們在形式化數學中應用 AI 一樣，我們也需要開發具備這種能力的模型，能夠逐步將高階證明目標分解為更小的目標。

所以，我們並不是主張用形式化數學的 AI 來取代非形式化數學的 AI。事實上，非形式化數學的 AI 和形式化數學的 AI 之間存在著一種自然的協同作用。重要的是將兩者結合起來，本質上是將非形式化推理的靈活性與形式化推理的嚴謹性結合起來。

例如，對於非形式化的陳述，我們可以嘗試對其進行自動形式化，然後利用形式化驗證和改進等手段來驗證其正確性。對於非形式化的定理陳述，以及用於非形式化數學的模型，它們可以幫助生成例如非形式化的證明草圖，這些證明草圖隨後可以被轉化為形式化的證明草圖，並最終生成經過驗證的形式化證明。

透過這種方式，非形式化數學部分可以幫助提升生成形式化證明的可擴充套件性、靈活性以及提供高層次的直覺，而形式化證明則可以為這些非形式化證明提供驗證。沒有這樣的形式化驗證，就無法真正推理並確保非形式化證明的正確性。

即使是數學論文和密碼學論文等領域的非形式化證明，有時也會出現錯誤。而對於 AI 生成的非形式化證明，出現錯誤和漏洞的可能性甚至更高。因此，將非形式化和形式化結合起來，最終生成經過形式化驗證的證明，是非常重要的。

透過將兩者結合起來，模型可以生成多種非形式化的解決方案，最終，正確的解決方案將被形式化地驗證。

另一個對於數學的可擴充套件性等來說也很重要的是學習數學抽象。

具體來說，無論是人類數學家還是數學系統，一般來說，這些抽象——比如開發新的定義和元素——實際上對於解決更復雜的數學問題至關重要。

我認為，這尤其是一個令人興奮的領域和方向。對於形式化數學中的 AI 而言，這不僅是一個挑戰，也是對模型創造力的考驗，即模型如何學會構建這些新的定義、引理和策略，並將其應用於完整的證明輔助中，以便在未來證明中也能被利用。

最近在學習簡單的證明策略方面已經取得了一些進展，這些策略是透過引導式的方法從智慧體自身解決數學問題的過程中得來的。我認為這是一個非常有前景且令人興奮的領域，即我們如何能夠本質上訓練模型以及證明智慧體，從而使其能夠更好地從自身以往的經驗中發現並學習抽象。

隨著我們持續推動這一正向迴圈，我們將繼續生成新的資料，並透過自動形式化等方式，不斷擴大定義、數學陳述、定理等的庫。在證明搜尋過程中，能夠利用庫中現有的知識來檢索相關的定理和陳述等，對證明 Agents 來說是非常有幫助且至關重要的。因此，一個開放性挑戰和未來方向是如何設計出更適合這種形式的數學以及利用這些數學庫的更好的模型和檢索機制。

另一個有趣的問題是，如何調和專家型和記者型的方法。記者型方法能夠識別跨領域的聯絡，而專家型方法則在各個具體領域中表現出高效性。我們希望可以將這兩種方法結合起來，例如透過為模型配備特定領域的工具等方式。

現在，我將簡要談談兩個主要應用領域的開放性挑戰和未來發展方向，一個是在輔助人類數學家發展更好的數學，另一個是在程式生成、共生成和驗證領域。

對於形式化數學（AFFMO），其動機和價值在於，我們希望這些工具能夠真正幫助人類數學家透過解決具有挑戰性的數學問題、開發新的定理和證明等，在形式化數學領域取得進展。

我們希望利用 AI 開發出更好的工具，融入數學研究的工作流程中，為人類數學家提供證明輔助，與人類數學家攜手合作，共同攻克具有挑戰性和前沿性的數學問題，生成相關證明等。

為了使這些工具真正發揮作用，本質上我們需要開發更好的工具，這些工具不僅用於自動化寫作，生成自動化的證明步驟，還需要更好地理解數學家如何使用 AI ，比如開展行為研究來觀察數學家與 AI 的互動。最終目標是為數學家開發出更好、更有用的工具。

我們希望藉助這些工具，能夠真正實現大規模的分散式協作，讓分佈在全球的數學家與 AI 工具攜手合作，將大型專案分解為不同的元件，整個社群共同攻克具有挑戰性和複雜性的數學問題。

另一個非常重要的應用領域是程式碼生成和程式驗證。

它的目標不僅僅是利用 AI 來解決數學問題，更重要的是，它可以幫助從程式驗證的角度來構建正確且安全的程式。

如今，與 LLaMA 相關的程式碼生成已經得到了廣泛的應用。有估計表明，在一些公司和專案中，超過 50% 的程式碼現在是由LLaMA生成的。但與此同時，確保生成程式碼的正確性和安全性面臨著巨大的挑戰。例如，通過幾個測試用例可以看到 AI 生成的程式碼不一定是正確的。

所以，我們不應該僅僅生成程式碼，而應該進行可驗證的程式碼生成——即在生成程式碼的同時，還要生成程式碼的形式化規範、以及證明生成的程式碼符合這些形式化規範的形式化證明。

比如我想為這個問題生成程式碼，計算變數的絕對值函式，那麼我們實際上可以生成程式碼的規範，同時也能生成證明。透過這種方式，就可以確保生成程式碼的正確性。

綜上，我已經討論了 AI 在形式化數學領域的多個不同方向和應用領域中的開放性挑戰和未來發展方向。

我認為，在這個領域，接下來的五年將會非常令人激動。我們希望將整個社群凝聚在一起，共同推動 AI 在形式化數學和定理證明領域的發展。

Goedel-Prover：自動定理證明領域的開源模型

普林斯頓大學的金馳教授做了主題為“Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving”的演講，探討了Goedel-Prover這一開源的大模型，透過將自然語言數學問題翻譯成形式語言（如 Lean 4），並生成形式化證明，從而解決形式化數學陳述和證明稀缺的問題。

在這次演講中，我會介紹我們開發的系統：Goedel-Prover。這個名字來源於 Gödel（哥德爾），一位在形式化系統領域非常著名的數學家。Goedel-Prover 是一個開源模型，在自動定理證明方面達到了當前的最佳效能水平。

論文連結：https://arxiv.org/abs/2502.07640

我首先會稍微談談評估，因為我之前提出了一個比較大膽的主張，說我們達到了最佳效能水平。所以，這就引出了一個問題：我們如何評估模型，以及我們如何判斷一個模型是好的，另一個模型是不好的。

正如前述，形式化數學的一個重大挑戰是資料稀缺。現有的訓練資料和評估方式在某種程度上是有限的，這是開源社群中主要的資料集和基準測試。訓練資料本質上是既包含 Lean 中的問題陳述，也包含 Lean 中的證明。

也就是說，我們為你提供了這些問題陳述的形式化證明，還有評估資料集，其中很多資料集只包含問題陳述，沒有證明。也就是說，我們需要讓模型自己生成證明，並讓 Lean 編譯器檢查這些證明是否正確。

其中非常著名的一個是資料集 MiniF2F。很多模型都在這個資料集上進行了評估。它包含了不同難度級別的數學問題，有些非常難，有些則相對簡單。

所以，很多事情都會集中在 MiniF2F 基準測試上，我們會說它包含 244 個驗證問題和 244 個測試問題。這些問題涵蓋了極具挑戰性的數學問題，比如國際數學奧林匹克競賽（IMO）、AIME（美國數學邀請賽）、ACM（美國計算機協會）相關問題，以及不同難度級別的代數問題（從5級到1級）和數論問題（從5級到1級），還有許多其他型別的問題。

在我們討論完評估資料集之後，我們還會評估效能。我們還希望討論一下在我們之前，什麼是最佳模型（SOTA，State of the Art）。為了能夠進行非常公平的比較，生成這種形式化數學的系統主要有兩種型別：

一種是整體證明生成的風格。本質上，你有一個語言模型，它會在給定問題的情況下一次性生成整個證明。一個具有代表性的模型是 DeepSeek Prover，比如 DeepSeek v1 或 DeepSeek v1.5。評估這類模型的一個非常重要的指標是，你需要生成多少個證明（比如你取樣了多少個證明），才能得到一個正確的證明。

換句話說，我們可能會說“透過率達到32次/6400”，這意味著你實際上生成了大約20萬個證明，只要其中有一個證明是正確的，有一個證明通過了Lean編譯器的驗證，我們就可以說我們解決了這個問題。因此，“透過率”是一個在評估整體證明生成中非常重要的指標。

另一種型別是樹搜尋方法。與一次性生成整個證明不同，這種方法是逐步生成的。在生成一步之後，我們會使用某種樹搜尋演算法，比如廣度優先搜尋或最佳優先搜尋等，來搜尋可能的最佳下一步。一些代表性模型，比如InternLMs 和 AlphaProof 系統（我認為它既用於幾何問題，也用於代數問題），都採用了這種基於樹的方法。

我們只與整體證明生成系統進行比較，因為我們的模型 Goedel-Prover是一個整體證明生成系統。不過，我們也有其他方法可以與開源的樹搜尋方法和內部方法進行比較。我們沒有與 AlphaProof 進行比較，因為它是一個閉源系統，儘管它的效能非常好，但到目前為止，該模型並未開源。

首先，我會關注小型化資料集。我們在路徑集32上進行了評估，此前的最佳水平是DeepSeek Prover，他們在經過監督微調或強化學習後有一些變體。在路徑32上，這是一個相對較小的預算，比如取樣推理時間，他們達到了大約50%的準確率。而我們的模型在路徑32上達到了57%的準確率，比之前的最佳水平高出7個百分點。

你也可以問，當我們增加推理計算量時，我們的模型表現如何。這就是這張圖展示的內容。我們可以看到一些一致的改進，我們的模型與DeepSeek Prover之間大約有7個百分點的效能差距。

第二點是，我們還希望在 PutnamBench 上評估我們的模型。這是一個包含所有永久性數學競賽問題的基準測試，這些問題極具挑戰性。我們在該基準測試中獲得了第一名，解決了七個問題。我認為第二名的模型也解決了七個問題，但它不是開源的。我們排名第一，是因為我們實際上使用了更少的推理時間和計算資源，我們通過了512。

其他一些成果，比如我們之前提到的 Lean-Workbook，它是一個龐大的訓練資料集，但不幸的是，其中只有很小一部分訓練資料是有證明的。比如，他們提供了大量的問題陳述，但其中只有很小一部分問題陳述附有證明。

因此，以前的模型或者現有的所有工作，總共只能找到大約 1.5 萬到 5 萬份 Lean-Workbook 的證明，而我們的模型能夠找到大約 3 萬份，幾乎是之前找到的證明數量的兩倍。這也在我們測試的多個數據集上得到了體現，包括miniF2F、ProofNets 和 FormalNuminous，這些是我們用作基準的內部資料集。

在介紹完我們的效能之後，我還想稍微說一下我們是如何實現這一成果的。

事實證明，我們的整體方法並不複雜，這正是我喜歡的——它非常簡單且清晰，我認為這作為一個起點，對於推動自動定理證明的發展是非常好的。

形式化數學中最關鍵的挑戰之一就是資料稀缺。

儘管 DeepSeek 聲稱他們形式化了很多大型資料集，但不幸的是，在開源社群中，可用的資料集和資料非常稀少。你可以看到，我們大約有 1000 萬非形式化的問題，但形式化的問題陳述卻少得多，例如，我們只有大約 40 萬形式化的問題陳述，以及僅有 1.5 萬個形式化的證明，這個數量是非常非常少的。基於這樣少量的資料，要訓練出一個好的證明器是非常困難的。

所以，我們首先需要做的是獲取更多形式化陳述，以便我們能夠獲得更好的訓練基礎，我們需要獲取更多的陳述和更多的證明。對於陳述，我們採用了自動形式化的途徑。因此，我們首先收集了大量既有形式化又有非形式化陳述的配對。這些是我們同時擁有形式化和非形式化陳述的數學問題。我們從 Lean-Workbook 中獲取了 14 萬個這樣的配對，它們同時提供了形式化和非形式化的陳述；此外，我們還從雲端生成了另外 17 萬個配對。

第二件事是我們需要訓練一個形式化器，因為僅僅 10 萬個問題陳述是不夠的。為了做到這一點，我們訓練了我們自己的形式化器。我們從 Qwen2.5-32B 模型開始，將這些形式化和非形式化的陳述配對輸入其中，最終得到了我們的形式化器。一旦我們有了形式化器，我們就可以處理一個更大規模的非形式化資料集。在這一過程中，我們特別使用了 Numina 資料集，它包含了大約 80 萬個高質量的數學問題。我們將這些非形式化的問題形式化為形式化陳述。

關於直接進行自動形式化陳述，存在一些問題：

第一個問題是，它可能會產生大量語法錯誤。例如，我們需要在 Lean 中形式化這些陳述，但其中一些可能語法錯誤，無法透過 Lean 編譯器的驗證。因此，我們會進行編譯正確性測試，本質上就是部署 Lean 編譯器。如果編譯器無法透過，例如返回一些錯誤提示，我們會要求模型進行修正。

第二個問題是，即使語法正確，形式化後的陳述可能與原始問題完全不一致。例如，非形式化的問題可能是這樣的，但形式化後的問題可能缺失了一些條件，或者最終變成了一個完全不同的問題。在這種情況下，我們無法像在大學裡那樣部署人力去人工檢查所有陳述，因為我們沒有足夠的人力資源。

因此，我們會使用“四重完整性測試”，本質上是要求四個大型語言模型作為獨立的裁判，獨立判斷這些問題是否是正確的翻譯，並基於一系列標準對語言模型進行提示。然後，我們會要求它們進行多數投票。經過這些流程後，我們最終得到了超過一百萬條能夠透過這兩項測試的形式化陳述，並將這些陳述用作我們的訓練資料集。

需要注意的是，這僅僅是關於問題陳述，而不涉及證明。那麼在我們得到了這些問題之後，如何獲取更多的證明呢？我們使用這種迭代訓練的方法。這是一個獲取更多證明的流程。

我們會從某個基礎模型開始。當我們有了基礎模型後，比如 Goedel-Prover 的第一版，它基於 DeepSeek Base 7B模型。我們將大量的形式化陳述輸入其中，然後進行推理，證明器能夠生成一些證明。在生成了一些證明之後，我們將它們提交給 Lean 編譯器，Lean 會驗證這些證明。我們會發現其中一些證明是正確的，然後將這些正確的證明加入到我們的資料集中，用於下一輪訓練。

透過這種迭代訓練的方式，我們可以獲得越來越多的證明，並將越來越多的形式化證明加入到我們的資料集中。我們能夠基於越來越多的證明進行訓練，這就是我們獲取更多形式化證明的方法。

表格如下：我們在進行迭代訓練時，不僅在不斷增加更多的證明，還在迭代地增加更多的陳述。這樣，當一個模型的容量更大時，隨著我們增加更多陳述，模型的表現也會更好。

我們在一開始並不會增加太多陳述，原因有兩個：一是為了節省計算資源；二是為了避免讓模型過於困惑。因此，我們會逐漸增加輸入到資料中的陳述數量。我們把這些陳述輸入到我們的證明器中生成證明，並且可以看到我們的模型持續地、穩定地解決更多問題，並基於 Lean 工作手冊以及 Lumina 資料集生成更多的證明。