史上首次，AI超越人类奥赛金牌得主！吴方法加持，30题做出27道破纪录

1,112 0 0

文章摘要

【关键词】 AI超越人类、数学奥赛金牌、AI数学大师、吴方法、AlphaGeometry

在最近的一项研究中，由印度理工学院海得拉巴分校、图宾根AI中心、剑桥大学的研究者合作开发的人工智能模型AlphaGeometry，结合了1970年代吴文俊提出的吴方法，取得了突破性的成就。这个AI系统在国际数学奥林匹克竞赛（IMO）的30个几何问题中解决了27个，超越了人类IMO金牌得主的水平，成为首个达到此成就的AI。

AlphaGeometry是一个神经符号模型，通过1亿个合成样本训练而成，之前已经能够解决IMO中的25个问题。而吴方法，作为一种开创性的算法，本身就能解决15个问题，其中包括一些其他方法无法解决的问题。研究者们通过结合吴方法和经典的演绎数据库（DD）以及角度、比率和距离追踪（AR）的合成方法，创建了一个新的符号性能基准，该基准能够在5分钟内解决30个问题中的21个，其性能足以与IMO银牌得主媲美。

此外，吴方法还解决了AlphaGeometry未能解决的5个问题中的2个。通过将AlphaGeometry与吴方法结合，新的AI系统在IMO-AG-30基准上解决了27个问题，超越了人类金牌得主。这一成就不仅展示了AI在欧氏几何推理能力上的进步，也证明了代数方法与合成方法在自动化几何推理中的互补性。

欧几里得几何是测试AI推理能力的一个标准，因为它已经被有限地公理化，且有许多适合自动定理证明的系统。在国际数学奥林匹克中，参赛者使用的方法被称为「三角破解」和「重心破解」。这些方法的搜索可以通过图形表示、概率验证，或是使用人类设计的启发式方法来进行。

在几何自动推理领域，方法可以分为代数方法和合成方法。代数方法，如吴方法和Gröbner基方法，能够将几何假设转换成多项式系统来验证结论。这些方法已被证实能够有效处理广泛的几何问题。而合成方法，如演绎数据库（DD），模仿人类的证明技巧，通过逐步搜索问题来生成易于理解的证明。

研究人员使用IMO-AG-30基准进行性能评估，这是一个由谷歌DeepMind团队推出的新基准测试，包含从2000年至2022年间竞赛题中筛选出的30道经典几何问题。研究结果表明，吴方法在非常低的计算需求下实现了出色的表现，在一台普通笔记本上，研究人员在5秒内解决了15个问题中的14个。

这项研究不仅证明了AI在数学领域的巨大潜力，也表明了传统方法在软件改进后可能超越现代AI模型的证明能力。研究人员希望这项研究能激励开发几何领域自动定理证明器的新基准，并促进经典计算方法软件的改进。同时，这一成就也表明，尽管IMO几何问题对人类具有挑战性，但可能并未充分挑战现代计算求解器的极限。