面向前提选择的新型图约简表示与图神经网络模型

作者：兰咏琪; 何星星; 李莹芳^*; 李天瑞

来源：计算机科学, 2023, 1-12.

• 图神经网络
• 前提选择
• 注意力机制
• 一阶逻辑公式
• 图约简表示方法

自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长，前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题，提出一种基于删除重复量词的简化逻辑公式图表示和具有注意力机制的项游走图神经网络模型，充分利用逻辑公式的语法和语义信息提高前提选择问题的分类精度。首先，将一阶逻辑猜想和前提公式转化为基于删除重复量词的简化一阶逻辑公式图；其次，利用消息传递图神经网络对节点和节点的项游走特征信息进行聚合和更新，随后使用注意力机制为图上的节点分配权重，进而调整图节点嵌入信息；最后，将前提图向量和猜想图向量拼接输入到二元分类器中实现前提分类。实验结果表明，本文所使用的方法在MPTP数据集和CNF数据集上的准确率分别达到了88.61%和84.74%，超越现有最优的前提选择方法。

• 单位
  西南交通大学; 数学学院; 西南财经大学