GAPS: 几何感知问题求解器
内容提要
本文综述自动求解数学问题的进展，聚焦几何题，涵盖语义鸿沟、形式语言与符号推理、神经网络与多模态融合、大规模数据集（Geometry3K、PGPS9K、GeoQA、UniGeo、Geo170K、FormalGeo7k）及求解器（Inter-GPS、PGPSNet、NGS、Geoformer、G-LLaVA、LANS、FGPS），并评估视觉语言模型的推理能力。
延伸解读
几何自动求解的技术演进
文章梳理了从2018年到2023年几何自动求解的发展脉络：早期Inter-GPS基于形式语言和符号推理，随后PGPSNet引入神经网络解决模态融合，NGS和Geoformer进一步结合多模态与统一框架，G-LLaVA和LANS则利用大语言模型和布局感知技术。这一演进反映了从符号推理到神经符号融合，再到多模态大模型驱动的趋势，逐步提升了几何问题的求解能力和可解释性。
数据集推动研究进展
文章提及多个大规模几何数据集：Geometry3K、PGPS9K、GeoQA、UniGeo、Geo170K和FormalGeo7k。这些数据集覆盖不同规模、任务类型（计算与证明）和标注形式（自然语言与形式语言），为模型训练和评估提供了基础。例如，FormalGeo7k包含6,981个问题的完整形式语言注释，并通过数据增强扩展至186,832个问题，支持形式化推理研究。数据集的丰富化直接促进了求解器性能的提升。
视觉语言模型的推理局限
文章指出，尽管大语言模型在多步数学推理上表现出色，但视觉语言模型在几何问题上的推理能力并不如先前基准测试所暗示的那样强。通过构建可控难度的合成几何数据集进行评估，发现解决更深层问题需要更长的推理链，而非依赖额外记忆知识。这表明当前模型在复杂几何推理上仍有不足，需进一步研究提升其深度推理能力。
形式化系统与可解释性
文章介绍了平面几何形式系统FormalGeo，包含88个几何谓词和196个定理，能够表示、验证和解决IMO级别几何问题。基于此开发的FGPS求解器支持交互式验证和自动求解，结合前向搜索、后向搜索和AI辅助搜索。后向深度优先搜索的失败率仅2.42%，结合深度学习可进一步降低。形式化方法不仅提高了求解成功率，还使证明过程可读、可追溯和可验证，增强了AI推理的可解释性。
Q&A
自动求解几何问题面临哪些主要挑战？
主要挑战包括语言和逻辑之间的语义鸿沟，以及需要融合多模态信息（如文本和图像）进行推理。
有哪些大规模几何问题数据集可用于训练AI模型？
常用数据集包括Geometry3K、PGPS9K、GeoQA、UniGeo、Geo170K和FormalGeo7k等。
Inter-GPS求解器是如何工作的？
Inter-GPS基于形式语言和符号推理，能够显著提高几何问题的求解效果，并具有可解释性。
G-LLaVA模型在几何问题求解上表现如何？
G-LLaVA利用图像输入理解几何问题，在MathVista基准测试上以仅有7B参数显著优于GPT-4-V。
LANS求解器有哪些创新模块？
LANS集成了多模态布局感知预训练语言模型(MLA-PLM)和布局感知融合注意力(LA-FA)，通过全局关系建模和对齐实现布局感知。
FormalGeo形式系统包含哪些内容？
FormalGeo包含88个几何谓词和196个定理，可以表示、验证和解决IMO级别的几何问题。
视觉语言模型在几何推理上的表现如何？
基准测试表明，这些模型在几何等主题的推理能力上并不如先前基准测试所暗示的那样出色，解决更深的问题需要更长的推理链。
