數學家透過提出猜想並用定理證明它們來探索想法。幾個世紀以來，他們小心翼翼地逐行構建這些證明，大多數數學研究人員今天仍然這樣工作。但人工智慧正準備從根本上改變這一過程。被稱為“副駕駛”的人工智慧助手開始幫助數學家開發證明——這真有可能在未來讓人類回答一些目前超出我們思維能力範圍的問題。
加州理工學院正在開發一種很有前景的人工智慧副駕駛。它可以自動提出證明中的下一步，並幫助完成中間數學目標，從而幫助構建更大步驟之間邏輯上的連線組織。“如果我正在開發一個證明，這個新的副駕駛會為我提供多個前進的建議，”加州理工學院計算和數學科學教授阿尼瑪什裡·阿南德庫馬爾說。阿南德庫馬爾和她的團隊在一篇最近的預印本論文中介紹了這款人工智慧副駕駛，該論文尚未經過同行評審。她說，至關重要的是，這些建議“都將是正確的”。
這款副駕駛是一個大型語言模型（LLM），與 OpenAI 的 ChatGPT 和 Google 的 Gemini 背後的機器學習系統是同一種類型。雖然它的訓練方式不同，但它也類似於 Google 的 AlphaProof 和 AlphaGeometry 2 的技術——這兩者都在今年的國際數學奧林匹克競賽（IMO）中生成了達到銀牌水平的複雜數學證明，參賽者是世界上最優秀的高中生。儘管 LLM 可以生成在技術意義上是“胡說八道”的東西，但副駕駛的錯誤建議會受到檢查和拒絕。在加州理工學院的副駕駛案例中，這要歸功於人工智慧執行的軟體 Lean，該軟體使用嚴格的數學邏輯來篩選有效陳述。
支援科學新聞報道
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞報道 訂閱。透過購買訂閱，您正在幫助確保有關塑造我們當今世界的發現和想法的具有影響力的故事的未來。
程式碼證明
在過去幾年中，Lean 越來越受到一小部分但不斷增長的使用者群的歡迎。這款開源軟體允許數學家透過編碼輸入他們的數學，這個過程被稱為形式化。這樣做有什麼好處？它永遠不會出錯。在 Lean 和其他證明助手應用程式中，軟體會自動檢查數學陳述的準確性。這與傳統的、所謂的非正式數學截然不同，在非正式數學中，審稿人和同事會費力地稽核一頁又一頁的此類陳述。這個過程容易出現人為錯誤，並且會遺漏錯誤。
如果您正在 Caltech 副駕駛的幫助下編寫證明，您可以單擊一個按鈕來請求新的 Lean 程式語言行，以表示您正在使用的數學。螢幕右側將出現幾個選項，阿南德庫馬爾稱之為“策略建議”；然後您只需選擇看起來最合適的選項。如果您的證明朝著具有明顯或眾所周知的中間結論的方向發展，副駕駛還可以建議如何完成該軌跡。
洛桑瑞士聯邦理工學院和倫敦帝國學院的純數學教授馬丁·海雷爾說，“Lean 沒有信任問題”，因為該軟體會檢查工作。儘管如此，許多學者尚未採用它。“它很難使用，因為你必須將所有數學都輸入為程式碼，”海雷爾說。他指出，用 Lean 編碼需要輸入在撰寫論文時會被省略的細節，因此可能需要多頁程式碼來顯示不言自明或顯而易見的內容。
但海雷爾沒有參與 Caltech 專案，他認為人工智慧副駕駛最終會消除所有這些繁瑣的工作。“一旦你提出了一個對大多數數學家來說顯而易見的陳述，LLM 應該能夠生成它的程式碼，”他說，並補充說，這種更快的流程“可能會吸引新一代數學家使用 Lean”。
阿南德庫馬爾也預測，更多的研究人員將接受形式化的人工智慧輔助數學。“今天，當我與年輕的數學家甚至職業生涯早期的本科生交談時，我看到他們熟悉這些人工智慧系統，”她說。“他們會不惜一切代價讓工作更快更容易，以獲得競爭優勢。”
數學變革
在國際數學界以有意義的方式採用人工智慧工具之前，這些平臺需要變得更加強大。憑藉今年國際數學奧林匹克競賽的銀牌標準，谷歌的 AlphaProof 和 AlphaGeometry 2 已經顯示出卓越的成果。但它們尚未達到研究數學家在複雜證明方面需要協助的水平；在這方面，人類仍然是更有能力的數學家。
然而，谷歌 DeepMind 強化學習副總裁大衛·西爾弗說，“很快就會有系統達到那個水平”。“我認為這基本上會將人類數學家提升到一個更高的水平，讓他們能夠以更高的水平進行操作和思考想法。”他說，數學正開始發生轉變，就像電子計算器發明時一樣。“在計算器出現之前，有大量的數學運算非常費力，需要花費大量精力，”他說。“我認為我們現在正處於證明的階段，在未來，我們將看到非常複雜的證明被人工智慧自動解決。”
透過人工智慧協作
採用人工智慧副駕駛也將改變數學家彼此合作的方式。通常，他們單獨或小組運作。受信任的同事會逐個評估他們的證明。但形式化的人工智慧助手可以使更大規模的人類合作者能夠透過將最大的問題分解為子問題來解決它們。每個部分都將被分批分配給不同的專家人工智慧-人類夥伴關係團隊來解決。“數學被認為是一項非常孤獨的事業，尤其是在大眾媒體中，但現在看來人工智慧將成為數學家之間協作的推動者，”阿南德庫馬爾說。
數學家普遍樂觀地認為，人工智慧副駕駛很快將為人類專家提供助力，使他們能夠將時間投入到更復雜和更困難的問題中。例如，在未來幾年，人工智慧-人類夥伴關係可能會嘗試解決臭名昭著的千禧年難題——甚至可能是像P 與 NP 這樣具有挑戰性的問題，這是一個理論計算機科學中長期存在的問題，它詢問每個其解決方案可以快速驗證的問題是否也可以快速解決。
“這就是我們很快將發現自己所處的位置，”西爾弗在考慮解決此類問題的概念時說。“像‘P 與 NP’這樣複雜的問題——或者像它一樣困難的問題——遠遠超出了我們今天的水平，甚至不知道如何開始，”他說。“但我可以想象，也許在三年左右的時間裡，我們可能會朝著類似的方向前進。”