在最新的數學界轟動新聞中，一羣來自清華的校友們藉助 AI 的力量，成功證明了162個之前無人能解的數學定理。更厲害的是，這個名叫 LeanAgent 的智能體，竟然還攻克了陶哲軒對多項式 Freiman-Ruzsa 猜想的形式化難題!這讓我們不得不感嘆，基礎科學的研究方法可謂是被 AI 徹底改頭換面了。

衆所周知，當前的語言模型（LLM）雖然炫酷，但大多依然是靜態的，無法在線學習新知識，證明高等數學定理更是難如登天。然而，加州理工、斯坦福大學和華盛頓大學的研究團隊聯合開發的 LeanAgent，正是一個具備終身學習能力的 AI 助手，能夠不斷地學習和證明定理。

image.png

LeanAgent 通過精心設計的學習路徑來應對不同數學難度，利用動態數據庫管理源源不斷的數學知識，確保它在學習新知識時不會忘記已經掌握的技能。實驗表明，它成功從23個不同的 Lean 代碼庫中，證明了162個此前無人能解的數學定理，性能比傳統的大模型高出了整整11倍，真是令人驚歎!

這些定理涵蓋了高等數學的諸多領域，包括抽象代數和代數拓撲等棘手的問題。LeanAgent 不僅能夠從簡單概念入手，逐漸攻克複雜主題，還在穩定性和反向遷移方面展現了卓越的表現。

不過，陶哲軒的挑戰依然讓 AI 感到無奈。儘管交互式定理證明器（ITPs）如 Lean，在形式化和驗證數學證明方面發揮着重要作用，但構建這樣的證明過程往往復雜且耗時，需細緻入微的步驟和大量數學代碼庫。像 o1和 Claude 這樣的先進大模型面對非形式化證明時，也容易出現錯誤，這突顯了 LLM 在數學證明準確性和可靠性上的短板。

image.png

過去的研究嘗試了使用 LLM 生成完整證明步驟，例如 LeanDojo，就是通過訓練大模型在特定數據集上創建的定理證明器。然而，形式化定理證明的數據極爲稀缺，限制了這種方法的廣泛適用。另一項目 ReProver 則是針對 Lean 定理證明代碼庫 mathlib4優化的模型，雖然它涵蓋了超過10萬個形式化數學定理和定義，但僅限於本科數學的範圍，因此在面對更復雜問題時表現不佳。

值得注意的是，數學研究的動態性給 AI 帶來了更大挑戰。數學家們通常同時或交替處理多個項目，比如陶哲軒就同時推進多個研究領域，包括 PFR 猜想和實數對稱平均等。這些例子顯示了當前 AI 定理證明方法的一個關鍵不足:缺乏一個能夠在不同數學領域自適應學習和提升的 AI 系統，尤其是在 Lean 數據有限的情況下。

image.png

正因如此，LeanDojo 的團隊創造了 LeanAgent，這是一個全新的終身學習框架，旨在解決上述難題。LeanAgent 的工作流程包括推導定理複雜度，以制定學習課程，通過漸進訓練在學習過程中平衡穩定性與靈活性，並利用最佳優先樹搜索來尋找尚未被證明的定理。

LeanAgent 與任何大模型結合使用，通過 “檢索” 來提升其泛化能力。它的創新之處在於使用自定義動態數據庫來管理不斷擴展的數學知識，以及基於 Lean 證明結構的課程學習策略，助力學習更復雜的數學內容。

image.png

在應對 AI 的災難性遺忘問題上，研究者採用了一種漸進訓練的方法，使 LeanAgent 能夠持續適應新的數學知識，同時不忘記先前的學習。這一過程涉及在每個新的數據集上進行增量訓練，確保穩定性與靈活性達到最佳平衡。

通過這種漸進訓練，LeanAgent 在證明定理方面的表現卓越，成功證明了162個尚未被人類解答的難題，尤其在抽象代數和代數拓撲的挑戰性定理上大展身手。其在證明新定理的能力上比靜態的 ReProver 高出11倍，且保持了對已知定理的證明能力。

LeanAgent 在定理證明的過程中表現出了漸進學習的特徵，從簡單的定理逐漸過渡到更復雜的定理，證明了它在數學知識掌握上的深度。例如，它證明了與羣論和環論相關的基礎代數結構定理，展現出對數學的深刻理解。總的來看，LeanAgent 以其強大的持續學習和改進能力，爲數學界帶來了令人興奮的前景!

論文地址：https://arxiv.org/pdf/2410.06209