人工智慧（AI）正從解決數學競賽題邁向探索科研級數學問題。Google旗下“深度思維”公司團隊開發並測試了一種名為AlphaProof Nexus的AI框架，其能自主搜尋數學證明，並利用電腦程序驗證推理過程。在測試中，該系統解決了9個此前未解決的厄多斯問題，其中兩個已懸而未決超過50年。此外，該系統還解決了44個開放數學猜想。相關成果發表於最新一期《科學》雜誌。同期評論文章指出，AI用於科研級數學的時代已經到來。
近年來，AI解決數學問題的能力不斷提升。然而，競賽數學主要考查已有方法的靈活運用，大型語言模型還容易產生邏輯錯誤，難以直接用於嚴謹的數學研究。
為解決這一問題，團隊讓AI使用Lean等形式化證明工具。所謂“形式化”，就是用足夠精確的語言完整寫出數學證明，讓電腦能夠逐步檢查每一步推理是否符合數學公理和規則。團隊在這裡使用的Lean證明助手，能夠自動驗證證明的邏輯正確性，幫助發現推理中的錯誤。
此次開發的AlphaProof Nexus能夠根據Lean編譯器的反饋不斷調整證明。其功能更完善的版本還可利用進化演算法協調多個子智能體，並呼叫“深度思維”的AlphaProof作為專門的證明工具。
團隊用該系統挑戰了以數學家保羅·厄多斯命名的一系列開放問題。在353個嘗試解決的問題中，系統攻克了9個，其中兩個此前已超過50年沒有得到解決。
此外，該系統解決了《整數數列線上百科全書》492個開放猜想中的44個，同時處理了代數幾何、最佳化、量子光學和圖論等領域的多個科研級問題。
團隊還發現，最基礎版本的智能體同樣解決了上述9個厄多斯問題，只是在處理較難問題時需要更多計算資源。該版本主要依靠商業化大型語言模型和Lean證明助手。這一結果表明，隨著通用大模型能力提升，通用AI智能體也有望參與科研級數學探索。
不過，部分數學家擔心，大規模使用AI可能削弱人們探索數學問題和理解證明過程的動力。團隊認為，即使AI未能完成證明，其嘗試也可能幫助數學家更好地理解問題、發現新思路。(科技日報)