「相當於銀牌得主」奧林匹亞解題難不倒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逐渐学会哪些证明步骤是有用或无用的，强化解决更复杂问题的能力。