從求解器到研究：大型語言模型驅動的前沿形式化數學
本文是一篇立場論文，系統回顧了人工智能數學（AI4Math）領域的最新進展，特別是大型語言模型（LLM）驅動的定理證明器在形式化證明生成方面取得的成功。然而，現有系統在應對前沿研究數學（如發現新定理或解決開放猜想）方面存在根本性限制。作者主張AI4Math系統應從預定義問題求解器轉向能進行嚴格形式化數學推理的研究代理，並指出了現有系統在數據集、關係結構、數學探索、工具生態和人機協作等方面的核心侷限性，為未來AI4Math的發展提出了戰略路線圖。
近年來，人工智能數學（AI4Math）領域取得了顯著進展，尤其是大型語言模型（LLM）驅動的定理證明器在形式化證明生成方面表現突出。這些系統通過交互式定理證明（ITP）語言，能夠為定義明確的數學問題自動生成形式化證明，標誌着AI在數學推理領域的重大突破。然而，這些成就主要集中在已有明確求解路徑的問題上，當面臨前沿研究數學——如發現全新定理或解決懸而未決的猜想——時，現有系統往往力不從心。這類任務通常具有開放性、説明不充分、涉及多層次抽象的特點，遠超當前系統的能力範圍。
在一篇發表於arXiv的立場論文中，由Eric Jiang等19位作者組成的團隊系統審視了AI4Math的現狀，並提出了一個關鍵論點：AI4Math的下一次飛躍需要從預定義的問題求解器轉向真正的研究代理，後者能夠以前沿數學挑戰為目標，進行嚴謹的形式化數學推理。論文首先回顧了該領域的三大核心組成部分：數據集、自動形式化和證明合成。數據集方面，現有基準如MiniF2F和ProofNet等主要針對已知競賽或教科書問題，缺乏涵蓋前沿研究的資源。自動形式化旨在將非形式化數學語句轉化為機器可驗證的ITP代碼，但當前方法在複雜語境下可靠性不足。證明合成技術雖然藉助LLM取得了進展，但生成的證明長度有限，難以處理需要深層探索的定理。
更關鍵的是，論文識別了現有系統在作為數學研究代理時的五大核心侷限。第一，數據集問題：現有數據集規模小、領域窄，無法反映數學研究的多樣性和深度。第二，關係結構缺失：數學知識以複雜的網絡形式存在，但當前系統缺乏對定理間邏輯關係的結構化理解。第三，數學探索能力不足：研究過程包含大量試探性和創造性步驟，而現有系統僅能按預設路徑搜索。第四，工具生態系統不完善：缺乏與現有數學軟件（如計算機代數系統）及人類協作的科學工作流集成。第五，人機協作機制薄弱：AI應輔助而非替代數學家，但目前交互範式有限。
基於以上分析，作者勾勒了一個戰略路線圖，強調未來AI4Math系統需在數據構建（如創建大規模關係型數學知識庫）、推理架構（如引入抽象與類比機制）、工具集成（如無縫對接證明助手與計算工具）以及交互設計（如自然語言與形式語言混合界面）等方面取得突破。這篇論文不僅是對現有技術的批評性總結，也為AI4Math領域指明瞭一個雄心勃勃的發展方向。