「相當於銀牌得主」奧林匹亞解題難不倒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逐漸學會哪些證明步驟是有用或無用的,強化解決更復雜問題的能力。