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

几何问题求解最近在自然语言处理（NLP）社区引起了广泛关注。这一任务具有挑战性，因为它需要对抽象问题的理解以及基于公理知识的符号推理。然而，当前的数据集要么规模较小，要么未公开可用。因此，我们构建了一个新的大规模基准数据集——Geometry3K，包含3,002个带有密集形式语言注释的几何问题。我们进一步提出了一种基于形式语言和符号推理的新颖几何求解方法，称为可解释几何问题求解器（Inter-GPS）。Inter-GPS首先通过基于规则的文本解析和神经对象检测分别自动将问题文本和图形解析为形式语言。与现有方法中的隐式学习不同，Inter-GPS将定理知识作为条件规则纳入其中，并逐步进行符号推理。此外，设计了一个定理预测器来推断定理应用序列，从而为符号求解器提供更高效和合理的搜索路径。在Geometry3K和GEOS数据集上的大量实验表明，Inter-GPS相比现有方法取得了显著改进。该项目的代码和数据可在https://lupantech.github.io/inter-gps 获取。