Proposing and solving olympiad geometry with guided tree search
作者: Chi Zhang, Jiajun Song, Siyu Li, Yitao Liang, Yuxi Ma, Wei Wang, Yixin Zhu, Song-Chun Zhu
分类: cs.AI, cs.LG
发布日期: 2024-12-14
💡 一句话要点
TongGeometry系统通过引导树搜索提出并解决奥林匹克几何问题。
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 几何定理发现 自动推理 树搜索 大型语言模型 奥林匹克几何
📋 核心要点
- 现有几何自动推理系统在定理发现和证明方面存在挑战，尤其是在涉及数值和空间元素的几何问题中。
- TongGeometry系统利用树搜索算法，并结合大型语言模型进行引导，从而实现几何问题的自动提出和解决。
- 实验结果表明，TongGeometry在奥林匹克几何问题上超越了现有技术，并在定理发现方面取得了显著成果。
📝 摘要（中文）
本文介绍了一种名为TongGeometry的欧几里得几何系统，该系统支持基于树搜索的引导式问题提出和解决。该系统建立了迄今为止最广泛的几何定理库：在与现有技术水平相当的计算预算内，TongGeometry发现了67亿个需要辅助构造的几何定理，其中包括41亿个表现出几何对称性的定理。其中，10个定理被提交给区域数学奥林匹克竞赛，TongGeometry的3个提案在实际比赛中被选中，获得了中国和美国国家队资格考试或顶级民间奥林匹克竞赛的参赛资格。在经过微调的大型语言模型的指导下，TongGeometry解决了IMO-AG-30中的所有国际数学奥林匹克几何问题，首次超过了金牌获得者。它还在更广泛的奥林匹克级别问题上超越了现有的技术水平。该系统的全部功能可以在消费级机器上使用，从而使该模型更易于访问，并促进其使用的广泛民主化。与仅仅像学生一样解决问题的现有系统不同，TongGeometry就像一位几何教练，发现、呈现和证明定理。
🔬 方法详解
问题定义：论文旨在解决奥林匹克级别的几何问题，包括自动提出问题和自动求解问题。现有方法在定理发现的数量和质量上存在不足，尤其是在需要辅助线构造和涉及复杂几何关系的场景下，难以达到奥林匹克竞赛的要求。
核心思路：论文的核心思路是利用树搜索算法探索几何定理空间，并使用大型语言模型对搜索过程进行引导。通过这种方式，系统能够高效地发现大量有意义的几何定理，并能够解决复杂的几何问题。这种结合了符号推理和数值计算的方法，能够更好地处理几何问题中的空间关系和数值约束。
技术框架：TongGeometry系统主要包含以下几个模块：1) 几何定理生成器：负责生成新的几何定理，基于已有的定理和公理，通过演绎推理生成新的几何关系。2) 几何定理验证器：负责验证生成的定理的正确性，采用数值验证和符号验证相结合的方式。3) 问题生成器：基于已验证的定理，生成具有挑战性的几何问题。4) 问题求解器：利用树搜索算法，结合几何推理规则和数值计算，求解生成的几何问题。5) 大型语言模型引导模块：利用大型语言模型对树搜索过程进行引导，提高搜索效率和定理质量。
关键创新：论文的关键创新在于将大型语言模型引入到几何定理发现和证明的过程中。大型语言模型能够理解几何问题的语义信息，并能够提供有用的启发式信息，从而引导树搜索过程，提高搜索效率和定理质量。此外，系统还采用了高效的几何定理验证方法，能够快速验证生成的定理的正确性。
关键设计：在树搜索算法中，论文采用了A*搜索算法，并使用大型语言模型预测的定理重要性作为启发式函数。在几何定理验证中，论文采用了数值验证和符号验证相结合的方式，首先使用数值验证快速排除错误的定理，然后使用符号验证对剩余的定理进行严格证明。大型语言模型采用经过微调的模型，使其能够更好地理解几何问题的语义信息，并能够提供更准确的启发式信息。
🖼️ 关键图片
📊 实验亮点
TongGeometry系统发现了67亿个需要辅助构造的几何定理，其中包括41亿个表现出几何对称性的定理。在IMO-AG-30测试集中，TongGeometry首次超越了金牌获得者。此外，TongGeometry的3个提案在实际奥林匹克竞赛中被选中，获得了国家队资格考试或顶级民间奥林匹克竞赛的参赛资格。这些结果表明，TongGeometry系统在几何定理发现和问题求解方面取得了显著进展。
🎯 应用场景
TongGeometry系统可应用于几何教育、自动定理发现、几何问题求解等领域。该系统能够帮助学生更好地理解几何概念，提高解题能力。同时，该系统也可以作为研究工具，帮助数学家发现新的几何定理，推动几何学的发展。此外，该系统还可以应用于工程设计、计算机图形学等领域，解决实际问题。
📄 摘要（原文）
Mathematics olympiads are prestigious competitions, with problem proposing and solving highly honored. Building artificial intelligence that proposes and solves olympiads presents an unresolved challenge in automated theorem discovery and proving, especially in geometry for its combination of numerical and spatial elements. We introduce TongGeometry, a Euclidean geometry system supporting tree-search-based guided problem proposing and solving. The efficient geometry system establishes the most extensive repository of geometry theorems to date: within the same computational budget as the existing state-of-the-art, TongGeometry discovers 6.7 billion geometry theorems requiring auxiliary constructions, including 4.1 billion exhibiting geometric symmetry. Among them, 10 theorems were proposed to regional mathematical olympiads with 3 of TongGeometry's proposals selected in real competitions, earning spots in a national team qualifying exam or a top civil olympiad in China and the US. Guided by fine-tuned large language models, TongGeometry solved all International Mathematical Olympiad geometry in IMO-AG-30, outperforming gold medalists for the first time. It also surpasses the existing state-of-the-art across a broader spectrum of olympiad-level problems. The full capabilities of the system can be utilized on a consumer-grade machine, making the model more accessible and fostering widespread democratization of its use. By analogy, unlike existing systems that merely solve problems like students, TongGeometry acts like a geometry coach, discovering, presenting, and proving theorems.