對 AI 研究者來說，數(shù)學既是一類難題，也是一個標桿，能夠成為衡量 AI 技術(shù)的發(fā)展重要尺度。近段時間，隨著 AI 推理能力的提升，使用 AI 來證明數(shù)學問題已經(jīng)成為一個重要的研究探索方向。著名數(shù)學家陶哲軒就是這一方向的推動者，他曾表示：未來數(shù)學家可以通過向類似 GPT 的 AI 解釋證明，AI 會將其形式化為 Lean 證明。這種助手型 AI 不僅能生成 LaTeX 文件，還能幫助提交論文，從而大幅提高數(shù)學家的工作效率和便利性。

如今，已經(jīng)誕生了 Gemini 2.0 Flash Thinking 和 o1/o3 等強大推理模型，那么用 AI 來進行形式化數(shù)學推理又已經(jīng)走到了哪一步呢？

Meta FAIR 和斯坦福大學等多所機構(gòu)的一篇新的立場論文（position paper）或許能為你給出這個問題的答案。

• 論文標題：Formal Mathematical Reasoning: A New Frontier in AI
• 論文地址：https://arxiv.org/pdf/2412.16075

本文一作楊凱峪在 X 上表示，AI4Math 的下一步是使用證明助手等形式化系統(tǒng)來實現(xiàn)形式化數(shù)學推理。他也在推文以及論文中感謝了陶哲軒等數(shù)學家提供的反饋。

Meta 研究科學家田淵棟也分享轉(zhuǎn)發(fā)了這篇立場論文，并表示很期待看到 AI 能基于現(xiàn)有的互聯(lián)網(wǎng)數(shù)據(jù)在數(shù)學階梯上能到達何種高度。

這篇論文的內(nèi)容相當豐富，機器之心將在此介紹該論文的主要內(nèi)容結(jié)構(gòu)，尤其是該團隊對多個相關研究方向的分級策略。這些分級可以幫助我們更好地界定 AI 在形式化數(shù)學推理方面的進展。下圖為該綜述的目錄截圖。

自 AI 誕生之初，研究者就夢想著構(gòu)建能夠自動進行數(shù)學推理的 AI 系統(tǒng)。歷史上，首個此類 AI 程序是 Newell 和 Simon 打造的 Logic Theorist（邏輯理論家），這個定理證明系統(tǒng)能夠證明《數(shù)學原理》中的 38 條定理。

自那之后已過去數(shù)十年，AI 的中心已經(jīng)從符號方法轉(zhuǎn)移到了機器學習，并出現(xiàn)了一個新領域：用于數(shù)學的統(tǒng)計式人工智能（AI4Math）。

這是一個非常吸引人的領域。原因不難理解，很多推理和規(guī)劃任務本質(zhì)上都是數(shù)學問題。另外，數(shù)學在定量學科中起著基礎性作用，因此 AI4Math 有可能給科學、工程和其他領域的人工智能帶來革新。也正因為這些原因，LLM 開發(fā)者通常會把數(shù)學問題求解能力作為一個核心衡量指標，人們也在努力創(chuàng)造能在數(shù)學問題上比肩甚至超越人類的 AI 系統(tǒng)。

AI4Math 的重要性吸引了大量研究者，他們開始使用來自自然語言處理（NLP）領域的技術(shù)來開發(fā)數(shù)學 LLM。

一種常用方法是使用數(shù)學數(shù)據(jù)來對 LLM 進行持續(xù)預訓練，比如可以使用來自 arXiv 論文和 MathOverflow 網(wǎng)頁的數(shù)據(jù)，然后在精心選擇的數(shù)學問題數(shù)據(jù)集（其中會提供詳細的分步解決方案）上對模型進行微調(diào)。該團隊稱之為非形式化（informal）方法。

類似于通用 LLM，數(shù)學 LLM 的配方也很簡單，秘訣往往在于數(shù)據(jù)的整編。在 GSM8K、MATH、AIMO Progress Prize 等常用基準上取得進展的數(shù)學 LLM 通常包含精心整編的訓練數(shù)據(jù)集、思維鏈等推理時間技術(shù)、自我一致性和工具使用能力。

然而，直到本文寫作時，非形式化方法得到的 AI 的數(shù)學能力基本都不超過 AIME 的高中數(shù)學水平。

那么，問題就來了：非形式化方法的規(guī)模擴展之路還能走多遠？它能讓數(shù)學 LLM 解決更具挑戰(zhàn)性的競賽問題（例如，IMO、國際數(shù)學奧林匹克）甚至還在研究中的數(shù)學問題嗎？

從高中到更高級的數(shù)學，非形式方法面臨的難題無法僅僅通過規(guī)模擴展解決。

首先，訓練數(shù)學 LLM 需要高質(zhì)量的數(shù)據(jù)，而高質(zhì)量高等數(shù)學數(shù)據(jù)很稀缺。對于新的研究數(shù)學問題，不可能在互聯(lián)網(wǎng)上找到類似問題的解答或大規(guī)模手動標注數(shù)據(jù)。如果沒法擴大數(shù)據(jù)規(guī)模，就不可能充分享受到 LLM 的 Scaling Law。

第二，很多高等數(shù)學的解并不是數(shù)值，因此難以通過比較 ground truth 來進行評估。例如證明問題需要一系列復雜的推理步驟。

LLM 還有個臭名昭著的幻覺問題，會生成看起來可行的推理步驟，因此評估模型輸出或收集有用反饋的難度非常大。

這些問題都難以通過擴大非形式化方法的規(guī)模來解決。

如果訓練時間擴展不夠用，那我們還需要什么呢？OpenAI o1 展示了一個可能方向：在推理時間擴展非形式化方法，比如將搜索與神經(jīng)驗證器組合起來緩解推理幻覺。

雖然這種方法吸引了很多人的眼球，但它究竟能不能有效解決高等數(shù)學問題還有待解答。

而本篇立場論文關注的則是一個較少被探索的補充方法：形式化數(shù)學推理（formal mathematical reasoning。

該團隊表示，形式化數(shù)學推理是指立足于形式化系統(tǒng)的數(shù)學推理，而形式化系統(tǒng)包括但不限于一階 / 高階邏輯、依賴類型理論和帶有形式規(guī)范注釋的計算機程序。

這種形式化系統(tǒng)可提供驗證模型推理并提供自動反饋的環(huán)境。它們不同于現(xiàn)代 LLM 使用的「工具」，因為它們可以建模廣泛命題的真與假，并且還是可證明的。此類系統(tǒng)提供的反饋可以緩解數(shù)據(jù)稀缺問題；此外，此類系統(tǒng)還可以進行嚴格的測試時間檢查，以抵抗幻覺。

相比之下，非形式化數(shù)學是指教科書、研究論文和在線數(shù)學論壇中常見的數(shù)學文本。非形式化數(shù)學會將自然語言與符號（例如 LATEX）交織在一起，但這些符號沒有自我包含的形式語義，而是依靠非形式文本來傳達其含義的重要部分。

AlphaProof 和 AlphaGeometry 是這一想法成功的兩個突出例子。在此之前，很多研究者嘗試過使用 LLM 來解決奧數(shù)級數(shù)學問題，但都失敗了。上述系統(tǒng)的關鍵區(qū)別在于原則性地使用了符號表示和證明檢查框架。其中，符號組件（AlphaProof 的 Lean、AlphaGeometry 的特定領域幾何系統(tǒng)）的作用是執(zhí)行神經(jīng)網(wǎng)絡的推理步驟并生成高質(zhì)量的合成數(shù)據(jù)，從而實現(xiàn)前所未有的數(shù)學推理能力。

AlphaProof 和 AlphaGeometry 之前，已經(jīng)有許多文獻做好了鋪墊 —— 它們探討了形式化方法和機器學習在數(shù)學任務中的協(xié)同使用。具體涉及的主題包括神經(jīng)定理證明、自動形式化（autoformalization）等。

LLM 的出現(xiàn)大大加速了這一領域的研究。例如，由于缺乏用于微調(diào)的已對齊非形式化 - 形式化對，自動形式化長期以來一直都進展緩慢。LLM 可以通過合成數(shù)據(jù)或執(zhí)行無微調(diào)自動形式化來緩解此問題。因此，人們開始認識到自動形式化在引導神經(jīng)定理證明器方面的潛力。LLM 也是定理證明的強大工具；事實上，最近已有方法利用 LLM 來預測證明步驟并修復有缺陷的證明，同時還無需基于形式化證明數(shù)據(jù)進行明確訓練。

圍繞 LLM 和形式化推理的研究基礎設施正在迅速成熟。Lean 這種用于編寫形式化證明的語言在數(shù)學家中越來越受歡迎，并催生了形式化研究數(shù)學和通用數(shù)學庫?，F(xiàn)在已有多個框架可支持 LLM 和 Lean 之間的交互。這些框架支持基于人工編寫的形式化證明提取訓練數(shù)據(jù)，以及通過與形式化環(huán)境的交互進行定理證明。

除了 Lean 之外，Coq 和 Isabelle 等證明語言的多語言基礎設施也已在構(gòu)建中 。

最后，LLM 已被用于協(xié)助人類數(shù)學家編寫形式化證明 ，這可能會啟動一個數(shù)據(jù)飛輪，其中不斷增長的人類編寫的形式化數(shù)學數(shù)據(jù)會產(chǎn)生更強大的 LLM，從而讓人可以更輕松地創(chuàng)建更多數(shù)據(jù)。

AI 在形式化數(shù)學推理方面大有機會，因而研究繁盛。AI 在形式化數(shù)學推理方面的新興機會導致了研究活動的蓬勃發(fā)展。正如最近的一項調(diào)查給出的那樣，該領域的發(fā)表文獻數(shù)量在 2023 年幾乎翻了一番，并且很可能在 2024 年再翻一番。通過將自動形式化與強化學習相結(jié)合，AlphaProof 成為第一個在 IMO 中獲得銀牌的人工智能。

該領域的進展也可直接應用于形式化驗證（formal verification） ，這是一個核心的計算機科學問題，傳統(tǒng)上一直是形式化數(shù)學最重要的應用之一。雖然形式化驗證可以得到極其穩(wěn)健和安全的軟件和硬件系統(tǒng)，但從歷史上看，除了安全性至關重要的應用之外，形式化驗證其實很少用，因為其部署成本太高。AI 可以通過自動化形式化和證明工作來大幅降低這一成本。這可能導致未來大規(guī)模生產(chǎn)的軟件和硬件系統(tǒng)比現(xiàn)在更加穩(wěn)健。

該團隊表示：「出于所有這些原因，我們相信基于 AI 的形式化數(shù)學推理已經(jīng)到達了一個轉(zhuǎn)折點，未來幾年將取得重大進展。然而，仍有大量工作要做?！?/span>

本立場論文概述了該領域在數(shù)據(jù)和算法方面面臨的難題，以及未來進步的可能路線。

AI4Math 與形式化數(shù)學推理

數(shù)學推理是 AI 領域的前沿研究方向。本節(jié)首先將介紹 AI4Math 的非形式化方法及其局限性。然后將介紹在推進 AI4Math 方面，形式化數(shù)學推理是一條有希望的道路。這一節(jié)涵蓋的內(nèi)容包括：

當前最佳的數(shù)學 LLM 以及它們的局限性，目前的難題包括數(shù)據(jù)稀缺、缺乏驗證正確性的手段。

用于形式化數(shù)學推理的 AI：這一節(jié)將介紹從非形式化到形式化的轉(zhuǎn)向、證明助理和 Lean 等。

數(shù)學 AI 的其它方向：AI4Math 范圍很廣，還包含其它許多研究方向，比如使用神經(jīng)網(wǎng)絡來近似函數(shù)等等。

用于形式化數(shù)學推理的 AI 的最新進展

AI 已在形式數(shù)學推理方面取得了實質(zhì)性進展。本節(jié)首先將討論兩個關鍵任務的進展：自動形式化和定理證明。然后將抽樣兩個相鄰領域 —— 自然語言和代碼生成 —— 它們可受益于形式化方法實現(xiàn)的可驗證推理。

在自動形式化方面，本文介紹了基于規(guī)則的自動形式化、基于神經(jīng)和 LLM 的自動形式化、自動形式化的應用。

在神經(jīng)定理證明方面，本文介紹了專家迭代、從錯誤中學習、非正式證明草圖、庫學習、前提選擇和檢索等主題。

此外，這一節(jié)還介紹了自然語言中的驗證推理、形式系統(tǒng)驗證和驗證生成。

挑戰(zhàn)與未來的方向

這一節(jié)，該團隊分享了幾個仍待解決的挑戰(zhàn)和有希望的研究方向，包括形式化數(shù)學推理的數(shù)據(jù)和算法、協(xié)助人類數(shù)學家和證明工程師的 AI 工具，以及集成 AI 和形式化方法來生成可驗證代碼。

數(shù)據(jù)

數(shù)據(jù)稀缺是首要問題。潛在的解決方案包括:

• 從教科書、論文和講義中自動形式化非形式化數(shù)學內(nèi)容
• 基于數(shù)學公理生成合成的猜想和證明
• 從不同的證明框架和代碼等數(shù)據(jù)豐富的領域遷移知識

算法

在這個方面，又有許多亟待解決的問題，該團隊也提出了一些解決的設想：

問題 1：如何讓 AI 能夠自動地將非形式化的內(nèi)容轉(zhuǎn)換成形式化的數(shù)學語言？

• 建立自動形式化語句的評估指標
• 將形式化過程分解為小步驟
• 加強與形式系統(tǒng)的交互

問題 2：如何改進數(shù)學推理的模型架構(gòu)？

• 增強多步推理、長文本處理、抽象和分層規(guī)劃能力
• 通過合成基準診斷推理失敗之處
• 利用檢索和搜索等推理技術(shù)輔助模型

問題 3：如何有效地搜索證明？

• 對搜索進行擴展以利用更多的測試時間計算；
• 對模型、搜索算法和超參數(shù)進行系統(tǒng)性評估；
• 用于評估證明目標并為其設定優(yōu)先級的價值模型。

問題 4：如何利用定理證明中的層次結(jié)構(gòu)？

• 將大型、高級證明目標逐步分解為較小的目標。

問題 5：如何學習數(shù)學抽象？

• 學習在成熟的證明助手中構(gòu)建新的定義、引理和策略。

問題 6：如何利用現(xiàn)有的數(shù)學知識？

• 為形式數(shù)學推理量身定制的檢索器；
• 處理動態(tài)增長的知識庫。

問題 7：如何協(xié)調(diào)專家方法和通用方法？

• 識別跨領域聯(lián)系的通用方法；
• 針對各個領域的有效性的專家方法以及與數(shù)學家合作的專家方法；
• 將通用方法和專家方法結(jié)合起來，例如為 LLM 配備特定領域的工具。

用于輔助人類數(shù)學家的工具

這方面的主要問題是：AI 如何更好地協(xié)助人類研究形式化數(shù)學？

這個方面的難題和潛在研究方向包括：

• 資源、激勵措施和工程開發(fā)，以提高可用性和用戶友好性；
• 研究數(shù)學家如何使用形式化工具的行為；
• 支持大規(guī)模分布式協(xié)作的工具。

形式驗證和已驗證生成

這方面的主要問題是：AI 如何輔助人類開發(fā)正確和安全的軟件？

這個方面的難題和潛在研究方向包括：

• 將形式化方法納入 AI 輔助的系統(tǒng)設計和實現(xiàn)中；
• 增強 AI 進行形式化軟件和硬件驗證的能力；
• 將基于 AI 的生成與形式化驗證結(jié)合起來。

評估標準

在解決問題的過程中，一個關鍵問題逐漸浮現(xiàn)：如何有效衡量進展？

受自動駕駛汽車自動化等級的啟發(fā)，該團隊提出了一個評估 AI 數(shù)學推理能力的分級框架。他們強調(diào)，在這個新興領域還需要建立更多新的基準和評估方法。

定理證明能力

目前，AI 在形式數(shù)學領域的主要工作集中在自動定理證明上。像 Lean 這樣的形式系統(tǒng)提供了巨大優(yōu)勢 - 一旦找到證明，即使人可能沒完全理解，就能保證其正確性。

研究團隊根據(jù)表 1 給出了 AI 形式定理證明的分級基準。

在最基礎的 0 級水平，AI 能夠識別正確的形式證明。

到了 1 級，AI 系統(tǒng)可以提供潛在有用的數(shù)據(jù)，但還不能寫出證明。

2 級及以上的系統(tǒng)可以生成完整或部分證明。人類專家設計和編寫的固定證明策略和規(guī)則，AI 按照這些預設的策略執(zhí)行證明過程。

在 3 級水平，AI 系統(tǒng)能夠在一般領域自動證明定理，但仍局限于簡單定理。

4 級系統(tǒng)應該能夠自主規(guī)劃和執(zhí)行形式化項目，分解大型結(jié)果，提出新的定義和定理，并在探索的過程中嘗試不同的解決方案。

5 級則意味著系統(tǒng)能夠解決超出人類水平的問題。

自然語言推理驗證能力

研究團隊首先提出了一個問題：如何在不完全形式化的情況下實現(xiàn)嚴謹?shù)耐评恚?/span>

他們發(fā)現(xiàn)，讓 AI 在形式系統(tǒng)和自然語言之間切換是一個很有前景的方向。這樣的 AI 系統(tǒng)應該能夠進行邏輯推理、數(shù)值計算，并以嚴謹且易懂的方式生成答案。

雖然推理過程可能不是嚴格的形式化證明，但其中的部分內(nèi)容仍可以在人工的監(jiān)督下以半自動化的形式驗證。該團隊將這種能力稱為「自然語言驗證推理」，并提出了一個分級框架 (表 2)。

在 0 級水平，AI 能夠用自然語言生成逐步推理過程，但不涉及驗證。

到了 1 級，AI 系統(tǒng)在生成推理的同時具備了驗證能力，可以評估每個推理步驟的正確性。

在 2 級，AI 系統(tǒng)能夠利用外部工具，執(zhí)行單靠神經(jīng)網(wǎng)絡難以學會的計算任務。

第 3 級的 AI 系統(tǒng)將可以使用外部工具進行嚴格的邏輯推理。

在第 4 級，AI 系統(tǒng)能夠識別日常任務中的數(shù)學問題并使用嚴謹?shù)姆椒?。對其進行推理

自動形式化的能力

該團隊提出了一個自動形式化能力評估體系，評估 AI 如何在數(shù)學知識的非形式化表述和形式化表述之間自動轉(zhuǎn)換。

根據(jù)表 3，在最基礎的 0 級水平，AI 系統(tǒng)能夠存儲和檢驗形式化知識，方便人工形式化。

在第 1 級，AI 將可以為自動生成形式化的幾種草稿，并通過持續(xù)收集和存儲人類反饋來不斷改進系統(tǒng)性能。

到了第 2 級，AI 應能夠在兩者之間進行穩(wěn)定且準確的轉(zhuǎn)換，準確度接近人類水平。

第 3 級的 AI 系統(tǒng)能夠在形式化的過程中推斷出缺失餓信息，并標記出它無法補全的部分。

在第 4 級，AI 將具備遇到錯誤或?qū)Σ簧系妮斎霑r自我糾正的能力。

最后在第 5 級，該團隊預計 AI 將能夠創(chuàng)造新的數(shù)學定義，有望降低證明的復雜度。

猜想能力

研究團隊發(fā)現(xiàn)，在數(shù)學研究中，提出定理證明之前的猜想階段同樣重要。該團隊認為，AI 有望自主提出數(shù)學猜想。

根據(jù)表 4 的分級標準，0 級水平是指 AI 能夠針對特定問題或目標結(jié)果提出相關猜想。更進一步，在 1 級水平上，AI 就預計可以在給定研究領域內(nèi)自主提出猜想，而不必局限于某個具體定理了。

形式化驗證與驗證生成的結(jié)果

研究團隊最新發(fā)現(xiàn)，把 AI 應用到程序驗證和系統(tǒng)開發(fā)時，面臨的挑戰(zhàn)與數(shù)學研究有很大不同。為了更好地理解這個領域，該團隊設計了一個 4 級能力評估體系 (表 5)。

在最基礎的第 1 級，AI 已經(jīng)能夠完成一些簡單的驗證工作，比如檢查小段代碼是否正確，或者自動生成一些簡單的可驗證代碼。

到了第 2 級，AI 的能力提升到可以幫助開發(fā)團隊驗證整個項目，并且能處理更復雜的問題。

第 3 級是一個重要突破，AI 不僅能生成代碼，還能提供證明并幫助維護系統(tǒng)。

在最高的第 4 級，AI 可以幫助開發(fā)人員制定技術(shù)規(guī)范，包括自動生成規(guī)范文檔、解釋具體要求，以及幫助找出規(guī)范中的問題。