「相當於銀牌得主」奧林匹亞解題難不倒AI 圍棋之道如何套用於數學？

谷歌DeepMind兩款人工智慧在今年國際數學奧林匹亞競賽一共解開六題中的四題，滿分42分拿到28分，程度相當於人類銀牌得主。路透／NURPHOTO

英國城市巴斯今年7月舉辦國際數學奧林匹亞競賽（IMO），吸引全球近110國600多名學生較量。不過這次比賽最引人矚目的，是谷歌DeepMind兩款人工智慧的參賽表現。它們一共解開六題中的四題，滿分42分拿到28分，程度相當於人類銀牌得主。

《科學人》（Scientific American）報導，國際數學奧賽分爲兩場測驗，要回答不同數學領域的六道問題，每場答題時間4個半小時。中國大陸浙江省高中生史皓嘉個人以滿分成績取得金牌；國家排名方面則是美國隊第一。

菲爾茲獎得主高爾斯（Timothy Gowers）在社羣媒體X上指出，谷歌DeepMind在這次比賽達到約銀牌等級，600多名參賽者中約只有60人贏過它。

如此成就歸功於兩款AI：AlphaProof與AlphaGeometry 2。前者的運作與精通西洋棋、日本將棋與圍棋的演算法類似，即使用強化學習，不斷與自己競爭並逐步改進。這種方法可以輕易上手棋盤類遊戲；AI會走幾步棋，如未能取勝，就會受到懲罰並學習改走其它步。

然而，相同方法套用在數學上，AI除了必須證明自己已解開問題，還得驗證答題的推理過程也是對的。

爲了實現這點，AlphaProof運用所謂的證明助手——這些演算法會逐步進行邏輯論證，檢查解法是否正確。證明助手已存在數十年，但要應用在機器學習則受到侷限，因爲它必須使用如Lean的形式語言（formal language），這方面的數學數據非常稀少。

相較之下，以人類自然語言寫成的數學題解答在網路上資源很多，也有逐步解法。因此，DeepMind團隊訓練了名爲Gemini的大型語言模型，將百萬個問題翻譯成Lean形式語言，供證明助手用於訓練。

「面對問題時，AlphaProof會生成解答候選，然後透過搜尋Lean中可能的證明步驟來證明或否定它們。」 開發人員在DeepMind網站寫道。如此一來，AlphaProof逐漸學會哪些證明步驟是有用或無用的，強化解決更復雜問題的能力。