FGeo-DRL：通过深度增强学习进行几何问题的演绎推理
内容提要
该研究提出几何形式化理论GFT，构建兼容的平面几何形式系统，开发了包含88个谓词、196个定理的FormalGeo及求解器FGPS，可表示、验证并解决IMO级几何问题。团队标注了含6981个完整形式化问题的FormalGeo7k数据集，增强后达186832个。实验表明GFT正确实用，后向深度优先搜索失败率仅2.42%，结合深度学习可进一步降低。
延伸解读
几何形式化系统的构建与验证
文章提出了几何形式化理论（GFT），并基于此构建了FormalGeo系统，包含88个几何谓词和196个定理，能够表示、验证和解决IMO级别的几何问题。通过开发FGPS求解器和标注FormalGeo7k数据集（含6981个完整形式化问题，增强后达186832个），实验验证了GFT的正确性和实用性。后向深度优先搜索的失败率仅为2.42%，结合深度学习可进一步降低失败率。
AI与形式系统整合的意义
该研究将现代AI模型与形式系统无缝整合，使AI能够为IMO级别的平面几何问题提供可读、可追溯和可验证的演绎推理解决方案。这为自动推理与人类可读证明之间建立了桥梁，有助于推动数学与人工智能交叉领域的发展。
数据集与求解器的开源贡献
FGPS和FormalGeo7k数据集的源代码已公开，为后续研究提供了可复现的基础。FormalGeo7k包含6981个几何问题的完整形式语言注释，并通过数据增强扩展至186832个问题，有助于训练和评估几何定理证明模型。
Q&A
FGeo-DRL 是什么？它主要解决什么问题？
FGeo-DRL 是一个通过深度强化学习进行几何问题演绎推理的研究项目。它旨在将现代 AI 模型与平面几何形式系统无缝整合，使 AI 能够为 IMO 级别的平面几何问题提供可读、可追溯和可验证的演绎推理解决方案。
几何形式化理论（GFT）是什么？它有什么作用？
几何形式化理论（GFT）是指导几何形式系统发展的理论框架。根据 GFT，研究者构建了 FormalGeo，它包含 88 个几何谓词和 196 个定理，可以表示、验证和解决 IMO 级别的几何问题。
FormalGeo7k 数据集包含多少问题？数据增强后规模如何？
FormalGeo7k 数据集包含 6,981 个几何问题的完整形式语言注释，通过数据增强扩展为 186,832 个问题。
FGPS 是什么？它有哪些功能？
FGPS（形式几何问题解决器）是用 Python 开发的工具，既可作为交互式助手验证问题解决过程，又可作为自动化问题解决器，利用前向搜索、后向搜索和 AI 辅助搜索等多种方法。
后向深度优先搜索在几何问题求解中的失败率是多少？
后向深度优先搜索方法只有 2.42% 的问题解决失败率，而结合深度学习技术可以实现更低的失败率。
FGeo-P 是什么？它在几何问题求解上取得了什么效果？
FGeo-P 是一种定理预测器，利用语言模型预测几何问题的定理序列。实验证明，在 FormalGeo7k 数据集上，问题解决率从 39.7% 提升至 80.86%。
