2024年7月25日，曾经发布过AlphaGo、AlphaFold和AlphaGeometry系列人工智能的DeepMind宣布，他们使用最新研发的，用于求解数学难题的人工智能程序AlphaProof和AlphaGeometry 2，在今年的国际数学奥林匹克竞赛当中取得了相当于银牌的成绩。
国际数学奥林匹克竞赛每年举行一次，每次比赛的试卷由6道题目组成，每题7分，满分42分；赛事分两日进行，每位选手独立答题，不得交流或使用场外资料等作弊手段；每天参赛者有4.5小时来解决3道问题（由上午9时到下午1时30分）。大约有十二分之一的学生可以获得金牌。银牌和铜牌的数量分别是金牌的2倍和3倍。
近几年全球范围内的人工智能热潮，能够维持多久的高速发展，最终又将怎样改变我们的生活，是一个引人注目的话题。视觉中国|图
今年国际数学奥林匹克竞赛共有609名选手参加，最终有58名选手获得金牌，123名选手获得银牌，145名选手获得铜牌。其中金牌选手的分数线为29分。AlphaProof与AlphaGeometry 2组成的“混合人工智能组合”完整解答了本次国际数学奥林匹克竞赛六道题目中的四道，最终得分为28分，差一分就能够获得金牌。
求解数学问题，一直是衡量人工智能逻辑推理和解决问题能力的一项重要指标。这其中，求解数学奥林匹克问题，更是判断人工智能数学能力的一个很好的标杆。这次AlphaProof与AlphaGeometry 2所取得成绩，也是目前人工智能在数学奥林匹克竞赛中的最好成绩。
这其中的AlphaGeometry 2，是DeepMind团队在年初发布的AlphaGeometry的更新版本。相较于上一代的AlphaGeometry，这次的AlphaGeometry 2不管是符号引擎的效率，还是用于合成数据的训练集，都要强不止一个数量级。这也就使得AlphaGeometry2的性能，相较于前代有了巨大提升。在解答今年国际数学奥林匹克的试题时，AlphaGeometry 2仅用时19秒就解决了六道试题中的第四道平面几何问题。
AlphaGeometry 2的这种提升，代表了近几年人工智能领域发展的一个主流趋势——使用更加高效化的引擎和模型架构，同时加大模型和数据集的规模，以此获得更加智能、更加高效的人工智能程序。不仅是AlphaGeometry系列，在诸如OpenAI研发的GPT系列，以及同样由DeepMind研发的AlphaFold系列等人工智能上，都可以看到最新一代的发布间隔越来越短，与此同时相较于前一代有着性能的巨大提升。这一切，都让人想到了著名的“摩尔定律”：当价格不变时，集成电路上可容纳的晶体管数目每隔18-24个月将增加一倍，性能也将提升一倍。
英特尔公司联合创始人戈登·摩尔在1965年提出的摩尔定律，预言了接下来五十余年芯片行业浩浩荡荡的发展进程，并最终彻底改变了我们现在的生活。作为对比，就让人不禁期待，近几年这波全球范围内的人工智能热潮，能够维持多久的高速发展，最终又将怎样改变我们的生活。
如果说AlphaGeometry 2的巨大提升可以看做是现阶段人工智能发展的“常规升级”的话，那么这次DeepMind所使用的“混合人工智能组合”中用来解决其他数学问题的AlphaProof，则可以看做是当前人工智能在求解数学问题这一领域的全新突破。
AlphaGeometry系列，是针对平面几何问题专门化的人工智能。AlphaGeometry能够对每一个几何图形，穷举该图形能够得到的命题，并且能够反过来回溯每个命题所包含的几何图形的集合。在解题过程中，AlphaGeometry会搜寻题目条件中的几何图形所能够得到的命题，以及包含题目所要证明的结论命题的几何图形的集合。通过比对这两个集合中集合对象的差异，找到辅助线的位置。通过这种训练，DeepMind成功地让AlphaGeometry的大型语言模型学会了几何证明中最为重要的技巧：添加和使用辅助线。但是，这种针对平面几何特化的策略，显然是无法应用到别的类型的数学问题上去的。
另外一方面，现阶段主流的，以GPT系列为代表的大型语言模型的训练和养成，主要是靠互联网上的信息。想要通过这样的方式，获得足够的数学材料，训练出AI的数学推理和解题能力，本身就是不现实的。而且，专业数学能力的培养，本身也不是GPT这类综合型大型语言模型所要实现的目标。
因此，DeepMind团队采取了另外一种方式，来训练AlphaProof。这种方式同样来自于DeepMind曾经的一款人工智能程序，AlphaZero。AlphaZero是DeepMind开发的，击败了李世石和柯洁AlphaGo的后续版本。AlphaZero基于蒙特卡洛树搜索，并且同样可以通过自我对弈来实现自主学习。
在AlphaProof这里，DeepMind团队也做了类似的事情。让AlphaProof自行尝试解决数学问题，并自己判断结果的对错。通过这样的方式，来让AlphaProof学会求解数学问题。
这看上去似乎是一种很自然的做法。似乎和我们在中小学阶段通过做习题来学习数学没有什么差别。但是，这种看似自然的学习方式，对于人工智能来说，有两个很难克服的障碍。
第一个难点就是数学题目都是用我们日常使用的自然语言写成的。怎样让人工智能能够“看懂”这些题目，并且提取题目中的信息，将其转化成抽象的数学问题，是首先必须要解决的问题。
针对这一难点，DeepMind团队使用了谷歌开发的大型语言模型Gemini，并且针对数学题目对其进行了微调。这一“定制版”的Gemini，能够将自然语言写成的题目转化成抽象的形式化的数学符号写成的命题。然后把转化后的问题，交给AlphaProof求解。这样，AlphaProof就能够“看懂”数学题目，并且理解其中的问题。
而这一做法真正的难点，在于AlphaProof自主学习的过程中，怎样让它知道什么是对，什么是错。这一点是至关重要的。否则，就相当于对着错题进行练习，练到最后也还是错的。这一点对于AlphaGo和AlphaZero完全不是什么问题。因为围棋这样的棋类运动，有一个非常简单的判断标准，那就是最后的胜负。只需要在每次对局结束之后判断双方的胜负关系，就可以得到反馈数据。
但是，要去判断一个数学题的证明过程是否正确，那难度就要高得多了。
在这里，DeepMind团队使用了Lean，这个由微软研究院的莱昂纳多·德·莫拉最初于2013年发布的开源交互式证明机，来验证AlphaProof得出的形式化证明的对错。通俗地说就是，相当于给AlphaProof找了一个“批改作业”的“老师”。
可以说，这次DeepMind团队解答国际数学奥林匹克竞赛题目所取得的成绩，来自于DeepMind自2014年AlphaGo以来，十余年的技术积累。与此同时，也离不开近几年人工智能在包括大语言模型等领域的飞速进展。正是这些已有的成果，使得DeepMind得以在很短的时间内，就在人工智能求解数学题这一领域当中取得了如此惊人的成绩。
南方周末特约撰稿 左力
责编 朱力远
