摘要
自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了一种基于删除重复量词的简化逻辑公式图表示和具有注意力机制的项游走图神经网络模型,充分利用逻辑公式的语法和语义信息提高前提选择问题的分类精度。首先,将一阶逻辑猜想和前提公式转化为基于删除重复量词的简化一阶逻辑公式图;其次,利用消息传递图神经网络对节点和节点的项游走特征信息进行聚合和更新,随后使用注意力机制为图上的节点分配权重,进而调整图节点嵌入信息;最后,将前提图向量和猜想图向量拼接并输入二元分类器中实现前提分类。实验结果表明,所提方法在MPTP数据集和CNF数据集上的准确率分别达到了88.61%和84.74%,超越现有最优的前提选择方法。
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 classification accuracy of premise selection problems.Firstly,the conjecture formulas and premise formulas are transformed into simplified first-order logic formula graphs based on removing repeated quantifiers.Secondly,the message passing graph neural network 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 surpasses the existing premise selection method.
作者
兰咏琪
何星星
李莹芳
李天瑞
LAN Yongqi;HE Xingxing;LI Yingfang;LI Tianrui(School of Mathematics,Southwest Jiaotong University,Chengdu 611756,China;School of Computer and Artificial Intelligence,Southwestern University of Finance and Economics,Chengdu 611130,China;School of Computer and Artificial Intelligence,Southwest Jiaotong University,Chengdu 611756,China)
出处
《计算机科学》
CSCD
北大核心
2024年第5期193-199,共7页
Computer Science
基金
中央高校基本科研业务费专项资金(2682020ZT107)
国家自然科学基金(62106206)
教育部人文社科项目(19YJCZH048,20XJCZH016)
四川省科技计划(2023YFH0066)。
关键词
图神经网络
前提选择
注意力机制
一阶逻辑公式
图约简表示方法
Graph neural network
Premise selection
Attention mechanism
First order logical formula
Graph reduction representation
