-
题名面向前提选择的新型图约简表示与图神经网络模型
- 1
-
-
作者
兰咏琪
何星星
李莹芳
李天瑞
-
机构
西南交通大学数学学院
西南财经大学计算机与人工智能学院
西南交通大学计算机与人工智能学院
-
出处
《计算机科学》
CSCD
北大核心
2024年第5期193-199,共7页
-
基金
中央高校基本科研业务费专项资金(2682020ZT107)
国家自然科学基金(62106206)
+1 种基金
教育部人文社科项目(19YJCZH048,20XJCZH016)
四川省科技计划(2023YFH0066)。
-
文摘
自动定理证明器在证明问题时其搜索空间通常会呈现爆炸式增长,前提选择为该问题提供了新的解决思路。针对现有前提选择方法中逻辑公式图、图神经网络模型难以捕捉到公式图潜在信息的问题,提出了一种基于删除重复量词的简化逻辑公式图表示和具有注意力机制的项游走图神经网络模型,充分利用逻辑公式的语法和语义信息提高前提选择问题的分类精度。首先,将一阶逻辑猜想和前提公式转化为基于删除重复量词的简化一阶逻辑公式图;其次,利用消息传递图神经网络对节点和节点的项游走特征信息进行聚合和更新,随后使用注意力机制为图上的节点分配权重,进而调整图节点嵌入信息;最后,将前提图向量和猜想图向量拼接并输入二元分类器中实现前提分类。实验结果表明,所提方法在MPTP数据集和CNF数据集上的准确率分别达到了88.61%和84.74%,超越现有最优的前提选择方法。
-
关键词
图神经网络
前提选择
注意力机制
一阶逻辑公式
图约简表示方法
-
Keywords
Graph neural network
Premise selection
Attention mechanism
First order logical formula
Graph reduction representation
-
分类号
TP391
[自动化与计算机技术—计算机应用技术]
-
