每周跟踪AI热点新闻动向和震撼发展 想要探索生成式人工智能的前沿进展吗？订阅我们的简报，深入解析最新的技术突破、实际应用案例和未来的趋势。与全球数同行一同，从行业内部的深度分析和实用指南中受益。不要错过这个机会，成为AI领域的领跑者。点击订阅，与未来同行！ 订阅：https://rengongzhineng.io/

周四，谷歌DeepMind宣布其AI系统AlphaProof和AlphaGeometry 2在今年的国际数学奥林匹克竞赛（IMO）中解决了六个问题中的四个，获得了相当于银牌的分数。谷歌称，这是AI首次在这一著名数学竞赛中达到这样的水平——但和AI领域的其他声明一样，这一成就也并非完全没有争议。

深入了解

谷歌表示，AlphaProof使用强化学习来在一种叫做Lean的形式化语言中证明数学命题。该系统通过生成和验证数百万个证明来训练自己，逐步解决更复杂的问题。与此同时，AlphaGeometry 2被描述为谷歌之前几何求解AI模型的升级版，现在由基于Gemini的语言模型提供支持，并在大量数据上进行训练。

据谷歌称，著名数学家蒂莫西·高尔斯爵士和约瑟夫·迈尔斯博士使用IMO的官方规则对AI模型的解答进行评分。公司报告称，其综合系统在42个可能得分中获得了28分，距离29分的金牌门槛仅差一点。这包括在比赛中最难的一个问题上取得的满分，谷歌声称今年只有五名人类选手解决了这个问题。

一场与众不同的数学竞赛

自1959年以来，每年举办的IMO让顶尖的高中数学家们面对代数、组合学、几何和数论中极其困难的问题。IMO问题的表现已成为评估AI系统数学推理能力的公认基准。

谷歌声称，AlphaProof解决了两个代数问题和一个数论问题，而AlphaGeometry 2则解决了几何问题。AI模型未能解决两个组合学问题。公司声称其系统在几分钟内解决了一个问题，而其他问题则花费了长达三天的时间。

谷歌表示，他们首先将IMO问题翻译成AI模型可以处理的形式化数学语言。这一步与正式比赛不同，后者要求人类选手在两次4.5小时的比赛中直接处理问题陈述。

谷歌报告称，在今年的比赛之前，AlphaGeometry 2能够解决过去25年历史IMO几何问题的83%，高于其前身的53%的成功率。公司称，新系统在收到形式化版本后，在19秒内解决了今年的几何问题。

局限性

尽管谷歌声称取得了突破，但蒂莫西·高尔斯爵士在X上的一个帖子中提供了更为细致的看法。虽然他承认这一成就“远超以往的自动定理证明器所能达到的水平”，但也指出了几个重要的限制条件。

“主要的限制是程序需要比人类选手更长的时间——有些问题超过60小时——当然处理速度也比人类大脑快得多，”高尔斯写道。“如果人类选手被允许每个问题有这么长的时间，他们的得分无疑会更高。”

高尔斯还指出，在AI模型开始工作之前，问题是由人类手动翻译成Lean的形式化语言的。他强调，尽管AI执行了核心的数学推理，但这一“自动形式化”步骤是由人类完成的。

关于对数学研究的更广泛影响，高尔斯表示不确定。“我们是否接近数学家变得多余的地步？很难说。我猜我们还需要一个或两个突破，”他写道。他认为系统的长处理时间表明它尚未“解决数学问题”，但也承认“当它运行时显然有些有趣的事情在发生。”

即便有这些限制，高尔斯推测这样的AI系统可能会成为有价值的研究工具。“我们可能接近拥有一个程序，它可以让数学家回答一系列广泛的问题，只要这些问题不是太难——类似于人类在几小时内可以解决的问题。即使它本身不能解决开放问题，这也将是一个非常有用的研究工具。”