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

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

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

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

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

……

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

比如，如果你在監(jiān)督式微調(diào)中添加了大量數(shù)學(xué)提示和數(shù)學(xué)類型的數(shù)據(jù)，你可能會(huì)在知識(shí)回憶方面表現(xiàn)下降，因?yàn)槟憧偸窍Ｍ稍絹?lái)越長(zhǎng)的思考鏈。所以，數(shù)據(jù)混合是構(gòu)建一個(gè)好的微調(diào)模型中非常重要的一步。

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

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

這其實(shí)并不是一個(gè)新想法，它在自然語(yǔ)言處理（NLP）領(lǐng)域的語(yǔ)義解析、語(yǔ)義理解和推理方面已經(jīng)被研究很久了。但現(xiàn)在它又在語(yǔ)言模型中重新受到關(guān)注，因?yàn)槿缃裎覀兛梢蕴幚磉@種既包含語(yǔ)言又包含形式化表達(dá)的推理鏈。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

當(dāng)我們引入更大的獎(jiǎng)勵(lì)模型時(shí)，這是非常直觀的——當(dāng)我們有一個(gè)更大的獎(jiǎng)勵(lì)模型時(shí)，我們期望PPO能取得更好的結(jié)果，但實(shí)際的提升并沒(méi)有達(dá)到我們的預(yù)期。我們?cè)疽詾椋辛烁蟮莫?jiǎng)勵(lì)模型，我們應(yīng)該會(huì)看到一個(gè)很大的跳躍，但結(jié)果卻只是這么多。我們并沒(méi)有看到太多提升，這讓我們感到非常驚訝。

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

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

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

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

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

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

研究發(fā)現(xiàn)，我們?cè)谑褂盟心Ｐ蜁r(shí)看到了很大的提升。我們展示出，與之前的偏好數(shù)據(jù)混合集相比，我們看到了一個(gè)巨大的進(jìn)步。同樣，我們進(jìn)行了大量的數(shù)據(jù)混合分析，研究應(yīng)該從監(jiān)督微調(diào)（SFT）中引入多少初始提示，以及應(yīng)該引入多少新的提示。這經(jīng)過(guò)了大量的實(shí)驗(yàn)，以確定最佳的混合比例。

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

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

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

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

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

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

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

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

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

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

這也與 DeepSeek V3 的發(fā)現(xiàn)非常一致，他們發(fā)現(xiàn)在處理更大模型時(shí)，強(qiáng)化學(xué)習(xí)帶來(lái)的改進(jìn)更為顯著。這實(shí)際上是一個(gè)非常有趣的觀察。這也引出了我們?cè)诒敬斡懻撻_(kāi)始時(shí)提到的觀點(diǎn)，即如果基礎(chǔ)模型變得更好，那么我們對(duì)強(qiáng)化學(xué)習(xí)微調(diào)（RFM）的期望也會(huì)更高。

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

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

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

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

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

如果模型沒(méi)有用完它的標(biāo)記預(yù)算，我們就添加一種延續(xù)標(biāo)記，后讓模型再思考一會(huì)兒。通過(guò)這種方式，我們發(fā)現(xiàn)模型現(xiàn)在能夠生成更好、更深入的推理路徑，這非常有趣。還有一個(gè)更有趣的事實(shí)：當(dāng)我們沒(méi)有添加任何標(biāo)記，只是簡(jiǎn)單地讓模型生成更多內(nèi)容時(shí)，我們并沒(mé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)悟到測(cè)試時(shí)通過(guò)驗(yàn)證器進(jìn)行的擴(kuò)展。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

這種情況也適用于其他類型的規(guī)劃任務(wù)，比如讓 Agents 將箱子推到目的地，這需要非常謹(jǐn)慎的規(guī)劃。因?yàn)槿绻渥颖煌频浇锹?，就沒(méi)有回頭路了。

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

通過(guò)“Searchformer”，我們發(fā)現(xiàn)最終得到的模型比原始的 A* 搜索模型更好，因?yàn)樗哂懈痰乃阉鬈壽E。這是由于采用了“直觀地址采樣”（Intuitive Address Sampling），這是一種簡(jiǎn)化的強(qiáng)化學(xué)習(xí)版本。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

未來(lái)需要我們繼續(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)用。事實(shí)上，我們可以利用各種經(jīng)過(guò)形式化驗(yàn)證的工具，比如定理證明器等。而且，實(shí)際上存在許多不同類型的定理證明系統(tǒng)。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

因?yàn)槲覀冞M(jìn)行自動(dòng)形式化時(shí)，并沒(méi)有后續(xù)的驗(yàn)證步驟，所以我們無(wú)法確切知道其他形式化的陳述是否真正正確。我們需要對(duì)它們進(jìn)行評(píng)估，并且需要開(kāi)發(fā)良好的指標(biāo)來(lái)評(píng)估這些形式化的陳述。

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

對(duì)于評(píng)估自動(dòng)形式化的陳述，有幾個(gè)原因使其相當(dāng)具有挑戰(zhàn)性。首先，我們不能依賴人工評(píng)估，因?yàn)檫@種方法無(wú)法擴(kuò)展。而對(duì)于其他形式化的陳述，通常存在不同的形式，即存在多種正確的方式來(lái)完成形式化，而自動(dòng)等價(jià)性檢查本身其實(shí)并不簡(jiǎn)單。

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

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

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

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

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

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

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

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

這很重要——正如我們?cè)谛问交瘮?shù)學(xué)中應(yīng)用 AI 一樣，我們也需要開(kāi)發(fā)具備這種能力的模型，能夠逐步將高級(jí)證明目標(biāo)分解為更小的目標(biāo)。

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

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

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

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

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

另一個(gè)對(duì)于數(shù)學(xué)的可擴(kuò)展性等來(lái)說(shuō)也很重要的是學(xué)習(xí)數(shù)學(xué)抽象。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

在這次演講中，我會(huì)介紹我們開(kāi)發(fā)的系統(tǒng)：Goedel-Prover。這個(gè)名字來(lái)源于 G?del（哥德?tīng)枺晃辉谛问交到y(tǒng)領(lǐng)域非常著名的數(shù)學(xué)家。Goedel-Prover 是一個(gè)開(kāi)源模型，在自動(dòng)定理證明方面達(dá)到了當(dāng)前的最佳性能水平。

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

我首先會(huì)稍微談?wù)勗u(píng)估，因?yàn)槲抑疤岢隽艘粋€(gè)比較大膽的主張，說(shuō)我們達(dá)到了最佳性能水平。所以，這就引出了一個(gè)問(wèn)題：我們?nèi)绾卧u(píng)估模型，以及我們?nèi)绾闻袛嘁粋€(gè)模型是好的，另一個(gè)模型是不好的。

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

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

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

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

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

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

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

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

我們只與整體證明生成系統(tǒng)進(jìn)行比較，因?yàn)槲覀兊哪Ｐ?Goedel-Prover是一個(gè)整體證明生成系統(tǒng)。不過(guò)，我們也有其他方法可以與開(kāi)源的樹(shù)搜索方法和內(nèi)部方法進(jìn)行比較。我們沒(méi)有與 AlphaProof 進(jìn)行比較，因?yàn)樗且粋€(gè)閉源系統(tǒng)，盡管它的性能非常好，但到目前為止，該模型并未開(kāi)源。

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

你也可以問(wèn)，當(dāng)我們?cè)黾油评碛?jì)算量時(shí)，我們的模型表現(xiàn)如何。這就是這張圖展示的內(nèi)容。我們可以看到一些一致的改進(jìn)，我們的模型與DeepSeek Prover之間大約有7個(gè)百分點(diǎn)的性能差距。

第二點(diǎn)是，我們還希望在 PutnamBench 上評(píng)估我們的模型。這是一個(gè)包含所有永久性數(shù)學(xué)競(jìng)賽問(wèn)題的基準(zhǔn)測(cè)試，這些問(wèn)題極具挑戰(zhàn)性。我們?cè)谠摶鶞?zhǔn)測(cè)試中獲得了第一名，解決了七個(gè)問(wèn)題。我認(rèn)為第二名的模型也解決了七個(gè)問(wèn)題，但它不是開(kāi)源的。我們排名第一，是因?yàn)槲覀儗?shí)際上使用了更少的推理時(shí)間和計(jì)算資源，我們通過(guò)了512。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

表格如下：我們?cè)谶M(jìn)行迭代訓(xùn)練時(shí)，不僅在不斷增加更多的證明，還在迭代地增加更多的陳述。這樣，當(dāng)一個(gè)模型的容量更大時(shí)，隨著我們?cè)黾痈嚓愂?，模型的表現(xiàn)也會(huì)更好。

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

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

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

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