Geometric problem solving has always been a long-standing challenge in the fields of automated reasoning and artificial intelligence. We built a neural-symbolic system to automatically perform human-like geometric deductive reasoning. The symbolic part is a formal system built on FormalGeo, which can automatically perform geomertic relational reasoning and algebraic calculations and organize the solving process into a solution hypertree with conditions as hypernodes and theorems as hyperedges. The neural part, called HyperGNet, is a hypergraph neural network based on the attention mechanism, including a encoder to effectively encode the structural and semantic information of the hypertree, and a solver to provide problem-solving guidance. The neural part predicts theorems according to the hypertree, and the symbolic part applies theorems and updates the hypertree, thus forming a predict-apply cycle to ultimately achieve readable and traceable automatic solving of geometric problems. Experiments demonstrate the correctness and effectiveness of this neural-symbolic architecture. We achieved a step-wised accuracy of 87.65% and an overall accuracy of 85.53% on the formalgeo7k datasets.

翻译：几何问题求解一直是自动推理和人工智能领域的长期挑战。我们构建了一个神经符号系统，用于自动执行类人的几何演绎推理。符号部分是基于FormalGeo构建的形式化系统，能够自动进行几何关系推理和代数计算，并将求解过程组织为以条件为超节点、以定理为超边的求解超树。神经部分称为HyperGNet，是基于注意力机制的超图神经网络，包含一个编码器以有效编码超树的结构和语义信息，以及一个求解器以提供问题求解指导。神经部分根据超树预测定理，符号部分应用定理并更新超树，从而形成“预测-应用”循环，最终实现几何问题的可读、可追溯的自动求解。实验证明了该神经符号架构的正确性和有效性。在formalo7k数据集上，我们实现了87.65%的步骤级准确率和85.53%的整体准确率。