在从围棋到战棋类游戏的所有领域战胜人类后，美国谷歌公司旗下DeepMind现在表示，它在解决数学问题方面即将击败世界顶尖学生。

　　7月25日，DeepMind宣布，其人工智能系统已经解决了本月在英国巴斯举行的2024年国际数学奥林匹克竞赛（IMO）所出6个题目中的4个。人工智能给出了严谨、循序渐进的证明，由两名顶级数学家打分，得分为28/九游智能体育科技42，仅比金牌差一分。

　　国际数学奥林匹克竞赛是世界上最重要的数学赛事。图片来源：MoiraM/Alamy

　　“这显然是一个非常重大的进步。”英国剑桥的数学家Joseph Myers说。他与菲尔兹奖获得者Tim Gowers一起审查了这些解题方案，并帮助选择了今年IMO的原创题目。

　　DeepMind和其他公司正在竞相让机器最终提供证明，以解决数学领域的实质性研究问题。该公司表示，IMO的题目已经成为实现这一目标的基准，并被视为机器学习的“重大挑战”。

　　“这是人工智能系统首次达到奖牌级别的表现。”DeepMind负责人工智能科学的副总裁Pushmeet Kohli表示，“这是构建高级定理证明过程中的一个关键里程碑。”

　　今年1月，DeepMind的人工智能系统AlphaGeometry在解决一种IMO问题——欧几里得几何方面取得了奖牌级别的成绩。这是第一个在整体测试中达到金牌水平的人工智能，包括代数、组合数学和数论。这些问题通常被认为比几何更具挑战性，解决它们将有资格获得500万美元的奖金，即人工智能奥数奖（AIMO）。

　　在最新的研究中，研究人员使用AlphaGeometry2在20秒内解决了几何问题。DeepMind计算机科学家Thang Luong表示，该人工智能是他们创纪录系统的改进版本，速度更快。

　　对于其他类型的问题，团队开发了一个名为AlphaProof的全新系统。该系统花了3天时间解决了竞赛中的两个代数问题，外加一个数论问题。不过，它无法解决组合数学领域的两个问题。

　　研究人员在试图用语言模型回答数学问题时，则取得了喜忧参半的结果。有时，这些模型给出了正确答案，但无法合理解释其推理；有时，它们会胡说八道。

　　据介绍，AlphaProof将语言模型与强化学习技术相结合，使用了DeepMind成功用于“狙击”围棋等游戏以及一些特定数学问题的AlphaZero系统。

　　在强化学习中，神经网络通过试错进行学习。当它的答案可以用一些客观指标评估时，这种方法很有效。为此，AlphaProof被训练用一种名为Lean的正式语言来阅读和编写证明，后者应用于数学家常用的同名“证明助手”软件包。AlphaProof在Lean包中运行并测试其输出是否正确，这有助于填写代码中的一些步骤。

　　训练任何语言模型都需要大量数据，但Lean中几乎没有数学证明。DeepMind机器学习研究员Thomas Hubert表示，为了解决这个问题，团队设计了一个额外的网络，试图将现有的100万个用自然语言编写的问题记录翻译成Lean语言，但其中不包括人类编写的解题方案。

　　许多Lean翻译都是荒谬的，但足够多的翻译足以让AlphaProof开始它的强化学习周期。Gowers说，结果远远好于预期。在某些情况下，AlphaProof似乎能够提供额外的创造力，在无限大的可能性范围内作出正确的一步。但Gowers补充说，还需要进一步分析才能确定。

　　Myers表示，这些技术是否能够完善到在数学方面进行研究水平的工作，仍有待观察。“它能扩展到其他类型的数学问题吗？其中可能没有100万个问题需要训练。”