本报讯 在从围棋到战略棋类游戏的所有领域战胜人类后，美国谷歌公司旗下的DeepMind表示，它即将在解决数学问题方面击败全球最优秀的学生。

7月25日，DeepMind宣布，其人工智能（AI）系统已经解答了本月在英国巴斯举行的2024年国际数学奥林匹克竞赛（IMO）6个题目中的4个。AI给出了严谨、循序渐进的证明，并由两名顶级数学家打分，得分为28/42，这相当于银牌的成绩，仅比金牌差1分。

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

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

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

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

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

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

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

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

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

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

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

Myers表示，这些技术能否完善到在数学领域进行研究级别的工作，仍有待观察。“它能扩展到其他类型的数学问题吗？在那里可能没有100万个问题可以训练。”（王方）