国际数学奥林匹克竞赛 (IMO) 可能是面向大学预科生的最负盛名的比赛。 每年，来自世界各地的学生争夺其令人垂涎的铜牌、银牌和金牌。 很快，人工智能程序也可能与他们竞争。
今年 1 月，由 Google DeepMind 的 Trieu H. Trinh 和纽约大学领导的团队在《自然》杂志上发布了一个名为 AlphaGeometry 的新人工智能程序。 研究人员报告称，该程序能够解决过去 IMO 中的 30 道几何题中的 25 道，成功率与人类金牌获得者相似。 该人工智能还找到了 2004 年 IMO 中一个更通用的解决方案，而该解决方案此前并未引起专家的注意。
在为期两天的比赛中，参加 IMO 的学生必须解决来自不同数学领域的六个问题。 其中一些问题非常复杂，即使是专家也无法解决。 它们通常具有简短而优雅的解决方案，但需要大量的创造力，这使得它们对人工智能研究人员特别有吸引力。
支持科学新闻报道
如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻报道 订阅。 通过购买订阅，您正在帮助确保未来能够继续报道关于塑造我们当今世界的发现和想法的具有影响力的故事。
将数学证明翻译成计算机能够理解的编程语言是一项艰巨的任务。 存在专门为几何开发的正式编程语言，但它们很少使用来自其他数学领域的方法——因此，如果一个证明需要一个涉及复数等中间步骤，则无法使用专门用于几何的编程语言。
为了解决这个问题，Trinh 和他的同事创建了一个数据集，该数据集不需要将人类生成的证明翻译成正式语言。 他们首先让算法生成一组几何“前提”或起点：例如，一个三角形，其中绘制了一些测量值，并在其边上标记了额外的点。 然后，研究人员使用演绎算法来推断三角形的进一步属性，例如哪些角匹配以及哪些线彼此垂直。 通过将前提与推导出的属性相结合，研究人员创建了一个由定理和相应证明组成的训练数据集。 例如，一个问题可能涉及证明三角形的某个特征——例如，它的两个角相等。 相应的解决方案将包括演绎算法得出该结论的步骤。
然而，为了解决 IMO 级别的问题，AlphaGeometry 需要更进一步。 “关键的缺失部分是生成新的证明项，”Trinh 和他的团队在论文中写道。 例如，为了证明关于三角形的某些东西，您可能需要引入问题中未提及的新点和线——而这正是大型语言模型 (LLM) 非常擅长做的事情。
LLM 通过计算一个词跟随另一个词的概率来生成文本。 Trinh 和他的团队能够以类似的方式使用他们的数据库来训练 AlphaGeometry 关于定理和证明。 LLM 不会学习解决问题所涉及的演绎步骤； 这项工作仍然由其他专门的算法完成。相反，人工智能模型专注于寻找点、线和其他有用的辅助对象。
当 AlphaGeometry 收到一个问题时，演绎算法首先推导出一个关于该问题的陈述列表。 如果要证明的陈述未包含在该列表中，则人工智能会介入。 例如，它可能会决定在三角形 ABC 中添加第四个点 X，以便ABCX表示一个平行四边形——这是该程序从之前的训练中学到的。 这样做，人工智能为演绎算法提供了新的信息来处理。 这个过程可以重复进行，直到人工智能和演绎程序达到预期的结论。 “这种方法听起来是合理的，并且在某些方面类似于国际数学奥林匹克竞赛参与者的培训，”菲尔兹奖章获得者彼得·舒尔茨说道，他曾三次获得 IMO 金牌。
为了测试 AlphaGeometry，科学家们选择了自 2000 年以来 IMO 中出现的 30 道几何题。 以前用于解决几何问题的程序 Wu’s algorithm 仅正确解决了 10 道题，而 GPT-4 在所有问题上都失败了，但 AlphaGeometry 解决了 25 道题。 研究人员表示，人工智能的表现优于大多数 IMO 参与者，后者平均解决了 30 道题中的 15.2 道。（金牌获得者平均正确解决了 25.9 道题。）
当研究人员查看人工智能生成的证明时，他们注意到，在解决一个问题的过程中，该程序并没有使用所有提供的信息——这意味着 AlphaGeometry 独立自主地开始工作，并找到了一个相关但更通用的定理的解决方案。 同样明显的是，复杂的任务——IMO 参与者表现不佳的任务——通常需要人工智能提供更长的证明。 似乎机器也面临着与人类相同的挑战。
AlphaGeometry 尚不能参加 IMO，因为几何只是比赛的三分之一，但 Trinh 和他的同事强调，他们的方法可以应用于其他数学子学科，例如组合数学。 谁知道呢——也许几年后，一位非人类的参与者将首次参加 IMO。 也许它甚至会赢得金牌。