Feb, 2024

FGeo-TP: 几何问题的语言模型增强求解器

PDF
TL;DR应用现代人工智能技术解决几何问题和自动演绎证明一直以来都是数学和人工智能交叉领域的重要挑战。本文提出了一种名为 FGeo-P 的定理预测器，利用语言模型预测几何问题的定理序列，从而提高了解决几何问题的性能，实验证明在 FormalGeo7k 数据集的问题解决率从 39.7% 提升至 80.86%。此外，FGeo-TP 在不同难度问题上表现出了解决时间和搜索步骤显著减少的特点。
artificial intelligence techniquesgeometric problemsautomated deductive proofformalgeofgeo-tp
发现论文，激发创造
  • FormalGeo: 让几何自动推理接近人类水平的 IMO 级别的第一步

    在过去十年的工作中，我们构建了一个完整且兼容的平面几何形式系统，该系统在 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 获取。

    Oct, 2023

  • FGeo-HyperGNet: 几何问题求解正式符号系统与超图神经网络的整合

    我们构建了一种神经符号系统，利用神经部分（HyperGNet）根据超树预测定理，并利用符号部分（FormalGeo）应用定理和更新超树，从而形成了一个可追踪的、可读的几何问题自动求解的预测 - 应用循环，实现了 87.65% 的逐步准确率和 85.53% 的总体准确率。

    Feb, 2024

  • Inter-GPS: 可解释的几何问题求解与形式化语言及符号推理

    构建了一个大规模的几何问题的数据集，并提出了一种基于形式语言和符号推理的新的解决方案，称为可解释几何问题求解器 (Inter-GPS)，其能够显著提高当前方法的解决几何问题的效果。

    May, 2021

  • 用于自动定理证明的生成语言建模

    本文探讨了基于 Transformer 的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一 —— 原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具 GPT-f，使用 Metamath 形式语言，并分析了其性能。 GPT-f 发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。

    Sep, 2020

  • FGeo-DRL：通过深度增强学习进行几何问题的演绎推理

    本文介绍了一个名为 FGeoDRL 的神经符号系统，用于自动执行类似人类的几何演绎推理。该系统通过强化学习建立策略网络进行定理选择，并使用蒙特卡洛树搜索进行启发式探索。实验结果表明，在形式化数据集上，FGeoDRL 实现了 86.40％的几何问题求解成功率。

    Feb, 2024

  • 多模态神经几何求解器：从图解析文本子句

    本文提出了一种基于神经网络的解题方案 PGPSNet 来解决几何问题求解中的模态融合问题；通过把图解转化成文本描述来更有效地描述数据特征，并结合结构和语义训练、数据增强和自限制解码等来增强几何理解和推理。此外，还构建了一个新的大规模、细粒度的 PGPS9K 数据库来帮助该领域的研究。我们在 PGPS9K 和 Geometry3K 数据集上的实验验证了该方法的优越性。

    Feb, 2023

  • GOLD: 几何问题解决器与自然语言描述

    通过分别处理图形符号和几何基元来增强几何关系的提取，并将提取的关系转化为自然语言描述，从而高效利用大型语言模型解决几何数学问题。实验证明，GOLD 模型在 UniGeo 数据集上表现优于 Geoformer，并分别在计算和证明子集中提高了 12.7% 和 42.1% 的准确率。此外，在 PGPS9K 和 Geometry3K 数据集上也优于 PGPSNet，分别获得了 1.8% 和 3.2% 的准确率提升。

    May, 2024

  • UniGeo: 通过重构数学表达式统一几何逻辑推理

    本文介绍了一个基于多任务转换器框架 Geoformer 的大规模统一几何问题基准测试 UniGeo，通过共同表达式生成的方式统一解决计算和证明问题，并提出了预测数学表达式的方法 MEP，从而提高了 Geoformer 的性能。

    Dec, 2022

  • GAPS: 几何感知问题求解器

    通过提出几何感知问题求解器（GAPS）模型，我们解决了几何问题求解中的挑战，该模型以其独特的问题类型分类器为帮助，生成不同类型几何数学问题的解决方案程序。借助 GAPS 对几何元素进行准确识别的改进，我们展示了其在解决几何数学问题方面的优越性能。在 UniGeo 数据集上的实验证明了 GAPS 模型在计算任务上超过 Geoformer 模型 5.3% 的准确率提升以及在证明任务上惊人的 41.1% 提升，特别是在证明问题上达到令人印象深刻的 97.5% 准确率，为几何证明任务的解决带来了重要进展。

    Jan, 2024

  • 通过模拟人类双重推理过程学习解决几何问题

    提出了一个名为 DualGeoSolver 的双重推理几何求解器，通过模拟人类的双重推理过程，从对人类推理过程和知识应用的显式建模中提高求解几何问题的准确率和鲁棒性。

    May, 2024