FormalGeo: An Extensible Formalized Framework for Olympiad Geometric Problem Solving
作者: Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang, Xiaoxiao Jin, Yanjun Guo, Chenyang Mao, Yang Li, Zhe Zhu, Dengfeng Yue, Fangzhen Zhu, Yifan Wang, Yiwen Huang, Runan Wang, Cheng Qin, Zhenbing Zeng, Shaorong Xie, Xiangfeng Luo, Tuo Leng
分类: cs.AI
发布日期: 2023-10-27 (更新: 2024-02-15)
备注: 44 pages
🔗 代码/项目: GITHUB
💡 一句话要点
构建FormalGeo框架以解决奥林匹克几何问题
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)
关键词: 几何问题求解 自动推理 形式化理论 AI模型 教育技术 数据集构建 深度学习
📋 核心要点
- 现有的几何问题求解方法在处理IMO级挑战时缺乏一致性和可读性，难以实现有效的自动推理。
- 论文提出了FormalGeo框架，通过几何形式化理论（GFT）整合现代AI模型，实现对IMO级几何问题的自动推理和验证。
- 实验结果表明，采用回溯深度优先搜索方法的求解失败率仅为2.42%，并且可以结合深度学习技术进一步降低该比例。
📝 摘要（中文）
本文是我们过去三年工作系列的第一篇论文，构建了一个一致的形式化平面几何系统，作为IMO级平面几何挑战与可读的AI自动推理之间的重要桥梁。在该框架内，我们成功整合了现代AI模型，使其能够提供IMO级平面几何问题的推理解决方案，且这些证明可读、可追溯和可验证。我们提出了几何形式化理论（GFT）以指导几何形式系统的发展，并建立了FormalGeo，包含88个几何谓词和196个定理，能够表示、验证和解决IMO级几何问题。此外，我们开发了FGPS（形式几何问题求解器），作为验证问题解决过程的交互助手和自动求解器。我们注释了formalgeo7k和formalgeo-imo数据集，前者包含6981个几何问题，后者包含18个IMO级挑战几何问题。实验验证了GFT的正确性和实用性。
🔬 方法详解
问题定义：本文旨在解决现有几何问题求解方法在IMO级挑战中的不足，特别是在一致性和可读性方面的挑战。
核心思路：通过构建FormalGeo框架，结合几何形式化理论（GFT），实现现代AI模型与形式几何系统的无缝集成，从而提供可读的推理解决方案。
技术框架：FormalGeo框架由88个几何谓词和196个定理组成，能够表示、验证和解决IMO级几何问题。FGPS作为核心模块，提供交互式验证和自动求解功能。
关键创新：最重要的创新在于将现代AI推理能力与形式几何系统结合，使得AI能够处理几何问题的推理过程，且结果可读、可追溯。
关键设计：FGPS的实现采用Python编写，设计了高效的回溯深度优先搜索算法，并注重数据集的注释和扩展，以确保问题的多样性和复杂性。
🖼️ 关键图片
📊 实验亮点
实验结果显示，FGPS采用的回溯深度优先搜索方法仅有2.42%的求解失败率，表明其在处理IMO级几何问题上的高效性和可靠性。结合深度学习技术的潜力，未来有望进一步降低失败率，提升求解能力。
🎯 应用场景
该研究的潜在应用领域包括教育、自动化推理系统和智能辅导工具。通过提供可读的几何推理，FormalGeo可以帮助学生更好地理解几何概念，并为教师提供辅助教学工具。此外，随着AI技术的发展，该框架可能在更广泛的数学问题求解中发挥重要作用。
📄 摘要（原文）
This is the first paper in a series of work we have accomplished over the past three years. In this paper, we have constructed a consistent formal plane geometry system. This will serve as a crucial bridge between IMO-level plane geometry challenges and readable AI automated reasoning. Within this formal framework, we have been able to seamlessly integrate modern AI models with our formal system. AI is now capable of providing deductive reasoning solutions to IMO-level plane geometry problems, just like handling other natural languages, and these proofs are readable, traceable, and verifiable. We propose the geometry formalization theory (GFT) to guide the development of the geometry formal system. Based on the GFT, we have established the FormalGeo, which consists of 88 geometric predicates and 196 theorems. It can represent, validate, and solve IMO-level geometry problems. we also have crafted the FGPS (formal geometry problem solver) in Python. It serves as both an interactive assistant for verifying problem-solving processes and an automated problem solver. We've annotated the formalgeo7k and formalgeo-imo datasets. The former contains 6,981 (expand to 133,818 through data augmentation) geometry problems, while the latter includes 18 (expand to 2,627 and continuously increasing) IMO-level challenging geometry problems. All annotated problems include detailed formal language descriptions and solutions. Implementation of the formal system and experiments validate the correctness and utility of the GFT. The backward depth-first search method only yields a 2.42% problem-solving failure rate, and we can incorporate deep learning techniques to achieve lower one. The source code of FGPS and datasets are available at https://github.com/BitSecret/FGPS.