基于边权重图神经网络的一阶逻辑前提选择

为提高自动定理证明器在大规模问题中证明问题的能力，前提选择任务应运而生. 由于公式图的有向性，主流的图神经网络框架只能单向地对节点进行更新，且无法编码公式图中子节点间的顺序. 针对以上问题，提出了带有边类型的双向公式图表示方法，并提出了一种基于边权重的图神经网络（edge-weight-based graph neural network，EW-GNN）模型用于编码一阶逻辑公式. 该模型首先利用相连节点的信息来更新对应边类型的特征表示，随后利用更新后的边类型特征计算邻接节点对中心节点的权重，最后利用邻接节点的信息双向地对中心节点进行更新. 实验比较分析表明:基于边权重的图神经网络模型在前提选择任务中表现得更加优越，其在相同的测试集上比当前最优模型的分类准确率高了约1%. 

Edge-Weighted-Based Graph Neural Network for First-Order Premise Selection

In order to improve the ability of automated theorem provers, the premise selection task emerges. Due to the directional nature of formula graphs, most current graph neural networks can only update nodes in one direction, and cannot encode the order of sub-nodes in the formula graph. To address the above problems, a bidirectional graph with edge types to represent logical formulae and a edge-weight-based graph neural network (EW-GNN) model to encode first-order logic formulae are proposed. The model firstly uses the information of connected nodes to update the feature representation of the corresponding edge type, then calculates the weight of the adjacent node to the central node with the updated edge type feature, and finally uses the information of the adjacent node to update the target node in both directions. The experimental results show the edge-weighted-based graph neural network model performs better in the premise selection task, which can improve the classification accuracy by 1% compared to the best model on the same test dataset.