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

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

扫码查看
原文链接
  • 万方数据
  • 维普
自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路.针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了 一种基于删除重复量词的简化逻辑公式图表示和具有注意力机制的项游走图神经网络模型,充分利用逻辑公式的语法和语义信息提高前提选择问题的分类精度.首先,将一阶逻辑猜想和前提公式转化为基于删除重复量词的简化一阶逻辑公式图;其次,利用消息传递图神经网络对节点和节点的项游走特征信息进行聚合和更新,随后使用注意力机制为图上的节点分配权重,进而调整图节点嵌入信息;最后,将前提图向量和猜想图向量拼接并输入二元分类器中实现前提分类.实验结果表明,所提方法在MPTP数据集和CNF数据集上的准确率分别达到了 88.61％和84.74％,超越现有最优的前提选择方法.
New Graph Reduction Representation and Graph Neural Network Model for Premise Selection
The search space of an automatic theorem prover usually grow explosively when it proves problems.Premise selection provides a new solution to this problem.Aiming at the problem that the logical formula graph and graph neural network models in the existing premise selection methods are difficult to capture the potential information of the formula graph,this paper proposes a simplified logical formula graph representation based on removing repeated quantifiers and a term-walk graph neural network with attention mechanism,which makes full use of the syntactic and semantic information of logical formulas to improve the clas-sification accuracy of premise selection problems.Firstly,the conjecture formulas and premise formulas are transformed into sim-plified first-order logic formula graphs based on removing repeated quantifiers.Secondly,the message passing graph neural net-work is used to aggregate and update nodes and their term walk feature information,and then the attention mechanism is used to assign weights to nodes on the graph,so as to adjust the graph nodes embedding information.Finally,the premise vector and the conjecture vector are concatenated and input into the binary classifier to realize the classification.Experimental results show that the accuracy of the proposed method on MPTP dataset and CNF dataset reaches 88.61％and 84.74％,respectively,which sur-passes the existing premise selection method.

Graph neural networkPremise selectionAttention mechanismFirst order logical formulaGraph reduction represen-tation

兰咏琪、何星星、李莹芳、李天瑞

展开 >

西南交通大学数学学院 成都 611756

西南财经大学计算机与人工智能学院 成都 611130

西南交通大学计算机与人工智能学院 成都 611756

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

中央高校基本科研业务费专项国家自然科学基金教育部人文社会科学研究项目教育部人文社会科学研究项目四川省科技计划

2682020ZT1076210620619YJCZH04820XJCZH0162023YFH0066

2024

10.11896/jsjkx.230300193

计算机科学
重庆西南信息有限公司（原科技部西南信息中心）

计算机科学

CSTPCD北大核心
影响因子：0.944
ISSN：1002-137X
年,卷(期)：2024.51(5)
  • 28