Google DeepMind 的人工智慧在今年的國際數學奧林匹克競賽 (IMO) 上獲得銀牌，這是人工智慧首次登上頒獎台。

IMO 被認為是世界上最負盛名的年輕數學家競賽。正確回答測驗問題需要人工智慧系統通常缺乏的數學能力。

一月份，Google DeepMind 展示了 AlphaGeometry，這是一個人工智慧系統，可以像人類一樣回答一些 IMO 幾何問題。然而，這不是來自現場比賽，也無法回答其他數學學科的問題，例如數論、代數和組合學，而這是贏得 IMO 獎牌所必需的。

GoogleDeepMind現已發布了一款名為AlphaProof的新AI，它可以解決更廣泛的數學問題，以及AlphaGeometry的改進版本，可以解決更多幾何問題。

當團隊在今年的 IMO 問題上同時測試這兩個系統時，他們正確回答了 6 個問題中的 4 個問題，在滿分 42 分中得到了 28 分。這足以贏得一枚銀牌，僅比今年的金牌門檻低一分。

上週在英國巴斯舉行的比賽中，58 名參賽者獲得金牌，123 名參賽者獲得銀牌。

IMO 主席 Gregor Dolinar 表示：“我們都非常清楚，人工智慧最終會比人類更好地解決大多數數學問題，但人工智慧進步的速度令人驚嘆。” “幾天前僅以一分之差錯過 IMO 2024 金牌確實令人印象深刻。”

在一次新聞發布會上，幫助標記AlphaProof 答案的劍橋大學蒂莫西·高爾斯(Timothy Gowers) 表示，人工智能的表現令人驚訝，它似乎找到了“神奇鑰匙”，以與人類類似的方式回答問題。高爾斯說：“我認為這些神奇的鑰匙可能有點超出了它的能力，所以在一兩次程序確實找到這些鑰匙的情況下，我感到非常驚訝。”

AlphaProof 的工作原理與 Google DeepMind 之前的人工智慧類似，可以在國際象棋和圍棋方面擊敗最優秀的人類。所有這些人工智慧都依賴一種稱為強化學習的試誤方法，系統透過多次嘗試找到自己的方法來解決問題。然而，這種方法需要用人工智慧可以理解和驗證的語言編寫大量問題，而大多數類似 IMO 的問題都是用英語編寫的。

為了解決這個問題，DeepMind 的Thomas Hubert 和他的同事使用了Google 的Gemini AI（一種類似於為ChatGPT 提供支援的語言模型）將這些問題轉化為一種名為Lean 的程式語言，以便AI 能夠學習如何解決它們。

休伯特在新聞發布會上說：“一開始，它可能能夠解決最簡單的問題，並從解決這些更簡單的問題中學習，以解決越來越難的問題。”它還以精益方式生成答案，因此可以立即驗證它們是否正確。

雖然 AlphaProof 的性能令人印象深刻，但它的運行速度很慢，需要長達三天的時間才能找到一些解決方案，而不是競爭對手允許的每三個問題 4.5 小時的時間。它也未能回答關於組合學的兩個問題，組合學是對數字進行計數和排列的研究。 Google DeepMind 的 Alex Davies 表示：“我們仍在努力了解其中的原因，這有望引導我們改進系統。”

高爾斯表示，目前還不清楚 AlphaProof 是如何得出答案的，也不清楚它是否使用與人類相同的數學直覺，但它能夠將精益證明翻譯成英語，從而可以輕鬆檢查它們的正確性。

澳洲雪梨大學的喬迪威廉森 (Geordie Williamson) 表示，這一結果令人印象深刻，是一個重要的里程碑。 “之前有很多嘗試在形式證明上進行強化學習，但都沒有取得太大成功。”

倫敦大學的Yang-Hui He 表示，雖然像AlphaProof 這樣的系統可能對工作數學家幫助開發證明很有用，但它顯然無助於識別需要解決和處理的問題，而這會佔用研究人員的大部分時間。

Hubert 表示，他的團隊希望 AlphaProof 能夠透過減少錯誤回應來幫助改進 Google 的大型語言模型，例如 Gemini。

貿易公司 XTX Markets 為能夠在 IMO 上獲得金牌的人工智慧提供了 500 萬美元的獎金（稱為人工智慧數學奧林匹克競賽），但 AlphaProof 不符合資格，因為它不公開。 「我們希望 DeepMind 的進步能激勵更多團隊角逐 AIMO 獎，當然也歡迎 DeepMind 自己公開參賽，」XTX Markets 的 Alex Gerko 說。