編輯：編輯部
【新智元導讀】用大語言模型定理證明，加州理工華人一作最新研究可能改變數學未來。
大語言模型，可以用來證明數學定理了！
「數學天才」陶哲軒曾在一篇部落格中稱，2026年，AI将與搜尋和符号數學工具相結合，成為數學研究中值得信賴的合著者。
這個預言，如今已經成真！
加州理工、英偉達、MIT等機構的學者，建構了一個基于開源LLM的定理證明器。
而這篇論文，或許将改變數學的未來。
項目位址：https://leandojo.org/
在此，研究人員提出一個開源平台LeanDojo，提供工具包、基準和模型，為LLM創造了一種定理證明的互動式環境。
數學：首個見證AI重大突破的領域
論文一作楊凱峪表示，公式證明是計算機程式，其正确性可以被驗證。
最重要的是，這項研究為解決LLM，在事實性和幻覺方面的缺陷開辟了一條新途徑。
因為，定理證明是一種具有嚴格評價的代碼生成形式，根本沒有讓模型産生幻覺的空間。
英偉達首席科學家Jim Fan激動轉發稱：見證人工智能實作重大突破的第一個學科，很可能就是數學！
他說：每個人都該讀一讀數學家陶哲軒的部落格。在此部落格中，陶預測在2026年，AI将與搜尋和符号數學工具相結合，成為數學研究中值得信賴的合著者。
為什麼AI的第一個重大突破會在數學？理由如下——
- 數學可以友善地表示為編碼問題
- 可以通過Lean這樣的定理證明器進行嚴格的驗證，而不是依賴經驗結果
- 不需要像生物學和醫學這樣的實體實驗，機器人技術的發展還有待進步
GPT擅長編碼，Lean是公式數學的編碼語言，還不會出現幻覺。
人工智能數學co-pilots來了。發現新定理的全自動人工智能數學家就是下一個！
有網友稱，是以陶哲軒可以被解雇，很容易被取代，不是嗎？
LeanDojo究竟有多強？
LeanDojo：定理證明互動式環境
機器學習，特别是大型語言模型，在使用證明助手Lean證明公式定理方面顯示出廣闊的前景。
LeanDojo其主要特點包括：
- 提供了用于資料提取和與Lean互動的工具
- 證明中的前提（現有定理）的細粒度标注：使用和定義這些前提的位置
- LeanDojo Benchmark：97000個人工編寫的定理/證明，用于開發定理證明的機器學習模型
- ReProver（檢索增強證明器）：第一個基于LLM的證明器，專門增強了前提選擇（Premise Selection）的檢索
Lean是一個在數學家中非常受歡迎的證明助手工具。
研究團隊針對Lean進行了加工和改進，開發出了LeanDojo。它可以從Lean中提煉出人類撰寫的證明過程，形成一個資料集。
進而可以通過與Lean的證明環境互動，使得這個訓練出來的模型可以用來證明定理。
LeanDojo的工作流程和原理大緻如下圖所示：
頂部右邊：LeanDojo從Lean中提驗證明到資料庫中，用來訓練機器學習模型。
這個流程也可以通過和Lean的證明環境進行互動後讓訓練好的模型來證明定理。
頂部左邊：這是Lean定理
的證明樹。在這裡gcd是最大公約數的意思。
在證明定理時，我們從原始定理作為初始狀态（根）開始，并重複應用政策（邊）将狀态分解為更簡單的子狀态，直到所有狀态都得到解決（葉節點處）。
政策可能依賴于大型數學庫中定義的諸如 mod_self 和 gcd_zero_left 之類的前提。
例如，mod_self 是證明中用于簡化目标的現有定理 ：
底部：隻要給定一個狀态，Reprover模型就能從數學庫中檢索前提，這些前提與狀态連接配接起來，輸入到一個作為編碼器和解碼器的Transformer中以生成下一個政策。
Benchmarks 基準測試
- LeanDojo Benchmark：從mathlib中提取的96,962個定理/證明、212,787個政策和128,163個前提。
- LeanDojo Benchmark 4：從mathlib4中提取的91,766個定理/證明和177,349個政策。前提資訊将很快提供。
LeanDojo可以從Lean中的任何GitHub存儲庫中提取資料（支援Lean 3和Lean 4）。
這些資料包含原始Lean代碼中不直接可見的豐富資訊，包括檔案依賴項、抽象文法樹 (AST)、證明狀态、政策和前提。
主要特征 1：前提資訊
LeanDojo Benchmark包含前提的細粒度标注（在證明中使用它們以及在庫中定義它們），為前提選擇（定理證明中的關鍵瓶頸）提供有價值的資料。
主要特征 2：具有挑戰性的資料分割
将定理随機分割到訓練/測試中會導緻高估模型性能。大語言模型可以通過在訓練期間記住類似定理的證明，就可以證明看似困難的定理。
研究人員通過設計具有挑戰性的資料分割來緩解這個問題，要求模型基于從未在訓練中使用的創新性前提來泛化到定理。
與Lean産生互動
如上圖所示，LeanDojo将Lean變成了一個類似體育館的環境，數學家可以在其中觀察證明狀态，運作政策來改變狀态，并接收有關錯誤或證明完成的回報。
這樣的一個環境對于評估/部署證明器或通過強化學習進行訓練是必不可少的。
實驗評估
研究人員使用LeanDojo Benchmark來訓練和評估ReProver。
下圖展示了10分鐘内證明的定理的百分比。每一列代表不同的資料分割。
ReProver的性能優于Lean内置的證明自動化政策（tidy），提供了一個無需檢索即可直接生成政策的測試基準。
研究人員采用的另一個基準是使用GPT-4以零樣本方式生成政策。
發現新證明&發現公式錯誤
研究人員采用在miniF2F和FroofNet中的定理來評估ReProver。
他們發現miniF2F中有33個證明，ProffNet中有39個證明在Lean中是不存在的。
與此同時，最新研究還發現了ProofNet定理陳述公式中的多個錯誤。
詳見：https://github.com/zhangir-azerbayev/ProofNet/pull/14
ChatGPT插件
研究人員還建構了一個LeanDojo的ChatGPT插件，使ChatGPT能夠通過與Lean互動來證明定理。
他們具體在三種數學公式上進行了嘗試，包括a+b+c=a+c+b，斯特林公式（Stirling's formula），以及高斯求和公式（Gauss' summation formula）。
結果發現，專業的定力證明LLM（ReProver）相比，ChatGPT可以将非正式數學與正式證明步驟交叉在一起，類似人類與證明助手的互動方式。
它甚至可以解釋Lean的錯誤資訊，并且比專業證明器更容易控制（通過提示工程）。
然而，由于搜尋和規劃方面的弱點，它在多數情況下很難找到正确的證明。
GitHub上，開發者給出使用示範方法示例：
插件安裝成功後，你可以讓ChatGPT證明定理，隻需告訴它定理的名稱和定義。比如：
I want you to prove a theorem in Lean. The theorem's name is `hello_world`, and it is defined in the file `src/example.lean` in `https://github.com/yangky11/lean-example`. Please explain the theorem to me, lay out a high-level proof plan, and then try various tactics to prove the theorem. 初始化證明搜尋可能需要一些時間。
你可以用提示來控制ChatGPT的行為。例如，在嘗試任何測術之前，你可以要求它「産生一個進階證明計劃」。
網友評論
這個發現是AI在數學領域的最佳應用，找到了一個非常現實的角度讓AI能為數學研究做出了貢獻。
我們離正式證明所有數學公式的偉大目标又進了一步！
數學證明真的是為大語言模型量身定制地任務，因為結果的有效性是可以完全確定的。
網友們除了狂贊這個項目對于數學研究的加速，紛紛腦洞大開，幻想了很多未來的可能性。
Cue了馬老闆，數學的飛速發展将使得人類進入一個科幻小說中才存在的世界。
因為數學是科學之母，數學的飛速發展将導緻所有的自然科學不斷加速。
數學将成為第一個看到人工智能實作重大突破的科學學科，這确實是有道理的。
作者介紹
Kaiyu Yang（楊凱峪）
楊凱峪是加州理工學院計算+數學科學（CMS）系的博士後研究員，導師是Anima Anandkumar。他曾在普林斯頓大學獲得了博士學位，導師是Jia Deng，還與Olga Russakovsky和陳丹琦一起工作。
他的研究重點是神經符号人工智能，旨在使機器學習能夠進行符号推理。
楊凱峪是兩個角度實作目标：（1）将機器學習應用于符号推理任務，如形式邏輯或自然語言中的數學推理和定理證明；（2）将符号元件引入機器學習模型，使其更具可解釋性、可驗證性和資料高效。
目前，他正在研究能夠了解和推理數學的人工智能。數學推理是人類智能的一個重要裡程碑，它有可能改變科學和工程中的許多重要問題，比如解決偏微分方程和公式驗證。
Alex Gu
Alex Gu是麻省理工學院的博士生，導師是Armando Solar-Lezama。在Armando和Jacob Andreas的指導下，他還在麻省理工學院獲得了學士和碩士學位。
Alex Gu曾在Meta AI Research、Jane Street和pony.ai實習。
Peiyang Song
PeiYang Song是加州大學聖巴巴拉分校（UCSB）創意研究學院（CCS）榮譽計算機科學學士候選人。
研究興趣包括機器學習及其在自然語言處理、計算機視覺中的應用，以及它與計算機架構、程式設計語言等的交叉。
他最近的研究工作主要在兩個方向：1）結合大語言模型（LLM）和互動式定理證明器（ITP）的神經定理證明和自動推理；2）節能機器學習推理的時序邏輯。
參考資料：
https://leandojo.org/
https://twitter.com/KaiyuYang4/status/1673882824158613504
https://twitter.com/DrJimFan/status/1674083328478318594