下载客户端

谷歌AI做题家AlphaGeometry解决几何奥数题暂时拔得头筹，登上Nature

2024-01-22 15:43

来源：澎湃新闻·澎湃号·湃客

原创 zzllrr小乐 zzllrr小乐

本文原创内容（不含图片部分）遵循CC知识共享协议，

未经许可，也可以自由转载引用，

但请保留zzllrr小乐公众号原文链接，谢谢理解支持。

前不久，伦敦金融科技公司XTX Markets刚刚公布1000万美元AI-MO奖，奖励能在国际数学奥林匹克竞赛（IMO）中获得金牌并公开分享开源的AI人工智能模型。各路国内外AI做题家纷纷摩拳擦掌跃跃欲试，包括谷歌Deepmind在内。

详情点击→：谷歌DeepMind的Alpha系列家族

新成员——AlphaGeometry阿尔法几何

产品年份用途AlphaGo2015打败围棋世界冠军，标志性的AI成就Magenta2016在创意过程中使用机器学习的先锋项目WaveNet2016实现了逼真的文本转语音，用于Google助手等AlphaZero2017推广了AlphaGo的概念，具有更广泛的适用性，解决多种游戏和问题AlphaStar2019打败《星际争霸II》顶级职业玩家，涉足RTS实时战略游戏Project Euphonia2019改善有语言障碍的人群的交流AlphaCode2020以竞争水平编写计算机程序的能力AlphaDev2020发现更快的排序算法AlphaFold2020准确预测蛋白质结构，推动生物学领域的进展MuZero2020AlphaZero的继任者，具备更广泛的游戏和实际问题求解能力LaMDA2021展示了更具对话性的AI系统潜力，提升了用户体验PaLM-SayCan2021在机器人系统中使用大型语言模型，提升机器人技能RT-22021创建更广泛的视觉-语言-动作模型Imagen2022文本到图像生成模型Bard2023Google的协作实验项目，对标New BingUniversal Speech Model2023提高对世界各地更多口音语言的理解能力AlphaGeometry2024解几何奥数题，接近人类选手水平

谷歌DeepMind的最新AI系统名叫AlphaGeometry（阿尔法几何），在解决数学几何问题方面取得了显著突破。这个系统据称在国际高中生数学奥林匹克竞赛（IMO）中的表现接近人类金牌得主水平，正确回答了30道题目中的25道（之前最先进的“吴文俊方法”解决了其中10个几何问题，而人类金牌得主平均解决了25.9个问题），正确率达83%。昨日这一成果在《自然》（Nature）杂志上公开发表，并被认为代表了人类水平的自动推理的一个显著里程碑。

关于测试基准Benchmark

测试基准包括从2000年至今的官方IMO问题，这些问题可以在论文作者工作中所使用的几何环境中显式表示出来。人类选手在IMO竞赛中的表现得分（0到7之间）被重新估算缩放到0到1之间，以匹配机器的失败/成功的二进制结果。例如，参赛者在满分7分中得到4分的成绩在此项比较中将被缩放，而被认为是解决了0.57（即4/7）个问题。而AlphaGeometry和其他机器求解器对于任何问题的得分要么是0（未解决），要么是1（解决）。

但请留意，这只是在经典几何题目中与人类选手的粗略比较，毕竟人类选手的特点是根据自然语言陈述进行思考操作，而不像AI机器是在狭窄特定领域对经过翻译转换后的内容进行操作。此外，一般的IMO竞赛还包括其他类型的问题，如几何不等式或组合几何，以及数学的其他领域，如代数、数论和组合数学。所以目前即使AlphaGeometry能做到100%成功解出几何题，还需要集成其它数学学科的能力来解决其它类型的奥数题。

解几何题的一个简单示例：等腰三角形等边对等角

下图显示了 AlphaGeometry 如何解决一道简单的中学几何证明题：

等腰三角形等边对等角

如下图a，设任一等腰三角形ABC，AB=AC，试证明：∠B=∠C。

图b，AlphaGeometry 通过运行符号推导引擎来启动证明搜索。引擎从定理前提条件中穷尽地推导出新陈述，直到定理被证明或新陈述被穷尽。

图c，由于符号引擎无法找到证明，语言模型构造一个辅助点，在符号引擎重试之前增加证明状态。这种循环一直持续到找到解决方案为止。

图d，举个简单的例子，在第一个辅助构造“设D为BC的中点”之后循环终止。该证明由另外两个步骤组成，这两个步骤都利用了中点性质：“BD = DC”和“B，D，C是共线的”，以蓝色突出显示。

解几何题的一个复杂示例：IMO 2015 P3

下图显示了 AlphaGeometry 如何解决 IMO 2015 问题 3 ：

如下图e，设ABC是锐角三角形。设圆O是它的外接圆（circumcircle），H是它的垂心（orthocenter），F是高AF的垂足。设M为BC的中点。设Q为圆O上的一点，满足QH⊥QA。设K为圆O上的一点，满足KH⊥KQ。

证明：三角形FKM和KQH的外接圆（分别是O₁、O₂）是相切的。

图f，解方案有三个辅助点D、G、E。论文作者将语言模型输出（蓝色）与符号引擎输出交错排列，以反映其执行顺序。请注意，出于说明目的，图f 中的证明已被大大缩短和编辑。其完整版本在原文补充信息中。

AlphaGeometry合成数据生成的过程

图a，先对一个大的随机定理前提条件集合抽样。

图b，使用符号推理引擎获得推理闭包。这将得到陈述语句的一个有向无环图。对于图中的每个节点，论文作者执行回溯以找到其最小的必要前提条件和推理依赖集合。例如，对于最右边的节点 'HA ⊥ BC'，回溯会返回绿色的子图。

图c，最小前提条件和相应的子图构成一个合成问题及其解决方案。在右下角的例子中，尽管点 E 和 D 与构造 HA 和 BC 无关，它们仍参与了证明；因此，它们被语言模型学习，认为是辅助构造。

生成的合成数据的分析

从生成的合成证明中，有9%包含辅助构造。仅有大约0.05%的合成训练证明的长度比测试集问题的平均AlphaGeometry证明长度更长。最复杂的合成证明长度为247，包含两个辅助构造。大多数合成定理前提条件不像人类发现的定理那样对称，因为它们不偏向于任何美学标准。

IMO-AG-30测试基准的主要结果

论文作者将AlphaGeometry与其他最先进的方法进行比较（包括计算机代数和搜索方法），尤其是吴文俊方法。论文作者还展示了DD + AR（论文作者的贡献）及其变体的结果，形成了最强大的基线DD + AR + 人工设计的启发式方法。最后涵盖了AlphaGeometry在没有预训练和微调情况下的消融设置。方法

已解决的问题数

（满分30个）计算机代数吴文俊方法10Gröbner基4搜索（类人）GPT-40全角度方式2推理数据库（DD）7DD + 人工设计的启发式方法9DD + AR（论文作者的）14DD + AR + GPT-4 辅助构造15DD + AR + 人工设计的启发式18

AlphaGeometry

（阿尔法几何）25无需预训练21无需微调23

AlphaGeometry发现了一个比IMO 2004 P1翻译后更为泛化的定理

IMO 2004 P1问题1：

设ABC为锐角三角形，AB≠AC。直径为BC的圆与AB和AC分别在M和N处相交。边BC的中点记作O。∠BAC和∠MON的平分线相交于R。证明：三角形BMR和CNR的外接圆，在边BC上有一个公共点P。

左侧，从上到下，是以自然语言陈述的IMO 2004 P1问题，经过翻译后的陈述以及AlphaGeometry的解决方案。由于回溯算法可以提取最小前提条件，AlphaGeometry确定了一个在证明中不必要的前提：O不必是BC的中点，使得P、B、C共线。右侧，顶部，是原定理图；底部，是泛化的定理图，在其中O被释放出其中点位置，而P仍然位于线段BC上。请注意，原始问题要求P在B和C之间，这是广义定理和解决方案无法保证的条件。

AlphaGeometry证明长度与IMO参与者在不同问题上的平均得分的对比

在已解决的问题中，IMO参与者认为2000 P6、2015 P3和2019 P6最为困难，所以AlphaGeometry对其证明也较长。然而，对于更容易的问题，AlphaGeometry的证明长度与人类得分之间的相关性较小。

结语

AlphaGeometry是第一个超越IMO参赛者在证明欧几里得平面几何定理方面平均表现的计算机程序，优于强大的计算机代数和搜索基准线。值得注意的是，论文作者通过AlphaGeometry展示了一种神经符号方法，通过从头开始进行大规模探索来证明定理，避免了对人类注释的证明示例和人工策划的问题陈述的需求。在纯合成数据上生成和训练语言模型的方法为面临相同数据稀缺问题的数学领域提供了一个通用的指导框架。

在攻克数学难题的路上，还是有很大的发展空间和难关。作为关心数学领域发展的普通人而言，我们期待有更全面的开源AI，能继续完成AlphaGeometry暂时无法解决的数学题任务，继续角逐AI-MO大奖，甚至为整个数学科研和教育领域带来新的推动力量和创造性解决方案，打破发展的瓶颈，造福广大社区。

参考资料

https://www.nature.com/articles/s41586-023-06747-5

https://www.nature.com/articles/s41586-023-06747-5.pdf

https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/

https://deepmind.google/about/

http://bard.google.com

https://imagen.research.google

https://magenta.tensorflow.org

https://sites.research.google/euphonia/about/

https://sites.research.google/usm/

https://www.deepmind.com/research/highlighted-research/alphafold