在 DeepSeek 能夠破圈而出的一眾原因中，完全摒棄傳統(tǒng)的監(jiān)督微調(diào)（SFT）、轉(zhuǎn)而采用大規(guī)模強化學(xué)習(xí)（RL）的創(chuàng)新之處是關(guān)鍵所在，這使得模型推理能力在質(zhì)上取得顯著突破，更證明了強化學(xué)習(xí)在提升大語言模型推理能力方面的巨大潛力。

近幾年，學(xué)界和業(yè)界關(guān)于 RL 和 LLM 也涌現(xiàn)出了頗多具備開創(chuàng)性意義的研究成果。在 AI 智能體推理與決策研討會（AIR 2025）上，來自倫敦大學(xué)學(xué)院、加州大學(xué)伯克利分校、普林斯頓大學(xué)、華盛頓大學(xué)、卡內(nèi)基梅隆大學(xué)、Meta、華為等多位學(xué)術(shù)界和工業(yè)界的研究人員圍繞強化學(xué)習(xí)、推理決策、AI 智能體展開討論，回答了諸多問題，例如：

AI 系統(tǒng)如何模擬類人推理和決策過程？

最新的算法、框架和工具如何支持在不確定性下進(jìn)行穩(wěn)健的決策？

如何確保 AI 的決策過程是道德的、透明的且公正的?

……

從一系列前沿的推理決策研究中，可以看到 DeepSeek 的影子。2023 年，來自華盛頓大學(xué)的 Hanna Hajishirai 教授團(tuán)隊發(fā)布了一項關(guān)于大語言模型推理的開放訓(xùn)練方法的工作，研究強調(diào)，為了從預(yù)訓(xùn)練模型發(fā)展到最終模型，需要經(jīng)歷了三個階段：指令微調(diào)、偏好微調(diào)以及具有可驗證獎勵的強化學(xué)習(xí)。而這一方法也是 DeepSeek 所采用的推理開放訓(xùn)練方法。

Meta GenAI 的田淵棟教授系統(tǒng)總結(jié)了當(dāng)下應(yīng)對大語言模型局限的解決方式，除了 Scaling Law 之外還有Test-time Scaling（測試時擴(kuò)展），即使用更大的模型加工具或思維鏈，使用不同的策略，最終可能會找到一個比單純的大型模型更好的解決方案。田淵棟教授也分享了通過使用梯度上升（gradient ascent）對神經(jīng)網(wǎng)絡(luò)進(jìn)行訓(xùn)練的方式，從而試圖將符號結(jié)構(gòu)與神經(jīng)網(wǎng)絡(luò)表示統(tǒng)一起來，但這一方法還處于非常初級的階段，并不確定未來是否能成為主流。

俄亥俄州立大學(xué)的 Huan Sun 教授從隱式推理出發(fā)，探討了數(shù)據(jù)集中的兩種事實：原子事實與推斷事實，并提出了一個與主流不相同的研究發(fā)現(xiàn)：泛化速度與絕對數(shù)據(jù)量并沒有關(guān)系，而是與關(guān)鍵數(shù)據(jù)分布、特別是推斷事實與原子事實的比例密切相關(guān)，且比例越高，泛化速度就越快。

同時，也有研究圍繞 AI for Math 這一主流的推理能力應(yīng)用領(lǐng)域。普林斯頓大學(xué)的金馳教授團(tuán)隊開發(fā)了Goedel-Prover 這一開源的大模型，通過將自然語言數(shù)學(xué)問題翻譯成形式語言（如Lean 4），并生成形式化證明，從而解決形式化數(shù)學(xué)陳述和證明稀缺的問題，這一模型在自動定理證明方面達(dá)到了當(dāng)前世界范圍內(nèi)的最佳性能水平。

更有實用性較強的 AI 智能體研究?？▋?nèi)基梅隆大學(xué)的 Graham Neubig 教授團(tuán)隊提出了一個混合 Agents 方案，這種 Agents 能夠交替執(zhí)行瀏覽和 API 調(diào)用操作，并且在每一步中，它會選擇與人類溝通、生成自然語言、執(zhí)行Python代碼（包括API調(diào)用）以及執(zhí)行網(wǎng)頁瀏覽操作。

AIR2025 由倫敦大學(xué)學(xué)院汪軍、Meta GenAI 田淵棟等教授聯(lián)合主辦，致力于推動智能系統(tǒng)的發(fā)展，使其能夠自主、適應(yīng)性強且負(fù)責(zé)任地運行（會議詳情及注冊可訪問官網(wǎng)：https://ai-agent-reasoning.com）。本次會議特別鳴謝來自加州大學(xué)伯克利分校的博士后研究員顧尚定。

這是一篇圍繞 DeepSeek 的過去、當(dāng)下與未來所展開的對人工智能的精彩討論。AI 科技評論截取會議部分精彩內(nèi)進(jìn)行編譯，以下為核心內(nèi)容的演講實錄：

一、DeepSeek 的語言模型推理開放訓(xùn)練方法

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

為了從預(yù)訓(xùn)練模型發(fā)展到最終模型，我們經(jīng)歷了三個階段：指令微調(diào)、偏好微調(diào)以及具有可驗證獎勵的強化學(xué)習(xí)。這是我們 2023 年論文中引入的新內(nèi)容。這基本上也是 DeepSeek 所采用的方法，后來我們發(fā)現(xiàn) DeepSeek 也引入了同樣的方法。

我們先來談?wù)勚噶钗⒄{(diào)。指令微調(diào)中，人們也把它稱為 SFT，即監(jiān)督式微調(diào)。其核心思想是，你拿一個預(yù)訓(xùn)練的語言模型，然后向模型輸入各種不同類型的任務(wù)指令，接著對模型進(jìn)行微調(diào)，教會它如何遵循這些指令。

我們團(tuán)隊在這個方向上已經(jīng)投入了很長時間。我們在 2022 年開始專注于語言模型的指令微調(diào)，當(dāng)時主要關(guān)注的是自然語言處理（NLP）標(biāo)簽等語言測試。

2023 年，我們引入了一個自我指導(dǎo)框架（self-instruct framework），在這個框架下，我們教會模型合成生成越來越多的數(shù)據(jù)，以便我們能夠獲得更好的、更多的數(shù)據(jù)用于監(jiān)督式微調(diào)。

這種范式在 2023 年得到了廣泛的關(guān)注，我們看到在工業(yè)界和學(xué)術(shù)界都有很多工作基于自我指導(dǎo)框架展開，并設(shè)計了像 Alpaca、Vicuna 等模型。這些模型都大量使用了合成生成的指令數(shù)據(jù)進(jìn)行訓(xùn)練。

下一步就是在監(jiān)督式微調(diào)中進(jìn)行偏好微調(diào)。這里有一個非常重要的步驟，就是數(shù)據(jù)整理。這和我剛才提到的合成數(shù)據(jù)生成是一樣的，但同時也是一個很好的數(shù)據(jù)混合設(shè)置，因為當(dāng)我們關(guān)注一組任務(wù)和我們試圖優(yōu)化的目標(biāo)技能時，當(dāng)我們增加一組任務(wù)的提示和完成內(nèi)容時，我們可能會在其他組上失去準(zhǔn)確性和改進(jìn)。

比如，如果你在監(jiān)督式微調(diào)中添加了大量數(shù)學(xué)提示和數(shù)學(xué)類型的數(shù)據(jù)，你可能會在知識回憶方面表現(xiàn)下降，因為你總是希望生成越來越長的思考鏈。所以，數(shù)據(jù)混合是構(gòu)建一個好的微調(diào)模型中非常重要的一步。

剛才我們一直在講數(shù)據(jù)，但現(xiàn)在我想聚焦于什么樣的數(shù)據(jù)才真正有助于推理。這里所說的“推理”，舉個例子，比如一個數(shù)學(xué)問題：一家商店正在進(jìn)行襯衫促銷，每件襯衫售價 25 美元，現(xiàn)在我們想買 7 件襯衫，總共要花多少錢？我們可以很容易地標(biāo)注出答案是 125 美元，但僅僅用這種問題和金額答案作為監(jiān)督式微調(diào)數(shù)據(jù)是不夠的。

大家已經(jīng)認(rèn)識到，真正重要的是處理這種逐步推理的輸出，它能一步步告訴我們發(fā)生了什么。這種數(shù)據(jù)可以成為監(jiān)督式微調(diào)的優(yōu)質(zhì)來源。

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

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

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

我們的方法是做混合數(shù)據(jù)策劃，即：查看現(xiàn)有的資源，然后將其與合成數(shù)據(jù)生成相結(jié)合。事實上，我們采用了這篇非常有趣的論文中介紹的方法，用于合成地生成數(shù)據(jù)，但針對不同的用戶角色。這為什么重要呢？因為它增加了生成提示的多樣性。而且，它還使我們能夠不斷擴(kuò)大這種思維鏈條以及這種很難收集的推理數(shù)據(jù)的規(guī)模。

論文鏈接：https://arxiv.org/abs/2406.20094

這是如何運作的呢？我們會給模型設(shè)定不同的用戶角色，比如“這是一個化學(xué)動力學(xué)研究人員”，然后讓模型以這個角色生成數(shù)據(jù)和數(shù)學(xué)問題。接下來，我們再給它設(shè)定一個不同的角色，讓它生成一個邏輯推理問題，就可以得到這樣的結(jié)果。

我們給模型提供了許多不同類型的用戶角色。事實上，我們使用了25萬種角色，包括計算機科學(xué)家、化學(xué)教授、五歲小孩等等。然后，我們讓模型根據(jù)這些角色生成數(shù)學(xué)問題。通過這種方式，我們收集了 15 萬道硬件數(shù)學(xué)題和 5 萬道小學(xué)數(shù)學(xué)題。

我們還讓模型生成編程問題，這主要是 Python 代碼生成以及精確指令的遵循，貫穿于這些角色之中。在收集完這些提示后，我們使用了像 GPT-4o 或 Claude 這樣的大模型來為我們生成思維鏈條數(shù)據(jù)。然后，它們生成了逐步的解決方案。

我們來看一下這是否有所幫助。我們已經(jīng)在這些設(shè)置下進(jìn)行了評估，查看了一個公開的數(shù)據(jù)集，例如在數(shù)學(xué)領(lǐng)域，有一些由社區(qū)驅(qū)動的公開開源數(shù)據(jù)集，這些數(shù)據(jù)集是由其他團(tuán)隊、朋友和學(xué)術(shù)界生成或策劃的。然后，我們開始引入一些我們基于角色生成的合成數(shù)學(xué)問題。

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

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

在生成合成數(shù)據(jù)時，一個重要的問題就是結(jié)果的質(zhì)量。你可能會說：“好吧，你們生成了這些數(shù)學(xué)數(shù)據(jù)，然后讓GPT-4為這些生成內(nèi)容做標(biāo)注，那么這些標(biāo)注的質(zhì)量高不高呢？”

為了提高數(shù)據(jù)的質(zhì)量，我們做了以下工作：我們讓 GPT-4 生成多個實例或者多條思維鏈條，然后進(jìn)行了多數(shù)投票，并保留了那些大多數(shù)情況下答案正確的實例。

通過這種方式，我們刪除了很多數(shù)據(jù)。我們基本上只保留了 60% 的數(shù)據(jù)。好消息是，即使只使用了 60% 的數(shù)據(jù)，我們在數(shù)學(xué)領(lǐng)域的準(zhǔn)確率仍然相似，GSM8K 上甚至略有提升。

在整個通用方案中，我們不僅僅局限于數(shù)學(xué)，而是涉及許多不同類型的數(shù)據(jù)。

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

這是監(jiān)督式微調(diào)階段的結(jié)果?，F(xiàn)在我們進(jìn)入下一個階段：偏好微調(diào)。

那么，偏好微調(diào)的作用是什么呢？它的想法是，我們將比較同一個提示的不同完成結(jié)果，并選擇我們認(rèn)為更強的那個。通常，這在風(fēng)格和聊天評估中非常有用。比如它會告訴我們：“這個結(jié)果可能更符合人類的偏好?！钡覀円舶l(fā)現(xiàn)，它甚至在推理測試中也有所提升。

我們將使用基于強化學(xué)習(xí)的方法來根據(jù)這種反饋、這種偏好數(shù)據(jù)進(jìn)行優(yōu)化。在優(yōu)化步驟中，我們將優(yōu)化一個獎勵，這個獎勵是受到人類偏好的啟發(fā)。同時，我們希望確保不會偏離原始語言模型太遠(yuǎn)。因此，我們加入了一個 KL 散度懲罰項。

我們?nèi)绾芜M(jìn)行優(yōu)化？有哪些不同的算法可以用于優(yōu)化這種形式化問題？通常，人們會使用 PPO（近端策略優(yōu)化）。然后，去年還引入了一種更簡單的算法，稱為直接近端偏好優(yōu)化（Direct Proximal Preference Optimization）。而我們的問題是：這兩種算法中，哪一種更好？

在直接近端偏好優(yōu)化（DPO）中，它就像是一種非常簡單的基于學(xué)習(xí)的算法，與機器學(xué)習(xí)中的排序算法非常相似。而在近端策略優(yōu)化（PPO）中，它是一種真正的強化學(xué)習(xí)方法，你有一個獎勵模型，然后我們希望對策略模型進(jìn)行優(yōu)化。

在最近的研究中，我們決定從理論和實證的角度更深入地研究這個問題，以了解這些算法中哪一個更好。我們發(fā)現(xiàn)PPO（近端策略優(yōu)化）始終優(yōu)于DPO（直接近端偏好優(yōu)化）。然而，PPO 的實現(xiàn)要復(fù)雜得多。它需要大量內(nèi)存，因為我們希望同時將獎勵模型和策略模型保留在內(nèi)存中進(jìn)行優(yōu)化。而當(dāng)我們處理更大的模型時，這會變得更加困難，吞吐量也會顯著降低。

論文鏈接：https://arxiv.org/abs/2406.09279

這些是關(guān)鍵的發(fā)現(xiàn)。我們在比較這兩種算法時注意到，有很多不同的變量在起作用。因此，我們開始分別對它們進(jìn)行消融研究。比如說，這是我的初始監(jiān)督微調(diào)結(jié)果，這些是我的平均性能，以及它們在一組任務(wù)——大量任務(wù)中的變化情況。

我們首先想研究數(shù)據(jù)的作用。我們最初加入了較弱的偏好數(shù)據(jù)，效果并不太強，所以只有一點點提升。當(dāng)我們提高了偏好數(shù)據(jù)的質(zhì)量時，我們看到了一個很大的跳躍。我們使用完全相同的數(shù)據(jù)，只是替換了算法，結(jié)果 PPO 帶來了更好的提升。

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

現(xiàn)在讓我更具體地談?wù)勌囟ǖ耐评頊y試，在一些數(shù)學(xué)推理測試上看到了幾乎完全相同的趨勢。但有趣的部分是，當(dāng)我們將其與PPO結(jié)合時，我們實際上看到了一個更大的提升，尤其是在引入更大的獎勵模型時。這非常有趣。當(dāng)我們開始引入更具體的數(shù)學(xué)提示時，我們在這里看到了一個很大的跳躍。

因此，我們意識到，當(dāng)我們專注于推理的提示時，情況就是這樣。這也是我們在偏好微調(diào)階段看到改進(jìn)的方式。比如我們希望整合更多特定領(lǐng)域的數(shù)學(xué)問題。

我們把所有的發(fā)現(xiàn)匯總起來，然后設(shè)計了我們 2.3 模型中的偏好微調(diào)階段：

首先，我們非常謹(jǐn)慎地選擇提示詞。我們使用了在監(jiān)督微調(diào)階段已經(jīng)引入模型的一部分提示詞。我們引入了新的提示，專注于像推理領(lǐng)域這樣的特定領(lǐng)域，我們希望在這些領(lǐng)域看到更大的改進(jìn)。同時，我們也引入了一些領(lǐng)域外的提示，并且發(fā)現(xiàn)這實際上也非常有幫助。

我們收集這些提示詞，并從一個非常大的模型集合中查看偏好響應(yīng)，比如從 70 億參數(shù)的模型到像 GPT-4o 這樣非常強大的模型。我們開始比較它們之間的偏好，看看哪一個更好，這樣你的模型就會逐漸得到改進(jìn)。我們還確保包含未請求的數(shù)據(jù)，確保將 Tulu 38B 和 70B 數(shù)據(jù)納入其中，因為這是符合策略的。

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

研究發(fā)現(xiàn)，我們在使用所有模型時看到了很大的提升。我們展示出，與之前的偏好數(shù)據(jù)混合集相比，我們看到了一個巨大的進(jìn)步。同樣，我們進(jìn)行了大量的數(shù)據(jù)混合分析，研究應(yīng)該從監(jiān)督微調(diào)（SFT）中引入多少初始提示，以及應(yīng)該引入多少新的提示。這經(jīng)過了大量的實驗，以確定最佳的混合比例。

我想在這里強調(diào)一點，對于 2.3 版本，我們決定在這個階段再次使用 DPO（直接近端偏好優(yōu)化），因為我們還想訓(xùn)練更大的模型，我們認(rèn)為它的實驗速度更快，而且很有幫助。因此，我們對 DPO 做了很多改進(jìn)，比如我們讓它進(jìn)行了長度歸一化等。我們進(jìn)行了大量的超參數(shù)調(diào)整，最終發(fā)現(xiàn)，這真的效果很好，尤其是在這里使用 DPO。

但對于我們的 2.3 版本，我們實際上引入了一種新算法。我們將其稱為“可驗證獎勵的強化學(xué)習(xí)”。當(dāng)我們觀察偏好微調(diào)時，我們實際上是在訓(xùn)練一個獎勵模型，這是一個為模型的某種輸出分配分?jǐn)?shù)的神經(jīng)網(wǎng)絡(luò)。

我們的想法是，如果我們使用一個更簡單的設(shè)置，僅僅使用一個驗證機制，會怎么樣呢？也就是說，如果我們生成的內(nèi)容與標(biāo)準(zhǔn)答案等價，就返回 1，否則返回 0。所以它只是一個基于規(guī)則的、非常簡單的獎勵模型。

然后，我們訓(xùn)練這個非常簡單、非常基礎(chǔ)的強化學(xué)習(xí)框架，訓(xùn)練數(shù)據(jù)以提示的形式輸入。如果生成的結(jié)果非常好，我們就優(yōu)化并改進(jìn)我們的策略。

它對于這類推理任務(wù)非常有用，因為我們在一開始就已經(jīng)提到，為復(fù)雜的數(shù)學(xué)問題標(biāo)注思維鏈條是非常困難的。然而，在很多情況下，最終答案就足夠了。得出一個最終答案相對容易?；蛘呶覀兲幚淼氖且恍┥飳W(xué)相關(guān)任務(wù)。對于所有這些任務(wù)，我們只需要兩種標(biāo)注：原始提示和最終答案。然后我們就可以進(jìn)行驗證。

我們甚至可以將其用于精確指令的遵循，如果給出一個非常復(fù)雜的指令，讓模型生成一些內(nèi)容。然后，我想了解滿足的約束條件的百分比是多少，所以我們可以將這種驗證擴(kuò)展到不同的階段。

這并不是一個全新的想法。但變化在于，現(xiàn)在的基礎(chǔ)模型，或者是在監(jiān)督微調(diào)階段結(jié)束時的模型，已經(jīng)得到了很大的改進(jìn)。如今，我們能夠生成相對較好的思維鏈條，并將其與真實情況相對比，從而判斷它是否足夠好，是否不好，等等。

這就是我們的最終方案。我們使用最終答案或可驗證的約束來進(jìn)行驗證。我們并不是在訓(xùn)練中間的思維鏈條，而是讓模型自己生成思維鏈條。我們采用了經(jīng)典的強化學(xué)習(xí)實現(xiàn)，特別是這里我們使用了 PPO 算法，并且我們嘗試了三個數(shù)據(jù)集。

結(jié)果是好的。以下展示是與這些數(shù)據(jù)集的基準(zhǔn)對比，包括一些模型，比如DeepSeek V3、GPT-4o以及我們模型的不同版本，這些版本分別來自監(jiān)督微調(diào)（SFT）、直接近端偏好優(yōu)化（DPO）和可驗證獎勵的強化學(xué)習(xí)（RLV）。

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

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

我們最近做了一個很小的改動，就是把 PPO 換成了 GRPO。我們借鑒了 DeepSeel 的想法，嘗試將強化學(xué)習(xí)的實現(xiàn)從 PPO 遷移到 GRPO，并將其應(yīng)用于一個更好的基礎(chǔ)模型——QwenMath。我們在數(shù)學(xué)推理方面看到了顯著的提升。

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

最后，我在這里提到的所有內(nèi)容都與訓(xùn)練有關(guān)，即如何從基礎(chǔ)模型發(fā)展到能夠進(jìn)行推理的真實且良好的模型。我們在最近的一篇論文中，還沒有將其整合到 Tulu 配方中，但我們目前正在做這項工作，我們開始專注于數(shù)學(xué)類任務(wù)，即數(shù)學(xué)推理任務(wù)。

然后我們開始收集非常高質(zhì)量的推理數(shù)據(jù)和更復(fù)雜的數(shù)學(xué)問題。我們最初收集了 6 萬個樣本，然后進(jìn)行了大量的質(zhì)量篩選，最終得到了 1000 個多樣化的樣本。然后我們生成了這種深度思考的推理鏈條，通過從 Gemini 思考模型中提煉出深度思考的標(biāo)記。不久前，我們將其替換為DeepSeek R1推理模型。到目前為止，我們只進(jìn)行了簡單的監(jiān)督微調(diào)（SFT），結(jié)果非常好。

然后我們采用了一種非常簡單但令人驚訝的推理時擴(kuò)展方法，得到了一個非常有趣的結(jié)果。我們允許模型在生成結(jié)果時有一定數(shù)量的標(biāo)記預(yù)算，然后我們將這個標(biāo)記預(yù)算從 512 調(diào)整到 2048，或者對于 GPQA 來說，調(diào)整到 496 等等。

如果模型沒有用完它的標(biāo)記預(yù)算，我們就添加一種延續(xù)標(biāo)記，后讓模型再思考一會兒。通過這種方式，我們發(fā)現(xiàn)模型現(xiàn)在能夠生成更好、更深入的推理路徑，這非常有趣。還有一個更有趣的事實：當(dāng)我們沒有添加任何標(biāo)記，只是簡單地讓模型生成更多內(nèi)容時，我們并沒有看到這種效果。

二、領(lǐng)悟的 Transformer 是隱式推理器

俄亥俄州立大學(xué)的 Huan Sun 教授做了主題為“Understanding Reasoning in LLMs and Agents:From Grokking of lmplicit Reasoning to Test-Time Scaling with Verifiers”的演講，探討了從隱式推理的領(lǐng)悟到測試時通過驗證器進(jìn)行的擴(kuò)展。

首先來談?wù)勈裁词请[式推理。

論文鏈接：https://arxiv.org/abs/2405.15071

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

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

首先，大規(guī)模訓(xùn)練或預(yù)訓(xùn)練的默認(rèn)模式大多數(shù)情況下是不需要 CoT 的，所有數(shù)據(jù)都是可用的。實際上，為訓(xùn)練提供推理器可能會非常昂貴。而且，從根本上來說，我認(rèn)為這決定了語言模型從數(shù)據(jù)中學(xué)習(xí)事實和規(guī)則結(jié)構(gòu)的能力。如果一個模型能夠在內(nèi)部進(jìn)行思考，那么它在壓縮和整合信息方面可能會更強大。

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

Transformer 是否能夠?qū)W會隱式推理呢？又或者，是否存在一些根本性的限制，阻礙了模型獲得這種能力？

哪些因素會影響這種能力的獲??？是數(shù)據(jù)、技能、分布，還是模型架構(gòu)？

這個數(shù)據(jù)集非常有趣。我們使用合成數(shù)據(jù)設(shè)置來控制研究，以便得出嚴(yán)謹(jǐn)?shù)慕Y(jié)論。

在我們的數(shù)據(jù)集中有兩種事實：一種被稱為原子事實（atomic facts），另一種被稱為推斷事實（infer factor）。

原子事實就像是知識圖譜中的每個邊，是單一關(guān)系，單一關(guān)系不能再進(jìn)一步拆分，這就是原子事實。

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

模型的目標(biāo)是能夠歸納并應(yīng)用潛在的規(guī)則。為了使模型能夠歸納出潛在規(guī)則，我們在訓(xùn)練過程中提供了一種混合的原子效應(yīng)和推斷事實。我們希望模型在訓(xùn)練中能夠?qū)W會這些潛在規(guī)則，比如如何應(yīng)用這些原子效應(yīng)來推導(dǎo)出多跳事實。

例如，現(xiàn)在給定一個新的查詢，比如關(guān)于哈勃望遠(yuǎn)鏡的查詢，我們希望模型在測試時能夠應(yīng)用這些歸納出的規(guī)則，并正確回答這個新的多跳查詢。

但更有趣的是，我們有 ID 和 OOD 兩種設(shè)置，基本上涵蓋了分布內(nèi)和分布外的所有情況。這意味著我們將所有的原子效應(yīng)分成兩組：一組用于 ID 設(shè)置，另一組用于 OOD 設(shè)置。

對于用于 ID 設(shè)置的原子效應(yīng)，我們會將這個集合中的所有原子事實進(jìn)行組合，并將推斷出的事實劃分為訓(xùn)練集和測試集。在這個測試設(shè)置中，我們稱之為 ID 測試集。對于另一組原子效應(yīng)，我們會對這個集合中的原子事實進(jìn)行組合，而這些推斷出的事實將被用作測試。

所以，你可以這樣理解：如果一個多跳查詢，比如（h，r1）、（h，r2）屬于 ID 設(shè)置，這意味著它們涉及的原子事實已經(jīng)在訓(xùn)練中與其他原子效應(yīng)組合過。但如果這個多跳查詢屬于 OOD 設(shè)置，那么這些原子效應(yīng)雖然在訓(xùn)練中出現(xiàn)過，但它們與其他任何因素的組合在訓(xùn)練中都沒有出現(xiàn)過。

我們在訓(xùn)練集上訓(xùn)練這個模型，并測試其在 ID 的表現(xiàn)。現(xiàn)在，我們先來看一下這兩個任務(wù)的學(xué)習(xí)曲線，可以觀察到，模型能夠達(dá)到完美的分布內(nèi)泛化性能，但是，這需要在過擬合之后進(jìn)行更長時間的訓(xùn)練。

對于這兩個任務(wù)，正如你所看到的，過擬合大致發(fā)生在這里，這意味著模型在這一點上傾向于完美地擬合訓(xùn)練性能，但它需要經(jīng)過更多步驟的優(yōu)化，才能使分布內(nèi)泛化性能趕上并達(dá)到完美的表現(xiàn)。這種延長的訓(xùn)練周期就是我們所說的“阻塞期”。

第二個發(fā)現(xiàn)是，我們來看一下藍(lán)色曲線?？梢杂^察到，在組合性任務(wù)中，Transformer 并沒有實現(xiàn)完全的泛化。所以，分布內(nèi)泛化性能從未提升，但相比之下，它最終趕上并達(dá)到了完美的表現(xiàn)。

我們還發(fā)現(xiàn)，泛化速度與絕對數(shù)據(jù)量并沒有關(guān)系，而是與關(guān)鍵數(shù)據(jù)分布、特別是推斷事實與原子事實的比例密切相關(guān)。也就是說，比例越高，泛化速度就越快。

這似乎與之前的研究結(jié)果相矛盾，他們認(rèn)為存在一個臨界數(shù)據(jù)量的概念，即所謂的“突破現(xiàn)象”。但我們認(rèn)為實際上起決定作用的是推斷事實與原子事實之間的比例。

然而，仍有一些更重要的問題有待進(jìn)一步探討。例如，泛化過程中發(fā)生了什么？為什么會出現(xiàn)泛化？為什么不同任務(wù)之間的泛化水平會有所不同？

這就需要我們進(jìn)行更多的分析，以剖析在泛化過程中模型內(nèi)部的工作機制。在這部分，我們使用了來自機制可解釋性文獻(xiàn)中的一些標(biāo)準(zhǔn)技術(shù)，稱為 Logit lens。

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

具體操作如下：在正常的運行過程中，我們輸入一個常規(guī)的查詢，然后生成最終的預(yù)測結(jié)果。這個過程是在模型已經(jīng)過擬合之后進(jìn)行的，因此模型總是能夠預(yù)測出目標(biāo)。關(guān)鍵在于，我們還會進(jìn)行一種干擾實驗，即用隨機采樣的 r1' 替換 r1，然后通過網(wǎng)絡(luò)獲取 r1' 的隱藏表示，并用它替換正常運行中 r1 的隱藏表示，觀察這一變化如何影響最終的預(yù)測結(jié)果。我們會多次重復(fù)這個過程，通過采樣許多不同的隨機實體，觀察最終預(yù)測結(jié)果的改變頻率。

在那之后，你可以將整個神經(jīng)網(wǎng)絡(luò)視為一個從輸入到輸出傳播信息的計算圖?；谶B接的強度，我們可以在那些連接非常弱的邊上進(jìn)行剪枝。在經(jīng)過阻塞或者在阻塞的最后階段，我們在模型檢查點（checkpoint）上進(jìn)行機制分析。我們發(fā)現(xiàn)了我們所說的“泛化電路”，用于這兩個任務(wù)。讓我?guī)憧纯催@個，這對我們來說非常有趣。

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

我們還通過 Logit lens 檢查每個隱藏狀態(tài)代表的輸入 token。我們發(fā)現(xiàn)，這個隱藏表示實際上代表標(biāo)記 B，它是橋接實體（bridge entity），也是 r1 的目標(biāo)，并且這個隱藏表示還代表關(guān)系 r2?；旧希瑑蓚€關(guān)系確實被保留了，上層確實正在執(zhí)行第二階段的知識檢索。

我們想要深入了解在 grokking（領(lǐng)悟）過程中發(fā)生了什么。因此，我們在 grokking 期間對許多檢查點進(jìn)行了類似的分析，并跟蹤隱藏狀態(tài)與目標(biāo)預(yù)測之間的因果聯(lián)系。這些特征實際上展示了隱藏狀態(tài)與最終預(yù)測之間的因果關(guān)系。兩者之間的差異被稱為在阻塞期間的變化。

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

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

基于這些證據(jù)，我們認(rèn)為這表明模型在阻塞期間逐漸形成了操作。在 grokking 之前，模型很可能只是在進(jìn)行記憶化操作，即將查詢直接與目標(biāo)關(guān)聯(lián)。

那么，為什么會出現(xiàn)“grokking”現(xiàn)象？我們認(rèn)為，在我們的模型訓(xùn)練初期，會形成一個記憶化電路，它直接將輸入與目標(biāo)預(yù)測關(guān)聯(lián)起來，而無需經(jīng)過中間步驟。然而，在訓(xùn)練的后期，隨著模型逐漸泛化，會形成一個泛化路線，這個泛化路線是從記憶化路線中分化出來的。

那么，為什么會出現(xiàn)這種分化呢？或者，為什么記憶化路線會在訓(xùn)練后期被泛化路線取代？

這是因為在優(yōu)化過程中，模型被激勵去變得更高效。從記憶化到泛化的轉(zhuǎn)變，我們可以從效率的角度來理解：記憶化路線需要存儲大量的事實，而泛化路線需要支持的事實數(shù)量要少得多。

此外，我們還可以從優(yōu)化過程中的權(quán)重調(diào)整來理解這一點。在 grokking 階段，當(dāng)模型達(dá)到完美的訓(xùn)練性能后，模型開始優(yōu)化權(quán)重，其中權(quán)重項會顯著減小。這表明模型試圖找到一種更簡潔的方式來保持相同的訓(xùn)練精度。

那么，為什么這兩個任務(wù)并沒有總是實現(xiàn) OOD 泛化呢？更根本的原因是，Transformer 架構(gòu)的非遞歸設(shè)計阻礙了跨層的記憶共享，從而限制了模型在 OOD 任務(wù)中的泛化能力。

我們還嘗試了一個小規(guī)模的實驗環(huán)境：我們在模型的不同部分共享參數(shù)，比如前四層和后四層使用相同的參數(shù)，然后我們重新進(jìn)行訓(xùn)練，結(jié)果發(fā)現(xiàn)泛化性能有了顯著提升。但我們沒有等到它完全收斂，就像一個生成器達(dá)到完美性能那樣。我們認(rèn)為這種參數(shù)共享的方式能夠解鎖更好的泛化性能，但這只是潛在的一種方法，還有其他方式可以改進(jìn)架構(gòu)。

三、統(tǒng)一符號結(jié)構(gòu)與神經(jīng)網(wǎng)絡(luò)表示

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

今天，我們?nèi)匀荒芸吹酱笳Z言模型（LLM）存在一系列問題，關(guān)于這一問題有幾種不同的方法可以解決：

首先，當(dāng)然你可以將越來越多的數(shù)據(jù)輸入到模型中，希望能夠通過數(shù)據(jù)量的增加來幫助模型更好地學(xué)習(xí)；

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

最后，我會簡要介紹我們最近的一些理論研究，這些研究試圖將符號結(jié)構(gòu)與神經(jīng)網(wǎng)絡(luò)表示統(tǒng)一起來。實際上，通過使用梯度上升（gradient ascent）對神經(jīng)網(wǎng)絡(luò)進(jìn)行訓(xùn)練，我們可以發(fā)現(xiàn)符號結(jié)構(gòu)逐漸出現(xiàn)。通過這種方式，我們實際上看到了符號表示和神經(jīng)表示在同一框架內(nèi)的統(tǒng)一。但目前這還處于非常初級的階段，希望未來它能成為主流，但我們還不確定。

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

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

對于工具的使用，我們實際上可以調(diào)用外部工具來解決推理問題。以旅行規(guī)劃問題為例，我們并不是讓用戶直接向模型提問，而是讓模型首先將用戶的需求轉(zhuǎn)化為符號形式。這個符號形式能夠準(zhǔn)確地描述用戶的需求。然后，結(jié)合來自外部的航班和酒店信息，將這些信息整合成一個大型的優(yōu)化問題，并通過混合整數(shù)線性規(guī)劃（一種組合求解器）來解決。

這個求解器會給出最優(yōu)行程的符號表示，然后你可以通過現(xiàn)有的大模型將其翻譯回自然語言，從而得到由 Agents提供的答案。通過這種方式，你可以得到一個有保證的解決方案。同時，這個過程并不慢。如果你走完整個流程，它實際上是非?？斓摹?/p>

我們基于這個思路構(gòu)建了一個演示，在兩到三秒內(nèi)，就能得到一個保證正確的解決方案。當(dāng)然，這是在用戶請求被準(zhǔn)確翻譯的前提下，大模型的翻譯是相當(dāng)準(zhǔn)確的。你可以看到有一個兩秒的延遲，但整個演示仍然可以很好地運行。此外，我們還讓人類標(biāo)注員進(jìn)行了測試，他們對結(jié)果非常滿意。

當(dāng)然，如果你考慮到旅行規(guī)劃，我們也會希望讓 Agents提出澄清性的問題，也就是說，我們希望 Agents 能夠真正思考用戶請求中缺少的細(xì)節(jié)，并且判斷 Agents 是否可以提出越來越多的問題來澄清這些細(xì)節(jié)，以確保他們理解用戶的需求。

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

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

我們基本上以一種有指導(dǎo)的方式進(jìn)行了這種直觀的 DPO（可能是某種優(yōu)化方法）和項目采樣，并且我們已經(jīng)展示了，通過這種方式訓(xùn)練的 AB 模型在多輪對話的多個方面，相比沒有經(jīng)過這種訓(xùn)練的原始 700 億參數(shù)模型要好得多。

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

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

當(dāng)我們思考導(dǎo)航問題時，我們有一個起點和一個終點，然后我們要求模型找出從起點到終點的最短路徑。在任何階段，我們既可以要求人工，標(biāo)注也可以要求符號求解器對問題進(jìn)行建模，并通過符號搜索來解決問題。A*算法（啟發(fā)式搜索算法）會打開一個優(yōu)先級表，這個表基本上會找到搜索中需要探索的下一個正確狀態(tài)。

然后，按照探索的方式，我們最終會找到通往目的地的路徑，并且它會保證給你一個最優(yōu)的軌跡。因此，按照A*算法的搜索過程，我們可以構(gòu)建如下所示的思維鏈。我們從一個提示開始，這個提示是問題規(guī)范的表示。

然后，我們可以通過像轉(zhuǎn)儲整個A搜索過程一樣來構(gòu)建一個軌跡。每次A搜索器在搜索空間中創(chuàng)建一個新節(jié)點時，我們實際上就在軌跡中插入一個創(chuàng)建操作；每次A*搜索器關(guān)閉一個節(jié)點時，我們在軌跡中插入一個關(guān)閉操作。因此，我們基本上會得到一個很長的軌跡，然后一旦開始找到目標(biāo)，我們就會插入一個計劃，這個計劃輸出最終的最優(yōu)軌跡。

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

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

我們發(fā)現(xiàn)，使用這種帶有軌跡增強的搜索增強模型時，情況會有所不同。我們看到，如果你只使用僅輸出解決方案的模型，那么你需要 100 萬樣本才能達(dá)到接近 100% 的準(zhǔn)確率。但如果你使用搜索增強模型，你實際上只需要十分之一的數(shù)據(jù)量，同時，你也只需要十分之一的參數(shù)量，就能達(dá)到類似的性能。所以，搜索增強模型不僅更簡單高效，而且在參數(shù)使用上也更加高效。

這種情況也適用于其他類型的規(guī)劃任務(wù)，比如讓 Agents 將箱子推到目的地，這需要非常謹(jǐn)慎的規(guī)劃。因為如果箱子被推到角落，就沒有回頭路了。

一旦我們有了這些操作模型——這些模型基本上是通過模仿學(xué)習(xí)實現(xiàn)的——我們可以通過在這些搜索增強模型的基礎(chǔ)上進(jìn)行微調(diào)來做得更好。具體來說，我們可以通過微調(diào)這些原始模型，使其生成更短的軌跡，但仍然保持最優(yōu)的計劃。這其實是一個非常典型的強化學(xué)習(xí)任務(wù)，因為目標(biāo)是明確的，但我們不知道如何實現(xiàn)這個目標(biāo)。所以，我們讓強化學(xué)習(xí) Agents 去探索并找到解決方案。

通過“Searchformer”，我們發(fā)現(xiàn)最終得到的模型比原始的 A* 搜索模型更好，因為它具有更短的搜索軌跡。這是由于采用了“直觀地址采樣”（Intuitive Address Sampling），這是一種簡化的強化學(xué)習(xí)版本。

從數(shù)據(jù)上看，我們發(fā)現(xiàn)減少后的軌跡與原始A*軌跡之間的比例越來越高，這意味著從數(shù)值上來看，這種情況確實存在。

不僅如此，我們還發(fā)現(xiàn)，不僅軌跡變得更短，而且經(jīng)過微調(diào)后的性能也在不斷提高。每次迭代后，解決方案達(dá)到最優(yōu)的比例越來越高。在這種情況下，你已經(jīng)可以看到，擁有 45M 個參數(shù)的模型——這里的參數(shù)指的是模型的參數(shù)數(shù)量——實際上可以與用 700M 個參數(shù)訓(xùn)練的模型相媲美，而后者是用一個更大的數(shù)據(jù)集進(jìn)行訓(xùn)練的。

這非常有趣，我相信這是最早展示在測試時間和訓(xùn)練推理數(shù)據(jù)上存在某種“皮膚法則”（可能是指某種優(yōu)化或提升性能的規(guī)律）的少數(shù)論文之一，這種法則有可能提高閱讀任務(wù)的性能。

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

論文鏈接：https://arxiv.org/abs/2410.09918

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

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

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

經(jīng)過訓(xùn)練，我們發(fā)現(xiàn)這種模式比單獨的快速模式更好，也比單獨的慢速模式更好。這是一個非常有趣的發(fā)現(xiàn)。

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

我認(rèn)為這可能是因為他們用來訓(xùn)練模型的數(shù)據(jù)具有這種特定的結(jié)構(gòu)，而模型在學(xué)習(xí)過程中會捕捉到這些結(jié)構(gòu)，從而作為一種副作用來控制模型的行為。我們很高興看到這種行為也出現(xiàn)在最先進(jìn)的大型模型中。

我們也將雙模式模型應(yīng)用于數(shù)學(xué)問題，基線模型會有一個非常長的思維鏈。但一旦你隨機丟棄一些句子，并用這些數(shù)據(jù)進(jìn)行微調(diào)，會非常驚訝地發(fā)現(xiàn)，序列的長度會基本保持不變，同步標(biāo)記會變得非常短，而且短得多。同時，生成的內(nèi)容仍然是合理的，并且能給出正確的答案。

這種行為挺有意思的。我們是在基礎(chǔ)模型上進(jìn)行這種大規(guī)模微調(diào)。這些是基礎(chǔ)模型，它們并不是針對特定任務(wù)優(yōu)化的，所以性能并不算出色。但即便如此，你仍然會看到性能有所提升。

四、基于 API 的網(wǎng)絡(luò)智能體

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

論文鏈接：https://openreview.net/forum?id=TPiJKs7ccR

我們實現(xiàn)了一個基礎(chǔ)的瀏覽 Agent。它基于無障礙功能樹運行，能夠在簡單布局的網(wǎng)頁上合理地導(dǎo)航并填寫表單。這就是我們的基線模型，也是我們在“Agents工作流記憶”論文中所使用的基線模型。

但挑戰(zhàn)在于無障礙功能樹結(jié)構(gòu)的復(fù)雜性，許多語言模型對此并不熟悉。當(dāng)內(nèi)容并非立即可見時，導(dǎo)航也會變得棘手，因為你需要滾動頁面、切換頁面，以及其他類似的操作。

一個失敗的例子是詢問：“Saptaks 對 Allyproject 做了多少次提交？”于是， Agents嘗試進(jìn)行瀏覽，它試圖訪問 GitLab.com，使用憑據(jù)登錄，點擊項目，點擊提交記錄，然后不斷向下滾動、向下滾動……最終，它耗盡了時間，并得出結(jié)論說沒有找到任何提交記錄，因此它認(rèn)為沒有提交發(fā)生，提交次數(shù)為零。

另一方面，我們還有另一種與環(huán)境交互的界面。這可以是像調(diào)用API這樣的方式。它為機器與網(wǎng)絡(luò)服務(wù)之間的通信提供了一個直接的接口，減少了操作復(fù)雜性，并且理想情況下，我們會得到更好的結(jié)果。

如果我們看看 API，它們是預(yù)定義的端點，允許計算機高效地執(zhí)行任務(wù)，并通過 GET、POST、PUT 等請求實現(xiàn)交互，返回結(jié)構(gòu)化數(shù)據(jù)，比如 JSON。有趣的是，我們在標(biāo)準(zhǔn)基準(zhǔn)測試（比如 Web）中使用的許多網(wǎng)站已經(jīng)提供了 API，所以在許多情況下，這些 API 已經(jīng)存在。如果我們能夠恰當(dāng)?shù)厥褂盟鼈儯覀兙涂梢酝ㄟ^ API 與這些網(wǎng)站進(jìn)行交互。

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

這是一個例子，在一個 API 文檔中，它會告訴你屬性的類型、屬性的描述，以及 API 的輸出會是什么，以及你可以如何執(zhí)行調(diào)用。API調(diào)用本質(zhì)上是通過調(diào)用代碼實現(xiàn)的。你可以使用requests.get這樣的請求，而這就是一個響應(yīng)的例子。

我們考察的是，如果我們把傳統(tǒng)上由瀏覽 Agent 解決的任務(wù)，讓 AI Agents 通過 API 來完成，會怎么樣呢？

這是我們基于 API 的 Agents。我們的實現(xiàn)方式是使用我們 Agents 框架中的標(biāo)準(zhǔn)編碼 Agents（OpenHands），并以我接下來會講的方式，為它提供對 API 的訪問。

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

那么，問題來了，你知道的鑒于 API 調(diào)用的好處，我們應(yīng)該完全拋棄網(wǎng)頁瀏覽嗎？當(dāng)然，答案是否定的。如果我們查看一百個隨機抽樣的任務(wù)的錯誤分布，當(dāng)我們將 API 提供給模型時，會發(fā)現(xiàn)其中大約三分之一的任務(wù)實際上是正確的，但 WebArena 的驗證器卻判定它們是錯誤的，而另外 50% 的任務(wù)根本無法通過 API 解決。

原因在于，并非所有網(wǎng)站都提供全面的 API 支持。它們并非都有完善的 API 文檔，而且網(wǎng)站的深度復(fù)雜性也是一個問題。

因此，我們提出的一個解決方案是創(chuàng)建一個混合 Agent。這種 Agent 能夠交替執(zhí)行瀏覽和 API 調(diào)用操作，并且在每一步中，它會選擇與人類溝通、生成自然語言、執(zhí)行 Python 代碼（包括API調(diào)用）以及執(zhí)行網(wǎng)頁瀏覽操作。

我們根據(jù)當(dāng)前可用的 API 的質(zhì)量來選擇操作：

我們提示 Agent，如果存在足夠的 API，就應(yīng)該嘗試使用 API。但如果足夠的 API 不存在，它就可以回到瀏覽模式。在其執(zhí)行軌跡的最后，當(dāng)它完成了所有需要做的事情后，我們要求 Agent 訪問一個能夠為用戶提供答案的網(wǎng)頁。這樣做的想法是，它可能會使用 API 調(diào)用，但最終會將結(jié)果展示在網(wǎng)頁上。這也符合 WebArena 評估的要求，即需要訪問特定的 URL。

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

如果你查看 Agent 的性能，我們在多個網(wǎng)站類別上對其進(jìn)行了評估，發(fā)現(xiàn)在某些特定類別上轉(zhuǎn)向使用 API 后，性能有了顯著提升。例如，在 GitLab 和地圖上，轉(zhuǎn)向使用 API 后性能大幅提升；而在 Reddit 和管理類網(wǎng)站上，轉(zhuǎn)向使用 API 后性能提升較小，但當(dāng)我們切換到使用混合 Agent 時，性能有了更大的提升。

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

我們所做的就是查看了所有的 API，并且編寫了一些新的 API。雖然數(shù)量并不多，但我們手動編寫了幾個，這使得在 Reddit 上使用 API 的 Agent 的準(zhǔn)確率翻了一番。所以，擁有高質(zhì)量的 API 對于網(wǎng)站來說是很重要的。

但就這項工作的未來方向而言，其中之一是獲取或生成合適的 API。那么，我們?nèi)绾文軌蜃詣由删W(wǎng)站的 API，以便我們能夠調(diào)用一個函數(shù)，而無需 Agent 事先具備該函數(shù)、以及改進(jìn)端點的檢索和利用？我們可能會有非常豐富的 API，如何從中篩選出我們需要的部分呢？

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

五、AI 新前沿：形式化數(shù)學(xué)推理

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

論文鏈接：https://arxiv.org/abs/2412.16075

AI 在形式化數(shù)學(xué)中有廣泛應(yīng)用。事實上，我們可以利用各種經(jīng)過形式化驗證的工具，比如定理證明器等。而且，實際上存在許多不同類型的定理證明系統(tǒng)。

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

在這一過程中，這一步是 AI 可以自動化的步驟之一。然后，生成的形式化證明和經(jīng)過驗證的定理可以被納入形式化數(shù)學(xué)庫。

此外，我們可以使用自動形式化（auto formalization）將非形式化的數(shù)學(xué)內(nèi)容轉(zhuǎn)換為形式化的數(shù)學(xué)陳述。

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

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

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

盡管整個社區(qū)已經(jīng)取得了非常顯著的進(jìn)展，但我現(xiàn)在想簡要介紹一下一些開放性挑戰(zhàn)和未來發(fā)展方向。

首先就是數(shù)據(jù)問題。

一般來說，在數(shù)學(xué)領(lǐng)域，尤其是形式化數(shù)學(xué)中，我們面臨數(shù)據(jù)稀缺的問題。例如，對于訓(xùn)練Code Llama，其訓(xùn)練數(shù)據(jù)集大約有 5000 億個 token，但當(dāng)我們看這些證明時，可用的證明數(shù)據(jù)量卻遠(yuǎn)遠(yuǎn)少于這個規(guī)模，甚至相差幾個數(shù)量級。因此，對于這些領(lǐng)域，開發(fā)各種方法來解決數(shù)據(jù)稀缺問題顯得尤為重要。

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

首先是通過自動形式化來創(chuàng)建數(shù)據(jù)。這種自動形式化本質(zhì)上是訓(xùn)練大型語言模型，使其能夠?qū)⒎切问交臄?shù)學(xué)內(nèi)容自動轉(zhuǎn)換為形式化的數(shù)學(xué)陳述。

鑒于我們有大量的非形式化數(shù)學(xué)內(nèi)容，比如教科書和其他各種材料，通過成功的自動形式化，我們可以自動地生成這些形式化的數(shù)學(xué)陳述。我們最近在利用反饋循環(huán)來改進(jìn)大型語言模型的自動形式化方面，已經(jīng)看到了令人興奮的進(jìn)展。

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

此外，AlphaGeometry 在 IMO 中的成功還歸功于它生成合成數(shù)據(jù)的另一種方式。它通過幾何規(guī)則生成了 1億個合成定理和證明，從而幫助它成功解決了 IMO 中具有挑戰(zhàn)性的幾何問題。這也為解決數(shù)據(jù)稀缺問題提供了一個很好的例子。

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

其核心思想是，可以開發(fā)模型來為定理和引理生成猜想，然后利用定理證明器嘗試自動證明這些猜想。如果成功生成了證明，那么這些經(jīng)過驗證的猜想就成為了定理和引理，并可以被添加到陳述和證明的庫中。

這可以幫助產(chǎn)生額外的數(shù)據(jù)，進(jìn)一步幫助訓(xùn)練模型，使其在生成更好的猜想和證明方面表現(xiàn)得更好。到目前為止，我們已經(jīng)在相對簡單的引理和定理上看到了這方面的進(jìn)展，因此未來我們可以在這方面努力，顯著提高能夠猜想和證明的定理的可擴(kuò)展性和難度水平。

在這一領(lǐng)域，我們需要解決許多不同的算法挑戰(zhàn)。例如，對于自動形式化，我們該如何擴(kuò)展自動形式化？我們?nèi)绾胃咝矣行У剡M(jìn)行證明搜索？我們?nèi)绾卫美碚摳倪M(jìn)中的層次結(jié)構(gòu)，以及如何真正學(xué)習(xí)數(shù)學(xué)抽象？此外，我們?nèi)绾卫矛F(xiàn)有的數(shù)學(xué)知識，以及如何調(diào)和專家型和通才型方法？

首先是，我們?nèi)绾握嬲龑崿F(xiàn)大規(guī)模的自動形式化？在進(jìn)行自動形式化時，實際上存在許多挑戰(zhàn)。

因為我們進(jìn)行自動形式化時，并沒有后續(xù)的驗證步驟，所以我們無法確切知道其他形式化的陳述是否真正正確。我們需要對它們進(jìn)行評估，并且需要開發(fā)良好的指標(biāo)來評估這些形式化的陳述。

此外，我們還需要能夠自動驗證這些自動形式化的陳述，理想情況下是利用改進(jìn)的形式化步驟等。因此，我們的期望是，對于復(fù)雜的自動形式化任務(wù)，我們實際上可以將其分解為更小的步驟，然后與形式化系統(tǒng)進(jìn)行交互以提供幫助。

對于評估自動形式化的陳述，有幾個原因使其相當(dāng)具有挑戰(zhàn)性。首先，我們不能依賴人工評估，因為這種方法無法擴(kuò)展。而對于其他形式化的陳述，通常存在不同的形式，即存在多種正確的方式來完成形式化，而自動等價性檢查本身其實并不簡單。

因此，為了應(yīng)對這一挑戰(zhàn)，我們需要利用像以太坊證明器這樣的正式驗證系統(tǒng)。我們希望借助定理證明器的反饋，迭代式地改進(jìn)自動形式化。

另一個挑戰(zhàn)是如何更高效、更有效地進(jìn)行證明搜索。這當(dāng)然是使用 AI 進(jìn)行形式化數(shù)學(xué)的一個關(guān)鍵目標(biāo)。對于理論改進(jìn)，有許多不同的方面和組成部分。我們可以做的是，從本質(zhì)上提升證明搜索的能力。

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

此外，我們還希望開發(fā)更好的價值模型，以幫助評估和優(yōu)先排序不同的證明目標(biāo)，以及證明搜索樹的不同部分。同時，我們希望系統(tǒng)地評估模型和搜索算法，并設(shè)置參數(shù)，以便能夠開發(fā)出更適合證明搜索的模型。

到目前為止，我們已經(jīng)看到，擴(kuò)大測試時的計算量對于提升模型的推理能力非常有效。比如在 AlphaGeometry 和 AlphaProof 等項目中，理論改進(jìn)是一個非常自然的方向。通過在證明搜索過程中增加計算量，我們可以幫助提升模型的證明搜索能力。

另一個重要話題是我們?nèi)绾我龑?dǎo)并更好地優(yōu)先排序研究。特別是，我們需要開發(fā)更好的價值模型，以幫助評估和優(yōu)先排序證明目標(biāo)。因此，一個關(guān)鍵的挑戰(zhàn)和未來方向是如何更好地訓(xùn)練價值模型，以及我們?nèi)绾潍@取更好的數(shù)據(jù)并利用獎勵模型（RM）來幫助解決這些問題。

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

另一個開放性挑戰(zhàn)和正式的研究方向是，我們希望更好地利用定理證明中的層次結(jié)構(gòu)。特別是在理論證明中，當(dāng)你面對一個復(fù)雜的定理時，通常即使是數(shù)學(xué)家手動證明時，也會將這些復(fù)雜定理分解為一些不同層次的高級證明目標(biāo)，以及一些不同的高級引理等。然后，這些復(fù)雜的定理會被進(jìn)一步分解為更小的目標(biāo)，依此類推。

這很重要——正如我們在形式化數(shù)學(xué)中應(yīng)用 AI 一樣，我們也需要開發(fā)具備這種能力的模型，能夠逐步將高級證明目標(biāo)分解為更小的目標(biāo)。

所以，我們并不是主張用形式化數(shù)學(xué)的 AI 來取代非形式化數(shù)學(xué)的 AI。事實上，非形式化數(shù)學(xué)的 AI 和形式化數(shù)學(xué)的 AI 之間存在著一種自然的協(xié)同作用。重要的是將兩者結(jié)合起來，本質(zhì)上是將非形式化推理的靈活性與形式化推理的嚴(yán)謹(jǐn)性結(jié)合起來。

例如，對于非形式化的陳述，我們可以嘗試對其進(jìn)行自動形式化，然后利用形式化驗證和改進(jìn)等手段來驗證其正確性。對于非形式化的定理陳述，以及用于非形式化數(shù)學(xué)的模型，它們可以幫助生成例如非形式化的證明草圖，這些證明草圖隨后可以被轉(zhuǎn)化為形式化的證明草圖，并最終生成經(jīng)過驗證的形式化證明。

通過這種方式，非形式化數(shù)學(xué)部分可以幫助提升生成形式化證明的可擴(kuò)展性、靈活性以及提供高層次的直覺，而形式化證明則可以為這些非形式化證明提供驗證。沒有這樣的形式化驗證，就無法真正推理并確保非形式化證明的正確性。

即使是數(shù)學(xué)論文和密碼學(xué)論文等領(lǐng)域的非形式化證明，有時也會出現(xiàn)錯誤。而對于 AI 生成的非形式化證明，出現(xiàn)錯誤和漏洞的可能性甚至更高。因此，將非形式化和形式化結(jié)合起來，最終生成經(jīng)過形式化驗證的證明，是非常重要的。

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

另一個對于數(shù)學(xué)的可擴(kuò)展性等來說也很重要的是學(xué)習(xí)數(shù)學(xué)抽象。

具體來說，無論是人類數(shù)學(xué)家還是數(shù)學(xué)系統(tǒng)，一般來說，這些抽象——比如開發(fā)新的定義和元素——實際上對于解決更復(fù)雜的數(shù)學(xué)問題至關(guān)重要。

我認(rèn)為，這尤其是一個令人興奮的領(lǐng)域和方向。對于形式化數(shù)學(xué)中的 AI 而言，這不僅是一個挑戰(zhàn)，也是對模型創(chuàng)造力的考驗，即模型如何學(xué)會構(gòu)建這些新的定義、引理和策略，并將其應(yīng)用于完整的證明輔助中，以便在未來證明中也能被利用。

最近在學(xué)習(xí)簡單的證明策略方面已經(jīng)取得了一些進(jìn)展，這些策略是通過引導(dǎo)式的方法從智能體自身解決數(shù)學(xué)問題的過程中得來的。我認(rèn)為這是一個非常有前景且令人興奮的領(lǐng)域，即我們?nèi)绾文軌虮举|(zhì)上訓(xùn)練模型以及證明智能體，從而使其能夠更好地從自身以往的經(jīng)驗中發(fā)現(xiàn)并學(xué)習(xí)抽象。

隨著我們持續(xù)推動這一正向循環(huán)，我們將繼續(xù)生成新的數(shù)據(jù)，并通過自動形式化等方式，不斷擴(kuò)大定義、數(shù)學(xué)陳述、定理等的庫。在證明搜索過程中，能夠利用庫中現(xiàn)有的知識來檢索相關(guān)的定理和陳述等，對證明 Agents 來說是非常有幫助且至關(guān)重要的。因此，一個開放性挑戰(zhàn)和未來方向是如何設(shè)計出更適合這種形式的數(shù)學(xué)以及利用這些數(shù)學(xué)庫的更好的模型和檢索機制。

另一個有趣的問題是，如何調(diào)和專家型和記者型的方法。記者型方法能夠識別跨領(lǐng)域的聯(lián)系，而專家型方法則在各個具體領(lǐng)域中表現(xiàn)出高效性。我們希望可以將這兩種方法結(jié)合起來，例如通過為模型配備特定領(lǐng)域的工具等方式。

現(xiàn)在，我將簡要談?wù)剝蓚€主要應(yīng)用領(lǐng)域的開放性挑戰(zhàn)和未來發(fā)展方向，一個是在輔助人類數(shù)學(xué)家發(fā)展更好的數(shù)學(xué)，另一個是在程序生成、共生成和驗證領(lǐng)域。

對于形式化數(shù)學(xué)（AFFMO），其動機和價值在于，我們希望這些工具能夠真正幫助人類數(shù)學(xué)家通過解決具有挑戰(zhàn)性的數(shù)學(xué)問題、開發(fā)新的定理和證明等，在形式化數(shù)學(xué)領(lǐng)域取得進(jìn)展。

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

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

我們希望借助這些工具，能夠真正實現(xiàn)大規(guī)模的分布式協(xié)作，讓分布在全球的數(shù)學(xué)家與 AI 工具攜手合作，將大型項目分解為不同的組件，整個社區(qū)共同攻克具有挑戰(zhàn)性和復(fù)雜性的數(shù)學(xué)問題。

另一個非常重要的應(yīng)用領(lǐng)域是代碼生成和程序驗證。

它的目標(biāo)不僅僅是利用 AI 來解決數(shù)學(xué)問題，更重要的是，它可以幫助從程序驗證的角度來構(gòu)建正確且安全的程序。

如今，與 LLaMA 相關(guān)的代碼生成已經(jīng)得到了廣泛的應(yīng)用。有估計表明，在一些公司和項目中，超過 50% 的代碼現(xiàn)在是由LLaMA生成的。但與此同時，確保生成代碼的正確性和安全性面臨著巨大的挑戰(zhàn)。例如，通過幾個測試用例可以看到 AI 生成的代碼不一定是正確的。

所以，我們不應(yīng)該僅僅生成代碼，而應(yīng)該進(jìn)行可驗證的代碼生成——即在生成代碼的同時，還要生成代碼的形式化規(guī)范、以及證明生成的代碼符合這些形式化規(guī)范的形式化證明。

比如我想為這個問題生成代碼，計算變量的絕對值函數(shù)，那么我們實際上可以生成代碼的規(guī)范，同時也能生成證明。通過這種方式，就可以確保生成代碼的正確性。

綜上，我已經(jīng)討論了 AI 在形式化數(shù)學(xué)領(lǐng)域的多個不同方向和應(yīng)用領(lǐng)域中的開放性挑戰(zhàn)和未來發(fā)展方向。

我認(rèn)為，在這個領(lǐng)域，接下來的五年將會非常令人激動。我們希望將整個社區(qū)凝聚在一起，共同推動 AI 在形式化數(shù)學(xué)和定理證明領(lǐng)域的發(fā)展。

六、Goedel-Prover：自動定理證明領(lǐng)域的開源模型

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

在這次演講中，我會介紹我們開發(fā)的系統(tǒng)：Goedel-Prover。這個名字來源于 G?del（哥德爾），一位在形式化系統(tǒng)領(lǐng)域非常著名的數(shù)學(xué)家。Goedel-Prover 是一個開源模型，在自動定理證明方面達(dá)到了當(dāng)前的最佳性能水平。

論文鏈接：https://arxiv.org/abs/2502.07640

我首先會稍微談?wù)勗u估，因為我之前提出了一個比較大膽的主張，說我們達(dá)到了最佳性能水平。所以，這就引出了一個問題：我們?nèi)绾卧u估模型，以及我們?nèi)绾闻袛嘁粋€模型是好的，另一個模型是不好的。

正如前述，形式化數(shù)學(xué)的一個重大挑戰(zhàn)是數(shù)據(jù)稀缺。現(xiàn)有的訓(xùn)練數(shù)據(jù)和評估方式在某種程度上是有限的，這是開源社區(qū)中主要的數(shù)據(jù)集和基準(zhǔn)測試。訓(xùn)練數(shù)據(jù)本質(zhì)上是既包含 Lean 中的問題陳述，也包含 Lean 中的證明。

也就是說，我們?yōu)槟闾峁┝诉@些問題陳述的形式化證明，還有評估數(shù)據(jù)集，其中很多數(shù)據(jù)集只包含問題陳述，沒有證明。也就是說，我們需要讓模型自己生成證明，并讓 Lean 編譯器檢查這些證明是否正確。

其中非常著名的一個是數(shù)據(jù)集 MiniF2F。很多模型都在這個數(shù)據(jù)集上進(jìn)行了評估。它包含了不同難度級別的數(shù)學(xué)問題，有些非常難，有些則相對簡單。

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

在我們討論完評估數(shù)據(jù)集之后，我們還會評估性能。我們還希望討論一下在我們之前，什么是最佳模型（SOTA，State of the Art）。為了能夠進(jìn)行非常公平的比較，生成這種形式化數(shù)學(xué)的系統(tǒng)主要有兩種類型：

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

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

另一種類型是樹搜索方法。與一次性生成整個證明不同，這種方法是逐步生成的。在生成一步之后，我們會使用某種樹搜索算法，比如廣度優(yōu)先搜索或最佳優(yōu)先搜索等，來搜索可能的最佳下一步。一些代表性模型，比如InternLMs 和 AlphaProof 系統(tǒng)（我認(rèn)為它既用于幾何問題，也用于代數(shù)問題），都采用了這種基于樹的方法。

我們只與整體證明生成系統(tǒng)進(jìn)行比較，因為我們的模型 Goedel-Prover是一個整體證明生成系統(tǒng)。不過，我們也有其他方法可以與開源的樹搜索方法和內(nèi)部方法進(jìn)行比較。我們沒有與 AlphaProof 進(jìn)行比較，因為它是一個閉源系統(tǒng)，盡管它的性能非常好，但到目前為止，該模型并未開源。

首先，我會關(guān)注小型化數(shù)據(jù)集。我們在路徑集32上進(jìn)行了評估，此前的最佳水平是DeepSeek Prover，他們在經(jīng)過監(jiān)督微調(diào)或強化學(xué)習(xí)后有一些變體。在路徑32上，這是一個相對較小的預(yù)算，比如采樣推理時間，他們達(dá)到了大約50%的準(zhǔn)確率。而我們的模型在路徑32上達(dá)到了57%的準(zhǔn)確率，比之前的最佳水平高出7個百分點。

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

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

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

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

在介紹完我們的性能之后，我還想稍微說一下我們是如何實現(xiàn)這一成果的。

事實證明，我們的整體方法并不復(fù)雜，這正是我喜歡的——它非常簡單且清晰，我認(rèn)為這作為一個起點，對于推動自動定理證明的發(fā)展是非常好的。

形式化數(shù)學(xué)中最關(guān)鍵的挑戰(zhàn)之一就是數(shù)據(jù)稀缺。

盡管 DeepSeek 聲稱他們形式化了很多大型數(shù)據(jù)集，但不幸的是，在開源社區(qū)中，可用的數(shù)據(jù)集和數(shù)據(jù)非常稀少。你可以看到，我們大約有 1000 萬非形式化的問題，但形式化的問題陳述卻少得多，例如，我們只有大約 40 萬形式化的問題陳述，以及僅有 1.5 萬個形式化的證明，這個數(shù)量是非常非常少的?；谶@樣少量的數(shù)據(jù)，要訓(xùn)練出一個好的證明器是非常困難的。

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

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

關(guān)于直接進(jìn)行自動形式化陳述，存在一些問題：

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

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

因此，我們會使用“四重完整性測試”，本質(zhì)上是要求四個大型語言模型作為獨立的裁判，獨立判斷這些問題是否是正確的翻譯，并基于一系列標(biāo)準(zhǔn)對語言模型進(jìn)行提示。然后，我們會要求它們進(jìn)行多數(shù)投票。經(jīng)過這些流程后，我們最終得到了超過一百萬條能夠通過這兩項測試的形式化陳述，并將這些陳述用作我們的訓(xùn)練數(shù)據(jù)集。

需要注意的是，這僅僅是關(guān)于問題陳述，而不涉及證明。那么在我們得到了這些問題之后，如何獲取更多的證明呢？我們使用這種迭代訓(xùn)練的方法。這是一個獲取更多證明的流程。

我們會從某個基礎(chǔ)模型開始。當(dāng)我們有了基礎(chǔ)模型后，比如 Goedel-Prover 的第一版，它基于 DeepSeek Base 7B模型。我們將大量的形式化陳述輸入其中，然后進(jìn)行推理，證明器能夠生成一些證明。在生成了一些證明之后，我們將它們提交給 Lean 編譯器，Lean 會驗證這些證明。我們會發(fā)現(xiàn)其中一些證明是正確的，然后將這些正確的證明加入到我們的數(shù)據(jù)集中，用于下一輪訓(xùn)練。

通過這種迭代訓(xùn)練的方式，我們可以獲得越來越多的證明，并將越來越多的形式化證明加入到我們的數(shù)據(jù)集中。我們能夠基于越來越多的證明進(jìn)行訓(xùn)練，這就是我們獲取更多形式化證明的方法。

表格如下：我們在進(jìn)行迭代訓(xùn)練時，不僅在不斷增加更多的證明，還在迭代地增加更多的陳述。這樣，當(dāng)一個模型的容量更大時，隨著我們增加更多陳述，模型的表現(xiàn)也會更好。

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

在多個數(shù)據(jù)集上進(jìn)行訓(xùn)練，甚至在一些統(tǒng)計誤差范圍內(nèi)，這已經(jīng)被證明是一種相當(dāng)有效的方法，它有點像在多次迭代中單調(diào)地提升性能。

這是我們整個模型的“配方”。這是我們推動自動形式化定理證明極限的第一步。在我們的模型的第一個版本中，我們提升了 CFR 性能，解決了多個 F2F 問題。我們還在 Putnam 基準(zhǔn)測試中取得了第一名，并且在主要工作手冊中解決了幾乎兩倍數(shù)量的問題。（雷峰網(wǎng)(公眾號：雷峰網(wǎng))雷峰網(wǎng)雷峰網(wǎng)）

雷峰網(wǎng)原創(chuàng)文章，未經(jīng)授權(quán)禁止轉(zhuǎn)載。詳情見轉(zhuǎn)載須知。