FGeo-TP: 几何问题的语言模型增强求解器
内容提要
本文介绍平面几何形式系统FormalGeo，包含88个谓词和196个定理，可表示、验证并解决IMO级几何题。配套FGPS求解器支持前后向搜索与AI辅助，FormalGeo7k数据集含6981题，后向搜索失败率仅2.42%。系统实现AI与形式推理结合，证明可读可验证，推动可解释几何自动推理发展。
延伸解读
形式系统与AI的融合方式
文章指出，FormalGeo形式系统将现代AI模型与形式推理无缝整合。AI能够像处理自然语言一样，为IMO级几何问题提供演绎推理解决方案，且证明过程可读、可追溯、可验证。这种融合不是简单替换，而是让AI在形式框架内工作，从而兼顾灵活性与严谨性。
求解器性能与可扩展性
FGPS求解器支持前向搜索、后向搜索和AI辅助搜索。实验显示，后向深度优先搜索的失败率仅为2.42%，而结合深度学习技术可进一步降低失败率。这表明符号推理与学习方法的结合能有效提升几何问题求解的鲁棒性，并为未来优化留下空间。
数据集规模与增强策略
FormalGeo7k数据集包含6,981个几何问题的完整形式语言注释，并通过数据增强扩展为186,832个问题。这种大规模标注与增强为训练和评估几何自动推理系统提供了丰富资源，也验证了几何形式化理论（GFT）的正确性和实用性。
Q&A
FormalGeo 形式系统包含哪些核心组件？
FormalGeo 包含 88 个几何谓词和 196 个定理，可以表示、验证和解决 IMO 级别的几何问题。
FGPS 求解器支持哪些问题解决方式？
FGPS 支持前向搜索、后向搜索和 AI 辅助搜索等多种方法，既可作为交互式助手验证问题解决过程，也可作为自动化问题解决器。
FormalGeo7k 数据集包含多少题目？
FormalGeo7k 数据集包含 6,981 个几何问题的完整形式语言注释，通过数据增强可扩展为 186,832 个问题。
后向深度优先搜索在 FormalGeo7k 上的失败率是多少？
后向深度优先搜索方法只有 2.42% 的问题解决失败率。
几何形式化理论（GFT）的作用是什么？
GFT 用于指导几何形式系统的发展，FormalGeo 的构建基于 GFT，实验验证了 GFT 的正确性和实用性。
AI 与形式系统结合后，几何证明具有哪些特性？
AI 能够为 IMO 级别的平面几何问题提供演绎推理解决方案，这些证明是可读、可追溯和可验证的。
