機器之心報道編輯：Panda、佳琪對 AI 研究者來說，數(shù)學(xué)既是一類難題，也是一個標(biāo)桿，能夠成為衡量 AI 技術(shù)的發(fā)展重要尺度。近段時間，隨著 AI 推理能力的提升，使用 AI 來證明數(shù)學(xué)問題已經(jīng)成為一個重要的研究探索方向。著名數(shù)學(xué)家陶哲軒就是這一方向的推動者，他曾表示：未來數(shù)學(xué)家可以通過向類似 GPT 的 AI 解釋證明，AI 會將其形式化為 Lean 證明。這種助手型 AI 不僅能生成 LaTeX 文件，還能幫助提交論文，從而大幅提高數(shù)學(xué)家的工作效率和便利性。如今，已經(jīng)誕生了 Gemini 2.0 Flash Thinking 和 o1/o3 等強大推理模型，那么用 AI 來進行形式化數(shù)學(xué)推理又已經(jīng)走到了哪一步呢？Meta FAIR 和斯坦福大學(xué)等多所機構(gòu)的一篇新的立場論文（position paper）或許能為你給出這個問題的答案。
論文標(biāo)題：Formal Mathematical Reasoning: A New Frontier in AI
論文地址：https://arxiv.org/pdf/2412.16075
本文一作楊凱峪在 X 上表示，AI4Math 的下一步是使用證明助手等形式化系統(tǒng)來實現(xiàn)形式化數(shù)學(xué)推理。他也在推文以及論文中感謝了陶哲軒等數(shù)學(xué)家提供的反饋。
Meta 研究科學(xué)家田淵棟也分享轉(zhuǎn)發(fā)了這篇立場論文，并表示很期待看到 AI 能基于現(xiàn)有的互聯(lián)網(wǎng)數(shù)據(jù)在數(shù)學(xué)階梯上能到達何種高度。
這篇論文的內(nèi)容相當(dāng)豐富，機器之心將在此介紹該論文的主要內(nèi)容結(jié)構(gòu)，尤其是該團隊對多個相關(guān)研究方向的分級策略。這些分級可以幫助我們更好地界定 AI 在形式化數(shù)學(xué)推理方面的進展。下圖為該綜述的目錄截圖。
自 AI 誕生之初，研究者就夢想著構(gòu)建能夠自動進行數(shù)學(xué)推理的 AI 系統(tǒng)。歷史上，首個此類 AI 程序是 Newell 和 Simon 打造的 Logic Theorist（邏輯理論家），這個定理證明系統(tǒng)能夠證明《數(shù)學(xué)原理》中的 38 條定理。自那之后已過去數(shù)十年，AI 的中心已經(jīng)從符號方法轉(zhuǎn)移到了機器學(xué)習(xí)，并出現(xiàn)了一個新領(lǐng)域：用于數(shù)學(xué)的統(tǒng)計式人工智能（AI4Math）。這是一個非常吸引人的領(lǐng)域。原因不難理解，很多推理和規(guī)劃任務(wù)本質(zhì)上都是數(shù)學(xué)問題。另外，數(shù)學(xué)在定量學(xué)科中起著基礎(chǔ)性作用，因此 AI4Math 有可能給科學(xué)、工程和其他領(lǐng)域的人工智能帶來革新。也正因為這些原因，LLM 開發(fā)者通常會把數(shù)學(xué)問題求解能力作為一個核心衡量指標(biāo)，人們也在努力創(chuàng)造能在數(shù)學(xué)問題上比肩甚至超越人類的 AI 系統(tǒng)。AI4Math 的重要性吸引了大量研究者，他們開始使用來自自然語言處理（NLP）領(lǐng)域的技術(shù)來開發(fā)數(shù)學(xué) LLM。一種常用方法是使用數(shù)學(xué)數(shù)據(jù)來對 LLM 進行持續(xù)預(yù)訓(xùn)練，比如可以使用來自 arXiv 論文和 MathOverflow 網(wǎng)頁的數(shù)據(jù)，然后在精心選擇的數(shù)學(xué)問題數(shù)據(jù)集（其中會提供詳細(xì)的分步解決方案）上對模型進行微調(diào)。該團隊稱之為非形式化（informal）方法。類似于通用 LLM，數(shù)學(xué) LLM 的配方也很簡單，秘訣往往在于數(shù)據(jù)的整編。在 GSM8K、MATH、AIMO Progress Prize 等常用基準(zhǔn)上取得進展的數(shù)學(xué) LLM 通常包含精心整編的訓(xùn)練數(shù)據(jù)集、思維鏈等推理時間技術(shù)、自我一致性和工具使用能力。然而，直到本文寫作時，非形式化方法得到的 AI 的數(shù)學(xué)能力基本都不超過 AIME 的高中數(shù)學(xué)水平。那么，問題就來了：非形式化方法的規(guī)模擴展之路還能走多遠(yuǎn)？它能讓數(shù)學(xué) LLM 解決更具挑戰(zhàn)性的競賽問題（例如，IMO、國際數(shù)學(xué)奧林匹克）甚至還在研究中的數(shù)學(xué)問題嗎？從高中到更高級的數(shù)學(xué)，非形式方法面臨的難題無法僅僅通過規(guī)模擴展解決。首先，訓(xùn)練數(shù)學(xué) LLM 需要高質(zhì)量的數(shù)據(jù)，而高質(zhì)量高等數(shù)學(xué)數(shù)據(jù)很稀缺。對于新的研究數(shù)學(xué)問題，不可能在互聯(lián)網(wǎng)上找到類似問題的解答或大規(guī)模手動標(biāo)注數(shù)據(jù)。如果沒法擴大數(shù)據(jù)規(guī)模，就不可能充分享受到 LLM 的 Scaling Law。
第二，很多高等數(shù)學(xué)的解并不是數(shù)值，因此難以通過比較 ground truth 來進行評估。例如證明問題需要一系列復(fù)雜的推理步驟。LLM 還有個臭名昭著的幻覺問題，會生成看起來可行的推理步驟，因此評估模型輸出或收集有用反饋的難度非常大。這些問題都難以通過擴大非形式化方法的規(guī)模來解決。如果訓(xùn)練時間擴展不夠用，那我們還需要什么呢？OpenAI o1 展示了一個可能方向：在推理時間擴展非形式化方法，比如將搜索與神經(jīng)驗證器組合起來緩解推理幻覺。雖然這種方法吸引了很多人的眼球，但它究竟能不能有效解決高等數(shù)學(xué)問題還有待解答。而本篇立場論文關(guān)注的則是一個較少被探索的補充方法：形式化數(shù)學(xué)推理（formal mathematical reasoning。該團隊表示，形式化數(shù)學(xué)推理是指立足于形式化系統(tǒng)的數(shù)學(xué)推理，而形式化系統(tǒng)包括但不限于一階 / 高階邏輯、依賴類型理論和帶有形式規(guī)范注釋的計算機程序。這種形式化系統(tǒng)可提供驗證模型推理并提供自動反饋的環(huán)境。它們不同于現(xiàn)代 LLM 使用的「工具」，因為它們可以建模廣泛命題的真與假，并且還是可證明的。此類系統(tǒng)提供的反饋可以緩解數(shù)據(jù)稀缺問題；此外，此類系統(tǒng)還可以進行嚴(yán)格的測試時間檢查，以抵抗幻覺。相比之下，非形式化數(shù)學(xué)是指教科書、研究論文和在線數(shù)學(xué)論壇中常見的數(shù)學(xué)文本。非形式化數(shù)學(xué)會將自然語言與符號（例如 LATEX）交織在一起，但這些符號沒有自我包含的形式語義，而是依靠非形式文本來傳達其含義的重要部分。AlphaProof 和 AlphaGeometry 是這一想法成功的兩個突出例子。在此之前，很多研究者嘗試過使用 LLM 來解決奧數(shù)級數(shù)學(xué)問題，但都失敗了。上述系統(tǒng)的關(guān)鍵區(qū)別在于原則性地使用了符號表示和證明檢查框架。其中，符號組件（AlphaProof 的 Lean、AlphaGeometry 的特定領(lǐng)域幾何系統(tǒng)）的作用是執(zhí)行神經(jīng)網(wǎng)絡(luò)的推理步驟并生成高質(zhì)量的合成數(shù)據(jù)，從而實現(xiàn)前所未有的數(shù)學(xué)推理能力。AlphaProof 和 AlphaGeometry 之前，已經(jīng)有許多文獻做好了鋪墊 它們探討了形式化方法和機器學(xué)習(xí)在數(shù)學(xué)任務(wù)中的協(xié)同使用。具體涉及的主題包括神經(jīng)定理證明、自動形式化（autoformalization）等。LLM 的出現(xiàn)大大加速了這一領(lǐng)域的研究。例如，由于缺乏用于微調(diào)的已對齊非形式化 - 形式化對，自動形式化長期以來一直都進展緩慢。LLM 可以通過合成數(shù)據(jù)或執(zhí)行無微調(diào)自動形式化來緩解此問題。因此，人們開始認(rèn)識到自動形式化在引導(dǎo)神經(jīng)定理證明器方面的潛力。LLM 也是定理證明的強大工具；事實上，最近已有方法利用 LLM 來預(yù)測證明步驟并修復(fù)有缺陷的證明，同時還無需基于形式化證明數(shù)據(jù)進行明確訓(xùn)練。圍繞 LLM 和形式化推理的研究基礎(chǔ)設(shè)施正在迅速成熟。Lean 這種用于編寫形式化證明的語言在數(shù)學(xué)家中越來越受歡迎，并催生了形式化研究數(shù)學(xué)和通用數(shù)學(xué)庫。現(xiàn)在已有多個框架可支持 LLM 和 Lean 之間的交互。這些框架支持基于人工編寫的形式化證明提取訓(xùn)練數(shù)據(jù)，以及通過與形式化環(huán)境的交互進行定理證明。
除了 Lean 之外，Coq 和 Isabelle 等證明語言的多語言基礎(chǔ)設(shè)施也已在構(gòu)建中 。最后，LLM 已被用于協(xié)助人類數(shù)學(xué)家編寫形式化證明 ，這可能會啟動一個數(shù)據(jù)飛輪，其中不斷增長的人類編寫的形式化數(shù)學(xué)數(shù)據(jù)會產(chǎn)生更強大的 LLM，從而讓人可以更輕松地創(chuàng)建更多數(shù)據(jù)。AI 在形式化數(shù)學(xué)推理方面大有機會，因而研究繁盛。AI 在形式化數(shù)學(xué)推理方面的新興機會導(dǎo)致了研究活動的蓬勃發(fā)展。正如最近的一項調(diào)查給出的那樣，該領(lǐng)域的發(fā)表文獻數(shù)量在 2023 年幾乎翻了一番，并且很可能在 2024 年再翻一番。通過將自動形式化與強化學(xué)習(xí)相結(jié)合，AlphaProof 成為第一個在 IMO 中獲得銀牌的人工智能。該領(lǐng)域的進展也可直接應(yīng)用于形式化驗證（formal verification） ，這是一個核心的計算機科學(xué)問題，傳統(tǒng)上一直是形式化數(shù)學(xué)最重要的應(yīng)用之一。雖然形式化驗證可以得到極其穩(wěn)健和安全的軟件和硬件系統(tǒng)，但從歷史上看，除了安全性至關(guān)重要的應(yīng)用之外，形式化驗證其實很少用，因為其部署成本太高。AI 可以通過自動化形式化和證明工作來大幅降低這一成本。這可能導(dǎo)致未來大規(guī)模生產(chǎn)的軟件和硬件系統(tǒng)比現(xiàn)在更加穩(wěn)健。該團隊表示：「出于所有這些原因，我們相信基于 AI 的形式化數(shù)學(xué)推理已經(jīng)到達了一個轉(zhuǎn)折點，未來幾年將取得重大進展。然而，仍有大量工作要做。」本立場論文概述了該領(lǐng)域在數(shù)據(jù)和算法方面面臨的難題，以及未來進步的可能路線。AI4Math 與形式化數(shù)學(xué)推理數(shù)學(xué)推理是 AI 領(lǐng)域的前沿研究方向。本節(jié)首先將介紹 AI4Math 的非形式化方法及其局限性。然后將介紹在推進 AI4Math 方面，形式化數(shù)學(xué)推理是一條有希望的道路。這一節(jié)涵蓋的內(nèi)容包括：當(dāng)前最佳的數(shù)學(xué) LLM 以及它們的局限性，目前的難題包括數(shù)據(jù)稀缺、缺乏驗證正確性的手段。用于形式化數(shù)學(xué)推理的 AI：這一節(jié)將介紹從非形式化到形式化的轉(zhuǎn)向、證明助理和 Lean 等。
數(shù)學(xué) AI 的其它方向：AI4Math 范圍很廣，還包含其它許多研究方向，比如使用神經(jīng)網(wǎng)絡(luò)來近似函數(shù)等等。用于形式化數(shù)學(xué)推理的 AI 的最新進展AI 已在形式數(shù)學(xué)推理方面取得了實質(zhì)性進展。本節(jié)首先將討論兩個關(guān)鍵任務(wù)的進展：自動形式化和定理證明。然后將抽樣兩個相鄰領(lǐng)域 自然語言和代碼生成 它們可受益于形式化方法實現(xiàn)的可驗證推理。在自動形式化方面，本文介紹了基于規(guī)則的自動形式化、基于神經(jīng)和 LLM 的自動形式化、自動形式化的應(yīng)用。
在神經(jīng)定理證明方面，本文介紹了專家迭代、從錯誤中學(xué)習(xí)、非正式證明草圖、庫學(xué)習(xí)、前提選擇和檢索等主題。
此外，這一節(jié)還介紹了自然語言中的驗證推理、形式系統(tǒng)驗證和驗證生成。挑戰(zhàn)與未來的方向這一節(jié)，該團隊分享了幾個仍待解決的挑戰(zhàn)和有希望的研究方向，包括形式化數(shù)學(xué)推理的數(shù)據(jù)和算法、協(xié)助人類數(shù)學(xué)家和證明工程師的 AI 工具，以及集成 AI 和形式化方法來生成可驗證代碼。數(shù)據(jù)數(shù)據(jù)稀缺是首要問題。潛在的解決方案包括:
從教科書、論文和講義中自動形式化非形式化數(shù)學(xué)內(nèi)容
基于數(shù)學(xué)公理生成合成的猜想和證明
從不同的證明框架和代碼等數(shù)據(jù)豐富的領(lǐng)域遷移知識
算法在這個方面，又有許多亟待解決的問題，該團隊也提出了一些解決的設(shè)想：問題 1：如何讓 AI 能夠自動地將非形式化的內(nèi)容轉(zhuǎn)換成形式化的數(shù)學(xué)語言？
建立自動形式化語句的評估指標(biāo)
將形式化過程分解為小步驟
加強與形式系統(tǒng)的交互
問題 2：如何改進數(shù)學(xué)推理的模型架構(gòu)？
增強多步推理、長文本處理、抽象和分層規(guī)劃能力
通過合成基準(zhǔn)診斷推理失敗之處
利用檢索和搜索等推理技術(shù)輔助模型
問題 3：如何有效地搜索證明？
對搜索進行擴展以利用更多的測試時間計算；
對模型、搜索算法和超參數(shù)進行系統(tǒng)性評估；
用于評估證明目標(biāo)并為其設(shè)定優(yōu)先級的價值模型。
問題 4：如何利用定理證明中的層次結(jié)構(gòu)？
將大型、高級證明目標(biāo)逐步分解為較小的目標(biāo)。
問題 5：如何學(xué)習(xí)數(shù)學(xué)抽象？
學(xué)習(xí)在成熟的證明助手中構(gòu)建新的定義、引理和策略。
問題 6：如何利用現(xiàn)有的數(shù)學(xué)知識？
為形式數(shù)學(xué)推理量身定制的檢索器；
處理動態(tài)增長的知識庫。
問題 7：如何協(xié)調(diào)專家方法和通用方法？
識別跨領(lǐng)域聯(lián)系的通用方法；
針對各個領(lǐng)域的有效性的專家方法以及與數(shù)學(xué)家合作的專家方法；
將通用方法和專家方法結(jié)合起來，例如為 LLM 配備特定領(lǐng)域的工具。
用于輔助人類數(shù)學(xué)家的工具這方面的主要問題是：AI 如何更好地協(xié)助人類研究形式化數(shù)學(xué)？這個方面的難題和潛在研究方向包括：
資源、激勵措施和工程開發(fā)，以提高可用性和用戶友好性；
研究數(shù)學(xué)家如何使用形式化工具的行為；
支持大規(guī)模分布式協(xié)作的工具。
形式驗證和已驗證生成這方面的主要問題是：AI 如何輔助人類開發(fā)正確和安全的軟件？這個方面的難題和潛在研究方向包括：
將形式化方法納入 AI 輔助的系統(tǒng)設(shè)計和實現(xiàn)中；
增強 AI 進行形式化軟件和硬件驗證的能力；
將基于 AI 的生成與形式化驗證結(jié)合起來。
評估標(biāo)準(zhǔn)在解決問題的過程中，一個關(guān)鍵問題逐漸浮現(xiàn)：如何有效衡量進展？受自動駕駛汽車自動化等級的啟發(fā)，該團隊提出了一個評估 AI 數(shù)學(xué)推理能力的分級框架。他們強調(diào)，在這個新興領(lǐng)域還需要建立更多新的基準(zhǔn)和評估方法。定理證明能力目前，AI 在形式數(shù)學(xué)領(lǐng)域的主要工作集中在自動定理證明上。像 Lean 這樣的形式系統(tǒng)提供了巨大優(yōu)勢 - 一旦找到證明，即使人可能沒完全理解，就能保證其正確性。研究團隊根據(jù)表 1 給出了 AI 形式定理證明的分級基準(zhǔn)。
在最基礎(chǔ)的 0 級水平，AI 能夠識別正確的形式證明。到了 1 級，AI 系統(tǒng)可以提供潛在有用的數(shù)據(jù)，但還不能寫出證明。2 級及以上的系統(tǒng)可以生成完整或部分證明。人類專家設(shè)計和編寫的固定證明策略和規(guī)則，AI 按照這些預(yù)設(shè)的策略執(zhí)行證明過程。在 3 級水平，AI 系統(tǒng)能夠在一般領(lǐng)域自動證明定理，但仍局限于簡單定理。4 級系統(tǒng)應(yīng)該能夠自主規(guī)劃和執(zhí)行形式化項目，分解大型結(jié)果，提出新的定義和定理，并在探索的過程中嘗試不同的解決方案。5 級則意味著系統(tǒng)能夠解決超出人類水平的問題。自然語言推理驗證能力研究團隊首先提出了一個問題：如何在不完全形式化的情況下實現(xiàn)嚴(yán)謹(jǐn)?shù)耐评�？他們發(fā)現(xiàn)，讓 AI 在形式系統(tǒng)和自然語言之間切換是一個很有前景的方向。這樣的 AI 系統(tǒng)應(yīng)該能夠進行邏輯推理、數(shù)值計算，并以嚴(yán)謹(jǐn)且易懂的方式生成答案。雖然推理過程可能不是嚴(yán)格的形式化證明，但其中的部分內(nèi)容仍可以在人工的監(jiān)督下以半自動化的形式驗證。該團隊將這種能力稱為「自然語言驗證推理」，并提出了一個分級框架 (表 2)。
在 0 級水平，AI 能夠用自然語言生成逐步推理過程，但不涉及驗證。到了 1 級，AI 系統(tǒng)在生成推理的同時具備了驗證能力，可以評估每個推理步驟的正確性。在 2 級，AI 系統(tǒng)能夠利用外部工具，執(zhí)行單靠神經(jīng)網(wǎng)絡(luò)難以學(xué)會的計算任務(wù)。第 3 級的 AI 系統(tǒng)將可以使用外部工具進行嚴(yán)格的邏輯推理。在第 4 級，AI 系統(tǒng)能夠識別日常任務(wù)中的數(shù)學(xué)問題并使用嚴(yán)謹(jǐn)?shù)姆椒āζ溥M行推理自動形式化的能力該團隊提出了一個自動形式化能力評估體系，評估 AI 如何在數(shù)學(xué)知識的非形式化表述和形式化表述之間自動轉(zhuǎn)換。
根據(jù)表 3，在最基礎(chǔ)的 0 級水平，AI 系統(tǒng)能夠存儲和檢驗形式化知識，方便人工形式化。在第 1 級，AI 將可以為自動生成形式化的幾種草稿，并通過持續(xù)收集和存儲人類反饋來不斷改進系統(tǒng)性能。到了第 2 級，AI 應(yīng)能夠在兩者之間進行穩(wěn)定且準(zhǔn)確的轉(zhuǎn)換，準(zhǔn)確度接近人類水平。第 3 級的 AI 系統(tǒng)能夠在形式化的過程中推斷出缺失餓信息，并標(biāo)記出它無法補全的部分。在第 4 級，AI 將具備遇到錯誤或?qū)Σ簧系妮斎霑r自我糾正的能力。最后在第 5 級，該團隊預(yù)計 AI 將能夠創(chuàng)造新的數(shù)學(xué)定義，有望降低證明的復(fù)雜度。猜想能力研究團隊發(fā)現(xiàn)，在數(shù)學(xué)研究中，提出定理證明之前的猜想階段同樣重要。該團隊認(rèn)為，AI 有望自主提出數(shù)學(xué)猜想。根據(jù)表 4 的分級標(biāo)準(zhǔn)，0 級水平是指 AI 能夠針對特定問題或目標(biāo)結(jié)果提出相關(guān)猜想。更進一步，在 1 級水平上，AI 就預(yù)計可以在給定研究領(lǐng)域內(nèi)自主提出猜想，而不必局限于某個具體定理了。
形式化驗證與驗證生成的結(jié)果研究團隊最新發(fā)現(xiàn)，把 AI 應(yīng)用到程序驗證和系統(tǒng)開發(fā)時，面臨的挑戰(zhàn)與數(shù)學(xué)研究有很大不同。為了更好地理解這個領(lǐng)域，該團隊設(shè)計了一個 4 級能力評估體系 (表 5)。
在最基礎(chǔ)的第 1 級，AI 已經(jīng)能夠完成一些簡單的驗證工作，比如檢查小段代碼是否正確，或者自動生成一些簡單的可驗證代碼。到了第 2 級，AI 的能力提升到可以幫助開發(fā)團隊驗證整個項目，并且能處理更復(fù)雜的問題。第 3 級是一個重要突破，AI 不僅能生成代碼，還能提供證明并幫助維護系統(tǒng)。在最高的第 4 級，AI 可以幫助開發(fā)人員制定技術(shù)規(guī)范，包括自動生成規(guī)范文檔、解釋具體要求，以及幫助找出規(guī)范中的問題。
