數(shù)學(xué)將成為第一門借助AI實現(xiàn)重大突破的學(xué)科？

去年 2 月份，DeepMind 發(fā)布了編程輔助利器 AlphaCode。它使用人工智能技術(shù)來幫助程序員更快地編寫代碼，可以自動完成代碼、提供代碼建議并檢查錯誤，從而提高編程效率。AlphaCode 的問世意味著 AI 在解決現(xiàn)實世界問題的道路上又邁出了一大步。

巧合的是，在同一天，OpenAI 也展示了一項重要成果：他們開發(fā)的神經(jīng)定理證明器成功解出了兩道國際奧數(shù)題。這一成果是在微軟打磨了多年的數(shù)學(xué) AI——Lean 的基礎(chǔ)上完成的。Lean 于 2013 年推出，數(shù)學(xué)家可以把數(shù)學(xué)公式轉(zhuǎn)換成代碼，再輸入到 Lean 中，讓程序來驗證定理是否正確。OpenAI 的成功表明，AI 不僅可以用于解決編程等應(yīng)用學(xué)科的問題，還能用來攻克數(shù)學(xué)等自然學(xué)科。

值得注意的是，這并不是 AI 研究者的「一廂情愿」。就像快速接受 AlphaCode 的軟件工程師一樣，數(shù)學(xué)家也在越來越頻繁地使用 AI，比如獲得過菲爾茨獎的陶哲軒。他甚至預(yù)言，到 2026 年，AI 將成為數(shù)學(xué)研究領(lǐng)域可信賴的合著者（co-author）。

與此同時，主攻數(shù)學(xué)問題的 AI 也在不斷發(fā)展壯大：一個名為 LeanDojo 的開放平臺提供了一套基于大型語言模型的開源定理證明器，消除了在機器學(xué)習(xí)方法用于定理證明時存在的私有代碼、數(shù)據(jù)和大量計算需求等障礙，為機器學(xué)習(xí)方法在定理證明領(lǐng)域的研究提供了便利。

「我相信，數(shù)學(xué)將成為第一門通過人工智能實現(xiàn)重大突破的學(xué)科。」在看到這些進(jìn)展之后，英偉達(dá)高級 AI 研究科學(xué)家 Jim Fan 在一篇推特中預(yù)言說。

除了以上種種進(jìn)展，Jim Fan 還列出了以下推斷依據(jù)：

• 數(shù)學(xué)可以被方便地轉(zhuǎn)化為編碼問題，字符串在其中具有重要地位，這使得數(shù)學(xué)問題可以通過人工智能工具進(jìn)行處理和分析；

• 與依賴實證結(jié)果的學(xué)科不同，數(shù)學(xué)可以通過定理證明器（如 Lean）進(jìn)行嚴(yán)格驗證；

• 與需要依賴物理實驗的學(xué)科（如生物學(xué)和醫(yī)學(xué)）不同，數(shù)學(xué)不需要進(jìn)行物理實驗，無需依賴尚未完全成熟的機器人技術(shù)或?qū)嶒炘O(shè)備。

在數(shù)學(xué)與 AI 的這場交叉之旅中，數(shù)學(xué)家和 AI 研究科學(xué)家在共同探索更多可能性。或許，陶哲軒和 Jim Fan 的預(yù)言都將加速實現(xiàn)。

在陶哲軒手里，AI 成了數(shù)學(xué)家的得力助手

「我預(yù)計，如果使用得當(dāng)，到 2026 年，AI 將成為數(shù)學(xué)研究和許多其他領(lǐng)域值得信賴的合著者。」數(shù)學(xué)家陶哲軒在前不久的一篇博客中說道。

在眾多知名數(shù)學(xué)家中，陶哲軒是較早接受并發(fā)現(xiàn) ChatGPT 這類 AI 大模型數(shù)學(xué)價值的一個。早在今年 3 月份 ChatGPT 連雞兔同籠問題都搞不定的時候，陶哲軒就給予了它肯定的態(tài)度，認(rèn)為這類大模型完全可以勝任一些輔助性質(zhì)的工作，比如幫數(shù)學(xué)研究者進(jìn)行語義搜索、生成一些提示。

在這個例子中，陶哲軒提出的問題是：「我在尋找一個關(guān)于 xx 的公式。我想這是一個經(jīng)典的定理，但我不記得名字了。你有什么印象嗎？」在這輪問答中，雖然 ChatGPT 沒能給出正確答案（庫默爾定理），但根據(jù)它給出的近似答案（Legendre 公式），我們可以結(jié)合傳統(tǒng)搜索引擎輕松找到正確答案。

沒過多久，OpenAI 就發(fā)布了數(shù)學(xué)能力顯著提升的 GPT-4。陶哲軒也一直在嘗試解鎖這一強大的 AI 工具。

在使用過程中，他總結(jié)出了一些經(jīng)驗：不要試圖讓 AI 直接回答數(shù)學(xué)問題（這樣得到的答案八成是廢話），而是讓它扮演合作者的角色，要求它提供策略建議。

按照這種提示方法，陶哲軒在 GPT-4 的幫助下成功解決了一個數(shù)學(xué)證明題（GPT4 提出了 8 種方法，其中 1 種成功解決了問題）。

陶哲軒利用 GPT-4 解決的問題。

陶哲軒為了解決上述證明題提供給 GPT-4 的 Prompt：「你好，我是一名數(shù)學(xué)教授，我希望你能扮演一位善于提出解題技巧的數(shù)學(xué)專家合作者。我正試圖回答 MathOverflow 中的以下問題……」

GPT-4 給出的部分建議。

當(dāng)然，除了這個證明題外，陶哲軒也在用 GPT-4 完成其他一些工作，包括但不限于：

• 提出問題：他將最近一些數(shù)學(xué)預(yù)印本論文的前幾頁輸入給 GPT-4，并讓其生成一些與該論文相關(guān)的問題，就像同行提出的問題一樣。這可以幫助他更好地進(jìn)行演講準(zhǔn)備。

• 回答問題：他現(xiàn)在經(jīng)常使用 GPT-4 來回答隨意和模糊的問題，以前他可能會通過精心準(zhǔn)備的搜索引擎查詢來嘗試回答這些問題；

• 輔助寫作：他曾經(jīng)讓 GPT-4 給復(fù)雜文檔提供初稿建議，以輔助寫作。

不過，陶哲軒也指出，AI 在數(shù)學(xué)等學(xué)術(shù)領(lǐng)域的廣泛應(yīng)用對出版界和教育界來說都是一個考驗：當(dāng)人工智能指導(dǎo)的研究生入門級數(shù)學(xué)論文可以在不到一天的時間內(nèi)生成時，研究期刊將如何改變其出版和引用機制？我們的研究生教育方式將如何改變？我們會積極鼓勵和訓(xùn)練學(xué)生使用這些工具嗎？對于這些問題，陶哲軒并沒有給出答案。

拿下數(shù)學(xué)定理證明，這項研究或讓陶哲軒預(yù)言早日成真

一直以來，形式化的定理證明都是機器學(xué)習(xí)的重要挑戰(zhàn)。形式化證明本質(zhì)上是一種計算機程序，但與 C++ 或 Python 中的傳統(tǒng)程序不同，證明的正確性可以用證明助手（如開頭提到的 Lean）來驗證。定理證明是代碼生成的一種特殊形式，在評估上非常嚴(yán)格，沒有讓模型產(chǎn)生幻覺的空間。

這對目前的大型語言模型（LLM）來說是有挑戰(zhàn)性的，盡管 LLM 在代碼生成方面表現(xiàn)出了優(yōu)秀的能力，但在事實性和幻覺性方面還有缺陷。

以往，對于用于定理證明的 LLM 研究面臨著許多障礙：比如，現(xiàn)有的基于 LLM 的證明器沒有一個是開源的；它們都使用私有的預(yù)訓(xùn)練數(shù)據(jù)，而且計算要求可以達(dá)到數(shù)千個 GPU 時；此外，有些基礎(chǔ)設(shè)施是依賴于為分布式訓(xùn)練和與證明助手的互動而定制的，如果沒有開源代碼，這兩者是不可能完全復(fù)現(xiàn)的。

在最近的一項研究中，來自加州理工學(xué)院、英偉達(dá)等機構(gòu)的研究者在該命題的解決進(jìn)程上走出了重要一步，提出了開放平臺 LeanDojo。

論文鏈接：https://arxiv.org/pdf/2306.15626.pdf

項目主頁：https://leandojo.org/

總體來說，該研究有如下貢獻(xiàn)：

• 首先，介紹了從 Lean 中提取數(shù)據(jù)并與之交互的工具；

• 第二，開發(fā)了第一個用于定理證明的檢索增強的語言模型 ReProver；

• 第三，為基于學(xué)習(xí)的定理證明構(gòu)建了一個具有挑戰(zhàn)性的基準(zhǔn)，并利用它來驗證 ReProver 的有效性；

• 最后，公開發(fā)布數(shù)據(jù)、模型和代碼，推動了對定理證明的 LLM 的研究。

LeanDojo 的誕生有望改變當(dāng)前現(xiàn)狀：從開源工具包、模型到基準(zhǔn)，LeanDojo 讓研究人員能夠以適度的計算成本獲得最先進(jìn)的基于 LLM 的證明器。ReProver 不依賴私人數(shù)據(jù)集，并且可以在一周內(nèi)在單個 GPU 上完成訓(xùn)練。

研究細(xì)節(jié)

Lean 是一種編程語言，既可以寫傳統(tǒng)的程序，也可以寫定理和證明。它提供了兩個機制：首先，基于具有依賴類型的函數(shù)式編程，Lean 為定義程序、數(shù)學(xué)對象、定理和證明提供了一種統(tǒng)一的語言；第二，Lean 提供了一個策略系統(tǒng)（tactic system），用于半自動地構(gòu)建機器可檢查的證明。

圖 2 展示了一個簡單的例子，以說明定理是如何在 Lean 中被形式化和證明的：

策略（tactic）的語法是相當(dāng)靈活的，可以接受參數(shù)，也可以組合成復(fù)合策略。策略可以看作是特定領(lǐng)域語言（DSL）中的程序。用戶可以通過定義新的策略來擴展 DSL。這種離散的、組合的和無界的行為空間使得定理證明對機器學(xué)習(xí)具有挑戰(zhàn)性。

另一個挑戰(zhàn)是前提的選擇。前提是對證明一個定理有用的現(xiàn)有公理或定義，被用作策略的論據(jù)。證明不能使用尚未定義的前提，也不能使用未導(dǎo)入當(dāng)前文件的前提。通常，前提是來自一個包含數(shù)十萬個現(xiàn)有定義和定理的大型數(shù)學(xué)庫，這使得人類和機器都很難在生成策略時選擇正確的前提。這是定理證明中的一個關(guān)鍵瓶頸，也是研究者希望通過檢索增強的 LLM 來解決的。

LeanDojo Benchmark

研究者使用 LeanDojo 構(gòu)建了一個包含 96,962 條從 mathlib 提取的定理 / 證明的基準(zhǔn)。該基準(zhǔn)是目前最大的以數(shù)學(xué)為重點的定理證明數(shù)據(jù)集之一，涵蓋了不同的主題，如分析、代數(shù)和幾何。

與現(xiàn)有的 Lean 數(shù)據(jù)集不同，LeanDojo Benchmark 還包含了 128,163 個前提的定義，不僅包括定理，還包括可以作為前提的其他定義，例如圖 2 中的 gcd。此外，該數(shù)據(jù)集有 212,787 個策略，其中 126,058 個策略至少有一個前提。在有前提的策略中，前提的平均數(shù)量為 2.12。

LeanDojo Benchmark 解決了兩項關(guān)鍵問題：

• 前提信息

Lean repos（例如，mathlib 或 lean-liquid）包含人寫定理 / 證明的源代碼。然而，原始代碼并不適合用于訓(xùn)練驗證器，它缺乏人類在使用 Lean 時可以獲得的運行時信息，例如證明步驟之間的中間狀態(tài)。

而 LeanDojo 可以從 Lean 的任何 GitHub repo 中提取數(shù)據(jù)，這些數(shù)據(jù)包含在原始 Lean 代碼中無法直接看到的豐富信息，包括文件依賴關(guān)系、抽象語法樹（AST）、證明狀態(tài)、策略和前提。LeanDojo Benchmark 包含細(xì)粒度的前提注釋（它們在證明中使用的位置和在庫中定義的位置），為前提選擇提供有價值的數(shù)據(jù)，也是定理證明的關(guān)鍵瓶頸。

• 具有挑戰(zhàn)性的數(shù)據(jù)分割

研究者發(fā)現(xiàn)，將定理隨機分成訓(xùn)練 / 測試的常見做法導(dǎo)致了之前論文中高估了性能。LLM 只需在訓(xùn)練期間記住類似定理的證明，就能證明看似困難的定理。

在人類編寫的 Lean 代碼中，一個常見的慣用語法是為同一數(shù)學(xué)概念的略微不同的屬性設(shè)置了一個類似的定理 / 證明塊。例如，在圖 3 中，最后兩個定理不僅看起來相似，而且有相同的證明。如果其中一個在訓(xùn)練中，模型可以通過記憶輕松證明另一個。這種捷徑使模型能夠證明看似不簡單的定理，包括那些需要前提才能證明的定理。

在 LeanDojo Benchmark 中，研究者通過設(shè)計具有挑戰(zhàn)性的數(shù)據(jù)分割 novel_premises 來緩解這個問題，它需要測試證明以使用至少一個從未在訓(xùn)練中使用過的前提。

例如，圖 3 中的最后兩個定理都使用了前提 conj_mul。如果一個定理在 novel_premises 分割的訓(xùn)練集中，另一個也必須在訓(xùn)練中。

以編程方式與 Lean 交互

LeanDojo 的另一個重要功能是以編程方式與 Lean 交互。它把 Lean 變成了一個類似健身房的環(huán)境，在這個環(huán)境中，證明器可以觀察證明狀態(tài)，運行策略來改變狀態(tài)，并接收錯誤或證明完成的反饋。這個環(huán)境對于評估 / 部署驗證器或通過 RL 訓(xùn)練證明器是不可缺少的。

下面是 LeanDojo 的主要形式，用于通過策略與 Lean 交互。Lean 同樣支持不基于策略的其他證明風(fēng)格，不過 LeanDojo 只支持策略風(fēng)格的證明。但只要有足夠的通用性，任何證明都可以轉(zhuǎn)換為策略風(fēng)格的證明。

ReProver

隨后，研究者使用 LeanDojo Benchmark 來訓(xùn)練和評估了 ReProver。其核心是一個由檢索增強的策略生成器（圖 1 底部）。

根據(jù)當(dāng)前的證明狀態(tài)，它可以檢索出少數(shù)可能有用的前提，并根據(jù)狀態(tài)和檢索出的前提的連接情況生成一個策略。在證明定理時，該模型在每一步都會生成多個策略候選者，這些候選者被用于標(biāo)準(zhǔn)的最優(yōu)搜索算法來尋找證明。

值得注意的是，ReProver 的訓(xùn)練只需要在單 GPU 上花費五天時間（120 個 GPU 時），所需的計算量大大低于之前的方法（1000 小時以上）。

此前的基于 LLM 的證明器都在數(shù)學(xué)和編碼的特定數(shù)據(jù)集上進(jìn)行預(yù)訓(xùn)練，計算成本很高而且數(shù)據(jù)集是保密的。相比之下，ReProver 避免特定領(lǐng)域的預(yù)訓(xùn)練，建立在「google/byt5-small」之上，這是一個通用的、公開可用的、相對較小的模型檢查點。

此外，ReProver 只在人類寫的策略上進(jìn)行了微調(diào)，沒有輔助數(shù)據(jù)或通過與 Lean 在線互動收集的數(shù)據(jù)。雖然這些正交方向是有價值的，但會大大增加方法的復(fù)雜性和計算要求。

在評估實驗中，ReProver 可以證明 51.4% 的定理，優(yōu)于直接生成策略而不進(jìn)行檢索的 baseline（47.5%）和另一個使用 GPT-4 以零樣本方式生成策略的 baseline（28.8%）。

研究者還在 MiniF2F 和 ProofNet 兩個數(shù)據(jù)集上測試了 ReProver。它可以在 MiniF2F 中證明 26.5% 的定理，在 ProofNet 中證明 13.8% 的定理，這幾乎能夠媲美強化學(xué)習(xí)的 SOTA 方法，且訓(xùn)練時使用的資源少得多。

此外，許多定理在 Lean 中沒有 ground- truth 證明。而 ReProver 能夠證明 65 個目前在 Lean 中沒有得到證明的定理，其中 MiniF2F 發(fā)現(xiàn)了 33 條證明，ProofNet 中發(fā)現(xiàn)了 39 條。研究者表示，ReProver 也可以作為一個有效的工具來增強 Lean 中現(xiàn)有的數(shù)學(xué)庫。

ChatGPT 插件

研究者還構(gòu)建了一個 LeanDojo ChatGPT 插件，使 ChatGPT 能夠通過與 Lean 交互來證明定理。與專門針對定理證明進(jìn)行微調(diào)的 LLM（例如 ReProver）相比，ChatGPT 可以將非形式化數(shù)學(xué)與形式化證明步驟交織在一起，類似于人類與證明助手的交互方式。它可以解釋來自 Lean 的錯誤消息，并且比專門的證明器更容易操縱。然而，由于搜索和規(guī)劃方面的弱點，在大多數(shù)情況下很難找到正確的證明。

示例如下：

a + b + c = a + c + b

Stirling’s formula

Gauss' summation formula

團隊信息

最后來認(rèn)識一下這篇文章的作者們：

論文一作楊凱峪目前是加州理工學(xué)院計算和數(shù)學(xué)科學(xué) (CMS) 系的博士后研究員 ，此前在普林斯頓大學(xué)獲得博士學(xué)位。

Alex Gu 是麻省理工學(xué)院的一名博士生，導(dǎo)師為 Armando Solar-Lezama。此前，他在麻省理工學(xué)院獲得了學(xué)士和碩士學(xué)位，擁有 Meta AI Research、Jane Street 和 pony.ai 多家公司的實習(xí)經(jīng)歷。

Peiyang Song 目前是加州大學(xué)圣巴巴拉分校（UCSB）創(chuàng)意研究學(xué)院（CCS）的計算機科學(xué)本科生。他的研究工作主要集中在兩個方向：1）神經(jīng)定理證明和自動推理，結(jié)合大型語言模型（LLMs）和交互式定理證明器（ITPs）；2）用于能源效率機器學(xué)習(xí)推理的時間邏輯。

Shixing Yu 目前是美國康奈爾大學(xué)計算機科學(xué)專業(yè)博士生，此前在德州大學(xué)奧斯汀分校獲碩士學(xué)位，本科就讀于北京大學(xué)信息科學(xué)技術(shù)學(xué)院。

參考鏈接：

https://unlocked.microsoft.com/ai-anthology/terence-tao/

https://unlocked.microsoft.com/ai-anthology/terence-tao/

THE END