Oct, 2023
FormalGeo: 让几何自动推理接近人类水平的 IMO 级别的第一步
FormalGeo: The First Step Toward Human-like IMO-level Geometric Automated Reasoning
Xiaokai Zhang, Na Zhu, Yiming He, Jia Zou, Qike Huang...
TL;DR在过去十年的工作中，我们构建了一个完整且兼容的平面几何形式系统，该系统在 IMO 级别的平面几何挑战和可读的 AI 自动推理之间建立了重要的桥梁。通过这个形式系统，我们成功地将现代 AI 模型与形式系统无缝整合。在这个形式框架内，AI 能够像处理其他自然语言一样，为 IMO 级别的平面几何问题提供演绎推理解决方案，并且这些证明是可读、可追溯和可验证的。我们提出了几何形式化理论（GFT）来指导几何形式系统的发展。根据 GFT，我们构建了 FormalGeo，它包含 88 个几何谓词和 196 个定理，可以表示、验证和解决 IMO 级别的几何问题。我们还使用 Python 开发了 FGPS（形式几何问题解决器），它既可作为交互式助手验证问题解决过程，又可作为自动化问题解决器利用前向搜索、后向搜索和 AI 辅助搜索等多种方法。我们标注了 FormalGeo7k 数据集，其中包含 6,981 个几何问题的完整形式语言注释（通过数据增强扩展为 186,832 个问题）。对形式系统的实施和对 FormalGeo7k 的实验验证了 GFT 的正确性和实用性。后向深度优先搜索方法只有 2.42% 的问题解决失败率，而我们可以结合深度学习技术实现更低的失败率。FGPS 和 FormalGeo7k 数据集的源代码可在此 https URL 获取。