利用AI驅動的形式化證明搜尋推進數學研究
一篇新論文首次大規模評估了使用大型語言模型（LLM）生成形式化證明來解決開放數學問題的能力。最先進的智慧體以每個問題幾百美元的成本，自主解決了353個開放Erdős問題中的9個，並驗證了492個OEIS猜想中的44個，目前已部署在組合學、最佳化、圖論、代數幾何和量子光學等多個領域。研究表明AI輔助形式化證明搜尋在數學研究中具有巨大潛力。
文章情報
要點
- 首次大規模評估LLM生成形式化證明解決開放數學問題的能力
- 最先進智慧體以每問題數百美元的成本解決了9個Erdős問題
- 智慧體還驗證了44個OEIS猜想，並應用於多個數學領域
- 研究表明AI輔助形式化證明搜尋在數學研究中的潛力
為什麼重要
這條新聞值得關注，因為首次大規模評估LLM生成形式化證明解決開放數學問題的能力。
技術影響
可能影響模型選型、推理成本、產品能力和評測基準。
大型語言模型（LLM）在數學推理方面日益出色，但其不可靠性限制了其在數學研究中的實用性。一種緩解方法是利用LLM生成形式化證明，例如在Lean語言中。近期一篇題為《利用AI驅動的形式化證明搜尋推進數學研究》的論文首次大規模評估了這種方法解決開放問題的能力。
該研究團隊設計了一種智慧體，它交替使用LLM生成證明和基於Lean的驗證。最先進的智慧體在353個開放Erdős問題中自主解決了9個，每個問題的成本僅為幾百美元。此外，該智慧體還成功證明了492個OEIS猜想中的44個。目前，這一方法已部署在組合學、最佳化、圖論、代數幾何和量子光學等研究領域。
論文還比較了不同智慧體設計的效果。一個基本版本僅透過交替生成和驗證也能解決部分Erdős問題，但在最困難的問題上成本更高。這些發現展示了AI輔助形式化證明搜尋的強大能力，並揭示了實現這一能力的關鍵智慧體設計要素。
該研究為數學研究開闢了新途徑，使AI能夠協助數學家探索開放問題，並有望在未來加速數學發現的程序。論文由George Tsoukalas等20位作者共同完成，於2026年5月21日提交至arXiv，主題為人工智慧（cs.AI）。研究不僅證明了AI在數學證明中的可行性，還強調了成本效益和設計選擇的重要性。隨著LLM技術的進步和推理成本的降低，AI輔助證明搜尋有望成為數學研究的常規工具，幫助解決更多長期困擾數學家的難題。