吴的方法可以将符号人工智能提升到银牌获得者的竞争对手，而 AlphaGeometry 则可以超越 IMO Geometry 金牌获得者

Shiven Sinha

{}^{1}

Ameya Prabhu

{}^{2*}

Ponnurangam Kumaraguru

{}^{1}

Siddharth Bhat

{}^{3\dagger}

Matthias Bethge

{}^{2\dagger}

{}^{1}

IIIT Hyderabad

{}^{2}

Tübingen AI Center, University of Tübingen

{}^{3}

University of Cambridge equal contribution

{}^{\dagger}

equal advising

摘要

证明几何定理是结合直觉和逻辑技能的视觉推理的标志。因此，奥林匹克级别几何问题的自动定理证明被认为是人类级别自动推理的一个重要里程碑。 AlphaGeometry 的推出标志着一项重大突破，这是一种用 1 亿个合成样本训练的神经符号模型。它解决了 30 个国际数学奥林匹克 (IMO) 问题中的 25 个，而基于 Wu 的方法报告的基线仅解决了 10 个。在这篇文章中，我们重新审视了 AlphaGeometry 引入的 IMO-AG-30 挑战赛，发现 Wu 的方法出奇地强大。仅吴的方法就可以解决15个问题，其中一些问题是其他任何方法都无法解决的。这导致了两个关键发现：（i）将 Wu 的方法与演绎数据库和角度、比率和距离追踪的经典综合方法相结合，仅使用仅使用 CPU 的笔记本电脑在 5 分钟的时间限制内解决了 30 种方法中的 21 种每个问题。从本质上讲，这种经典方法仅比 AlphaGeometry 少解决 4 个问题，并建立了第一个完全象征性基线，其强度足以与 IMO 银牌得主的表现相媲美。 (ii) Wu 的方法甚至解决了 AlphaGeometry 未能解决的 5 个问题中的 2 个问题。因此，通过将 AlphaGeometry 与 Wu 的方法相结合，我们在 IMO-AG-30 上建立了一种新的最先进的自动定理证明，解决了 30 个问题中的 27 个，这是第一个超越 IMO 金牌得主的人工智能方法。

https://huggingface.co/datasets/bethgelab/simplegeometry

1简介

自动定理证明一直是开发能够满足数学研究所需的猜想和证明能力的计算机程序的长期目标[10]。该领域已将解决奥林匹克级几何问题视为一个关键里程碑[2, 1]，标志着计算机执行复杂数学推理的前沿。国际数学奥林匹克 (IMO) 始于 1959 年，举办世界上最著名的定理证明竞赛，在发现解决问题的杰出人才方面发挥着重要作用。事实上，一半的菲尔兹奖获得者在年轻时就参加过国际海事组织（IMO），在奥林匹克级别上追平人类顶尖表现已成为人工智能研究的一个显着里程碑。

欧几里得几何非常适合测试人工智能系统的推理能力。它是有限公理化的[15]，多年来已经提出了许多欧几里得几何的证明系统，这些系统适用于自动定理证明技术[4, 5]。此外，证明搜索可以通过图表表示 [12, 18]、概率验证 [11, 23] 以及使用人类设计的启发式进行的大量可能推论来指导对于角度、面积和距离等属性，International 亲切地称为“trig bashing”和“bary bashing”[24, 25] 的方法数学奥林匹克（IMO）参与者。此外，这个领域具有挑战性 - 需要定义特定的证明系统来指定问题，缺乏训练数据，并且问题通常包含围绕退化情况的模糊性[29,20,17] 解决起来很复杂，并导致了幽默的民间传说“几何问题永远不会解决简并性”。

几何中的自动推理可以分为代数[28,27,16]和综合方法[12,6,22]。最近的重点是演绎数据库 (DD) [6] 等合成方法，这些方法模仿人类的证明技术，并通过将定理证明问题视为逐步搜索问题来生成可理解的证明使用一组几何公理。例如，DD 使用一组固定的专家策划的几何规则，这些规则被重复应用于初始几何配置。执行此操作直到系统达到固定点并且无法使用可用规则推断出新的事实。 AlphaGeometry [26] 是一种新颖的神经符号证明器，代表了该领域最近的突破性进展。它在 DD 的先前工作中添加了额外的规则来执行角度、比率和距离追逐 (AR)，并且使用大型语言模型 (DD+AR+LLM) 建议的结构进一步增强了最终的符号引擎 (DD+AR) -Constructions）经过 1 亿次合成证明训练。它通过解决 30 个 IMO 问题中的 25 个来超越代数方法，而基于 Wu 的方法 [28, 8] 的报告基线仅解决了 10 个 [26]。

代数方法，例如吴氏方法和Gröbner基方法[16]，将几何假设转化为多项式组来验证结论。它们提供了强大的过程，经证明可以决定广泛的几何类别[8, 16]中的陈述。更准确地说，吴的方法能够解决任何可以使用代数方程表达假设和结论的问题[7]，同时自动生成非简并条件[29, 17 ]。这一显着特征意味着吴的方法不仅可以处理平面几何中的问题，还可以处理实体和高维几何中的问题，即在需要付出巨大努力和额外考虑才能使用合成方法的领域。 [9]。

在这项工作中，我们将吴的方法的能力用于涉及有意义和结构化数学陈述的问题的测试，而不是通常任意的最坏情况实例[13]。为此，我们在Trinh等人[26]引入的IMO-AG-30基准上重新评估Wu的方法。我们发现它的性能出人意料地强大，解决了 15 个问题，其中一些问题是任何其他方法都无法解决的。这导致了两个重要的发现：

•

将 Wu 方法 (Wu) 与演绎数据库 (DD) 和角度、比率和距离追踪 (AR) 等经典综合方法相结合，仅使用一台仅使用 CPU 的笔记本电脑即可解决 30 种方法中的 21 种，每次时间限制为 5 分钟问题。从本质上讲，这种经典方法（Wu&DD+AR）仅比 AlphaGeometry 少解决了 4 个问题，并建立了第一个完全符号基线，其强度足以与 IMO 银牌得主的表现相媲美。
•

Wu的方法甚至解决了AlphaGeometry（AG）未能解决的5个问题中的2个。因此，通过将 AlphaGeometry 与 Wu 的方法 (Wu&AG) 相结合，我们在 IMO-AG-30 上建立了一种新的最先进的自动定理证明，解决了 30 个问题中的 27 个，这是第一个超越 IMO 金牌获得者的 AI 方法。

2 实验与结果

Refer to caption — 图1： A) IMO-AG-30 问题集上符号法和 LLM 增强方法的表现以及人类表现。我们按照银牌获得者的标准在符号系统中设定了强有力的基线，并且以一个问题的优势超越了金牌获得者。右图：图表显示了不同方法在 IMO-AG-30 问题上如何相互重叠或互补。

2024 年 1 月，Trinh 等人[26]引入了 IMO-AG-30 作为新基准，以展示 AlphaGeometry 的技能水平。 IMO-AG-30 基于自 2000 年以来从 IMO 竞赛中收集的几何问题，并适应于交互式图形证明助手中使用的更窄的、专门的经典几何环境，从而形成了包含 30 个经典几何问题的测试集。该基准测试中解决的问题数量与 IMO 参赛者平均解决的问题数量有关。如图1（A）中的灰色水平线所示，铜牌、银牌和金牌选手平均解决了这些问题的19.3、22.9和25.9，15.2代表了所有参赛者的平均水平。为 IMO-AG-30 收集的具体问题集列在图 1 (B) 的图表左栏中。

实验细节。我们使用 IMO-AG-30 基准测试来评估性能，基线和数据集均来自 Trinh 等人[26]。我们只是通过 JGEX 软件[19, 30]重新实现了 Wu 的方法，将 IMO-AG-30 问题手动转换为 JGEX 兼容格式¹¹1但是，由于 JGEX 框架内缺乏适当的构造，30 个问题中有 4 个无法翻译，因此我们报告的问题是 26 个问题中的一个。. 我们还成功地重现了 DD+AR 基线，这是我们从 AlphaGeometry 代码库中最终提出的方法所必需的。我们手动验证了JGEX针对我们翻译的几个问题生成的假设和结论方程确实是正确的。

结果。我们的发现与 [26] 之前的结果结合显示在图 1 中。图1（A）比较了解决的问题数量，（B）显示了哪些问题通过哪种方法解决，以可视化不同方法如何相互重叠或互补。在图1（A）中，IMO参赛者的表现水平用灰色水平线表示，显示金、银、铜、平均和荣誉奖级别。合成符号方法的性能水平用蓝色条显示，LLM 增强神经符号方法的性能水平用绿色条显示。我们自己用吴的方法获得的结果属于代数综合方法的范畴，用橙色条表示。合成符号方法（蓝色）或神经符号LLM增强方法（绿色）的所有结果均来自[26]。

我们将 Wu 的方法与 DD+AR 相结合，设置了一个新的符号基线 (Wu&DD+AR)，其性能比所有传统方法高出了 6 个问题。它解决了 21 个 IMO-AG-30 问题，与附录中所示的 AlphaGeometry 水平相匹配，无需微调（仅限 FT-9M）（图 2)。吴的方法以非常低的计算要求实现了这种性能。在配备 AMD Ryzen 7 5800H 处理器和 16 GB RAM 的笔记本电脑上，我们能够在 5 秒内解决 15 个问题中的 14 个问题，其中一个问题（2015 P4）需要 3 分钟。在我们的实验中，吴的方法要么几乎立即解决问题，要么笔记本电脑在 5 分钟内耗尽内存。值得注意的是，我们用 Wu 的方法解决的 15 个问题中，有 2 个问题（2021 P3、2008 P1B）属于 AlphaGeometry 难以解决的 5 个问题。因此，通过 Wu 的方法和 AlphaGeometry 之间的简单集成组合，我们获得了新的最先进的解决方案，解决了 IMO-AG-30 基准上 30 个问题中的 27 个，如绿色/橙色条所示 (Wu&AG) 图 1。

3结论

总的来说，我们的笔记强调了代数方法在自动几何推理中解决国际数学奥林匹克（IMO）几何问题的潜力²²2Peter Novotný 使用 Gröbner 基础方法类似地证明了 1984 年至 2003 年 17 个 IMO 几何问题中的 11 个，尽管只是在手动添加非简并条件之后[ 3]如此处所引用。，将 IMO-AG-30 上吴方法解决的问题数量从 10 个增加到 15 个。在这十五个问题中，有几个对于合成方法及其目前最流行的LLM增强版本来说是困难的。

据我们所知，我们的符号基线是唯一表现高于 IMO 参赛者平均水平并接近 IMO 几何银牌得主表现的符号基线。同样，我们将 AlphaGeomtery 与 Wu 的方法相结合，是第一个在 IMO 几何问题上超越人类金牌得主的人工智能系统。这一成果说明了该领域代数方法和综合方法的互补性（见图1 B）。代数方法的有用性在 2008 P1B 和 2021 P3 这两个问题中最为明显，目前除了 Wu 的方法之外，没有其他自动定理证明器可以解决这两个问题。

虽然代数方法一直因其理论保证而受到认可，但其实用性此前曾因速度太慢且无法被人类解释而受到质疑。我们的观察表明，在几个问题上，吴氏方法的执行效率比之前认识的要高，我们主张不要仅仅因为它无法产生人类可读的证明而驳回它。

我们的结果正在进行中，目前受到现有实现的稀缺性的阻碍，尽管理论上有希望，但每个实现都存在重大缺陷，包括有限的结构和次优性能。我们相信通过纯粹的传统方法超越 AlphaGeometry 的证明能力可能是可行的，并希望我们的笔记鼓励改进该领域经典计算方法的当前软件。

另一方面，我们方法的显着成功表明，IMO 几何问题虽然对人类具有挑战性，但可能无法完全测试现代计算求解器的极限。重复应用人类定义的启发式方法并结合少量构造（之前已证明最多三个构造就足以[26])来取得成功，而不是对组合可能性进行深入、复杂的探索。这种情况让人想起国际象棋的残局，这些残局是由暴力求解器[14, 21]相对较早地掌握的。我们希望这篇文章能够鼓励几何自动定理证明者开发新的基准。

在我看来，《几何》感觉就像是国际象棋残局，固定的，回旋余地很小。

真正的乐趣在于教机器解决几何中局！

悉达多巴特

致谢

作者要感谢（按字母顺序排列）：Shashwat Goel、Shyamgopal Karthik、Yash Sharma、Matthias Tangemann、Saujas Vaduguru 对草案提供的有用反馈。 MB 感谢 Good Ventures 基金会资助的开放慈善基金会提供的财务支持。

参考

[1] Aimo prize. https://aimoprize.com/.
[2] Imo grand challenge. https://imo-grand-challenge.github.io/.
[3] Peter novotný’s masters thesis. https://skmo.sk/cvika/ukazpdf.php?pdf=diplomka.pdf.
Avigad et al. [2009] Jeremy Avigad, Edward Dean, and John Mumma. A formal system for euclid’s elements. The Review of Symbolic Logic, 2009.
Beeson et al. [2018] Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries, and Julien Narboux. Geocoq. 2018.
Chou et al. [2000] S.C. Chou, X.S. Gao, and J.Z. Zhang. A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning, 2000. doi: 10.1023/A:1006171315513.
Chou [1984] Shang-Ching Chou. Proving elementary geometry theorems using wu’s algorithm. In Woodrow Wilson Bledsoe and Donald W Loveland, editors, Automated Theorem Proving: After 25 Years, volume 89. American Mathematical Soc., 1984.
Chou [1988] Shang-Ching Chou. An introduction to wu’s method for mechanical theorem proving in geometry. Journal of Automated Reasoning, 1988.
Chou et al. [1995] Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang. Automated production of traditional proofs in solid geometry. Journal of Automated Reasoning, 14(2):257–291, 1995.
de Bruijn [1983] Nicolaas Govert de Bruijn. AUTOMATH, a language for mathematics. 1983.
Ferro et al. [1997] Giuseppa Carr‘a Ferro, Giovanni Gallo, and Rosario Gennaro. Probabilistic verification of elementary geometry statements. In Automated Deduction in Geometry, 1997. doi: 10.1007/BFb0022721.
Gelernter [1995] H. Gelernter. Realization of a geometry-theorem proving machine. Computers & Thought, 1995. doi: 10.5555/207644.207647.
[13] W. T. Gowers. How can it be feasible to find proofs? https://drive.google.com/file/d/1-FFa6nMVg18m1zPtoAQrFalwpx2YaGK4/view. Accessed: 7 April 2024.
Haworth [2005] Guy McCrossan Haworth. 6-man chess solved. ICGA Journal, 28(3):153–153, 2005.
Heath et al. [1956] Thomas Little Heath et al. The thirteen books of Euclid’s Elements. 1956.
Kapur [1986] Deepak Kapur. Using gröbner bases to reason about geometry problems. Journal of Symbolic Computation, 1986.
Kapur [1988] Deepak Kapur. A refutational approach to geometry theorem proving. Artificial Intelligence, 1988.
Kim [1989] Michelle Y. Kim. Visual reasoning in geometry theorem proving. In Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, 1989.
Kovács and Vujic [2024] Zoltán Kovács and Alexander Vujic. Open source prover in the attic. arXiv preprint arXiv:2401.13702, 2024.
Kovács et al. [2021] Zoltán Kovács, Tomas Recio, Luis F Tabera, and M Pilar Vélez. Dealing with degeneracies in automated theorem proving in geometry. Mathematics, 2021.
Nalimov et al. [2000] Eugene V Nalimov, G Haworth, and Ernst A Heinz. Space-efficient indexing of chess endgame tables. ICGA Journal, 23(3):148–162, 2000.
Nevins [1975] Arthur J Nevins. Plane geometry theorem proving using forward chaining. Artificial Intelligence, 6(1):1–23, 1975.
Richter-Gebert and Kortenkamp [1999] Jürgen Richter-Gebert and Ulrich Kortenkamp. The Interactive Geometry Software Cinderella. 1999.
Schindler and Chen [2012] Max Schindler and Evan Chen. Barycentric coordinates in olympiad geometry. Olympiad Articles, 2012.
[25] Justin Stevens. Coordinate and trigonometry bashing. http://services.artofproblemsolving.com/download.php?id=YXR0YWNobWVudHMvYi9kLzRmMTA5OWJhNmI1MTg2YzM2ODdkZTVhYTJjMGU0NjdmYmViNGRk&rn=Q29vcmRpbmF0ZSBhbmQgVHJpZ29ub21ldHJ5IEJhc2hpbmcucGRm. Accessed: 4 April 2024.
Trinh et al. [2024] Trieu H Trinh, Yuhuai Wu, Quoc V Le, He He, and Thang Luong. Solving olympiad geometry without human demonstrations. Nature, 2024.
Wang [1995] Dongming Wang. Reasoning about geometric problems using an elimination method. Automated practical reasoning: Algebraic approaches, pages 147–185, 1995.
Wen-Tsün [1978] Wu Wen-Tsün. On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica, 1978.
Wu [1986] Wenjun Wu. On zeros of algebraic equations–an application of ritt principle. Kexue Tongbao, 1986.
Ye et al. [2011] Z. Ye, S.C. Chou, and X.S. Gao. An introduction to java geometry expert – (extended abstract). 2011. doi: 10.1007/978-3-642-21046-4_10.

附录A详细比较

扩展比较。我们在 IMO-AG-30 基准 [26] 上与所有人工和自动化方法进行比较，如图 2 所示。我们的评估包括GPT4、全角度方法（FA）、格罗布纳基础（Gröbner）、演绎数据库（DD）、与代数规则相结合的演绎数据库以及GPT-4的增强构造建议（DD+AR+GPT4）。此外，我们还检查了 AlphaGeometry 模型的不同配置：一个仅对 1 亿个样本进行了预训练 (PT-100M)，另一个仅对 900 万个结构进行了微调 (FT-9M)。请注意，我们通过简单地并行运行 Wu 和 DD+AR 方法并在任一方法解决问题时停止来构建 Wu&DD+AR 基线。同样，我们构建 Wu&AlphaGeometry 基线。我们看到我们的 Wu&DD+AR 基线与 AG (FT-9M) 基线匹配，而 Wu 的方法单独与最好的 DD+AR+GPT4 算法匹配。

附录B插图：2008 P1B 和 2021 P3

我们提供了 Wu 的方法对 AlphaGeometry 无法解决的两个问题的解决方案的说明，以便进行额外的审查，而无需在 JGEX 求解器上重现相同的问题。