当巴黎准备举办第33届奥运会时，来自近110个国家的600多名学生于7月齐聚在田园诗般的英国小镇巴斯，参加国际数学奥林匹克竞赛（IMO）。他们有两场分别为四个半小时的考试，回答来自不同数学学科的六道问题。中国学生施皓嘉以满分的成绩在个人排名中名列第一。在国家队排名中，美国队名列榜首。然而，本次赛事最引人注目的成果是谷歌DeepMind的两台机器取得的成绩。DeepMind的人工智能程序总共解决了六道题中的四道，这相当于银牌得主的水平。这两个程序获得了总分42分中的28分。只有大约60名学生的得分高于这个分数，数学家和菲尔兹奖得主蒂莫西·高尔斯在X（前身为Twitter）上的一则帖子中写道，他本人曾是该比赛的金牌得主。
为了取得如此令人印象深刻的成绩，DeepMind团队使用了两个不同的人工智能程序：AlphaProof和AlphaGeometry 2。前者以类似于掌握了国际象棋、将棋和围棋的算法的方式工作。AlphaProof使用所谓的强化学习，反复与自身对弈，并逐步改进。这种方法可以很容易地应用于棋盘游戏。人工智能执行几个步骤；如果这些步骤没有带来胜利，它就会受到惩罚，并学习追求其他策略。
然而，要对数学问题做同样的事情，程序不仅必须能够检查它是否解决了问题，还必须验证它为得出解决方案而采取的推理步骤是否正确。为了实现这一目标，AlphaProof使用了所谓的证明助手——算法一步一步地检查逻辑论证，以检查对所提出的问题的答案是否正确。尽管证明助手已经存在了几十年，但它们在机器学习中的应用一直受到形式语言（如Lean）中可用的数学数据量非常有限的限制，而计算机可以理解这些语言。
支持科学新闻报道
如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻报道 订阅。通过购买订阅，您正在帮助确保有关塑造我们当今世界的发现和想法的具有影响力的故事的未来。
另一方面，以自然语言编写的数学问题解决方案非常丰富。互联网上有大量人类一步一步解决的问题。因此，DeepMind团队训练了一个名为Gemini的大型语言模型，将一百万个此类问题翻译成Lean编程语言，以便证明助手可以使用它们进行训练。“当遇到问题时，AlphaProof会生成候选解决方案，然后通过在Lean中搜索可能的证明步骤来证明或反驳它们，”开发者在DeepMind的网站上写道。通过这样做，AlphaProof逐渐学习哪些证明步骤是有用的，哪些是无用的，从而提高其解决更复杂问题的能力。
几何问题也出现在IMO中，通常需要完全不同的方法。早在今年1月，DeepMind就展示了一个名为AlphaGeometry的人工智能，它可以成功解决此类问题。为了做到这一点，专家们首先生成了大量的几何“前提”或起点：例如，一个绘制了高线并在边上标记了点的三角形。然后，研究人员使用所谓的“演绎引擎”来推断三角形的进一步性质，例如哪些角重合，哪些线彼此垂直。通过将这些图表与推导出的性质相结合，专家们创建了一个由定理和相应的证明组成的训练数据集。这个过程与一个大型语言模型相结合，该模型有时也使用所谓的辅助构造；该模型可能会向三角形添加另一个点，使其成为四边形，这可以帮助解决问题。DeepMind团队现在推出了改进版本AlphaGeometry 2，通过使用更多数据训练模型并加快算法速度。
为了测试他们的程序，DeepMind的研究人员让这两个人工智能系统参加了今年的数学奥林匹克竞赛。该团队首先必须手动将问题翻译成Lean。AlphaGeometry 2设法在短短19秒内正确解决了几何问题。与此同时，AlphaProof能够解决一个数论问题和两个代数问题，其中包括一个只有五名人类参赛者能够破解的问题。然而，人工智能未能解决组合问题，这可能是因为这些问题很难翻译成Lean等编程语言。
AlphaProof的性能很慢，完成一些问题需要超过60个小时——大大超过了学生们被分配的总共九个小时。“如果人类参赛者被允许每个问题有这么长的时间，他们无疑会获得更高的分数，”高尔斯在X上写道。“然而，（i）这远远超出了以前的自动定理证明器所能做到的，并且（ii）随着效率的提高，这些时间可能会缩短。”
高尔斯和另一位曾获得金牌的数学家约瑟夫·K·迈尔斯使用与人类参与者相同的标准评估了这两个人工智能系统的解决方案。根据这些标准，这些程序获得了令人印象深刻的28分，相当于银牌。这意味着人工智能仅以微弱差距错失了达到金牌水平的表现，金牌水平的分数是29分或更高。
高尔斯在X上强调，人工智能程序已经接受了相当广泛的问题的训练，并且这些方法不仅限于数学奥林匹克竞赛。“我们可能很快就会拥有一个程序，使数学家能够获得各种问题的答案，”他解释说。“我们是否已经接近数学家变得多余的程度？这很难说。”
本文最初发表于《明镜在线》并经许可转载。