當巴黎準備舉辦第33屆奧運會時，來自近110個國家的600多名學生於7月齊聚在田園詩般的英國小鎮巴斯，參加國際數學奧林匹克競賽（IMO）。他們有兩場分別為四個半小時的考試，回答來自不同數學學科的六道問題。中國學生施皓嘉以滿分的成績在個人排名中名列第一。在國家隊排名中，美國隊名列榜首。然而，本次賽事最引人注目的成果是谷歌DeepMind的兩臺機器取得的成績。DeepMind的人工智慧程式總共解決了六道題中的四道，這相當於銀牌得主的水平。這兩個程式獲得了總分42分中的28分。只有大約60名學生的得分高於這個分數，數學家和菲爾茲獎得主蒂莫西·高爾斯在X（前身為Twitter）上的一則帖子中寫道，他本人曾是該比賽的金牌得主。
為了取得如此令人印象深刻的成績，DeepMind團隊使用了兩個不同的人工智慧程式：AlphaProof和AlphaGeometry 2。前者以類似於掌握了國際象棋、將棋和圍棋的演算法的方式工作。AlphaProof使用所謂的強化學習，反覆與自身對弈，並逐步改進。這種方法可以很容易地應用於棋盤遊戲。人工智慧執行幾個步驟；如果這些步驟沒有帶來勝利，它就會受到懲罰，並學習追求其他策略。
然而，要對數學問題做同樣的事情，程式不僅必須能夠檢查它是否解決了問題，還必須驗證它為得出解決方案而採取的推理步驟是否正確。為了實現這一目標，AlphaProof使用了所謂的證明助手——演算法一步一步地檢查邏輯論證，以檢查對所提出的問題的答案是否正確。儘管證明助手已經存在了幾十年，但它們在機器學習中的應用一直受到形式語言（如Lean）中可用的數學資料量非常有限的限制，而計算機可以理解這些語言。
支援科學新聞報道
如果您喜歡這篇文章，請考慮透過以下方式支援我們屢獲殊榮的新聞報道 訂閱。透過購買訂閱，您正在幫助確保有關塑造我們當今世界的發現和想法的具有影響力的故事的未來。
另一方面，以自然語言編寫的數學問題解決方案非常豐富。網際網路上有大量人類一步一步解決的問題。因此，DeepMind團隊訓練了一個名為Gemini的大型語言模型，將一百萬個此類問題翻譯成Lean程式語言，以便證明助手可以使用它們進行訓練。“當遇到問題時，AlphaProof會生成候選解決方案，然後透過在Lean中搜索可能的證明步驟來證明或反駁它們，”開發者在DeepMind的網站上寫道。透過這樣做，AlphaProof逐漸學習哪些證明步驟是有用的，哪些是無用的，從而提高其解決更復雜問題的能力。
幾何問題也出現在IMO中，通常需要完全不同的方法。早在今年1月，DeepMind就展示了一個名為AlphaGeometry的人工智慧，它可以成功解決此類問題。為了做到這一點，專家們首先生成了大量的幾何“前提”或起點：例如，一個繪製了高線並在邊上標記了點的三角形。然後，研究人員使用所謂的“演繹引擎”來推斷三角形的進一步性質，例如哪些角重合，哪些線彼此垂直。透過將這些圖表與推匯出的性質相結合，專家們建立了一個由定理和相應的證明組成的訓練資料集。這個過程與一個大型語言模型相結合，該模型有時也使用所謂的輔助構造；該模型可能會向三角形新增另一個點，使其成為四邊形，這可以幫助解決問題。DeepMind團隊現在推出了改進版本AlphaGeometry 2，透過使用更多資料訓練模型並加快演算法速度。
為了測試他們的程式，DeepMind的研究人員讓這兩個人工智慧系統參加了今年的數學奧林匹克競賽。該團隊首先必須手動將問題翻譯成Lean。AlphaGeometry 2設法在短短19秒內正確解決了幾何問題。與此同時，AlphaProof能夠解決一個數論問題和兩個代數問題，其中包括一個只有五名人類參賽者能夠破解的問題。然而，人工智慧未能解決組合問題，這可能是因為這些問題很難翻譯成Lean等程式語言。
AlphaProof的效能很慢，完成一些問題需要超過60個小時——大大超過了學生們被分配的總共九個小時。“如果人類參賽者被允許每個問題有這麼長的時間，他們無疑會獲得更高的分數，”高爾斯在X上寫道。“然而，（i）這遠遠超出了以前的自動定理證明器所能做到的，並且（ii）隨著效率的提高，這些時間可能會縮短。”
高爾斯和另一位曾獲得金牌的數學家約瑟夫·K·邁爾斯使用與人類參與者相同的標準評估了這兩個人工智慧系統的解決方案。根據這些標準，這些程式獲得了令人印象深刻的28分，相當於銀牌。這意味著人工智慧僅以微弱差距錯失了達到金牌水平的表現，金牌水平的分數是29分或更高。
高爾斯在X上強調，人工智慧程式已經接受了相當廣泛的問題的訓練，並且這些方法不僅限於數學奧林匹克競賽。“我們可能很快就會擁有一個程式，使數學家能夠獲得各種問題的答案，”他解釋說。“我們是否已經接近數學家變得多餘的程度？這很難說。”
本文最初發表於《明鏡線上》並經許可轉載。