一阶逻辑中基于treelet图神经网络的前提选择

马 雪,何星星,兰咏琪,李莹芳

(1.西南交通大学数学学院,四川 成都 611756;2.西南财经大学计算机与人工智能学院,四川 成都 611130)

1 引言

自动推理是人工智能研究领域中的一个重要方向,其目标是利用计算机实现人类的推理过程。自动定理证明是自动推理领域中的重要课题,其任务是研究自动化系统的设计,利用设计的系统对数学中提出的定理或猜想进行推理和证明[1]。其研究成果已成功应用于多个实际领域,如操作系统[2,3]、分布式系统[4,5]、编译器[6,7]、微处理器设计[8]和数学问题的求解[9]等。

当推理规则确定后,自动定理证明本质上是一个搜索问题,其目标是寻找从前提集到给定的定理或猜想的一个演绎序列。经典的自动定理证明器ATPs(Automatic Theorem Provers)对于解决需要在较小的公理集上执行复杂的推理步骤的问题是有效的,然而,对于一些包含数百到数千万个公理的问题,证明它们时搜索空间呈爆炸型增长,超出了自动定理证明器的能力,并且大型知识库中通常只有一小部分公理与给定的定理或猜想的证明相关。随着大型逻辑理论的研究变得越来越广泛[10-12],这种缺陷变得更加明显。前提选择是避免这种缺陷的有效方法,其任务是在证明器的预处理阶段,选择对给定的定理或猜想的证明有用的公理,这对缩小搜索空间,提高ATPs的性能发挥了关键作用。

前提选择的研究最早是基于比较和分析符号手工设计启发式方法[13]。随后,机器学习方法提供了一些替代方案,如朴素贝叶斯方法[14]、K近邻算法[15]等。Alama等[16]使用词袋特征训练了一个基于内核的分类器,取得了很好的实验结果。Alama等[17]首次将深度学习应用于大规模理论的前提选择,有效避免了机器学习中依赖大量手工设计的特征。该方法利用长短期记忆网络LSTM(Long Short-Term Memory)[18]和GRU(Gated Recurrent Unit)[19]对成对的公理和猜想进行训练,以确定最有可能与自动证明相关的公理,该模型在Mizar语料库的前提选择任务中取得了良好的效果。

目前,前提选择与深度学习的融合研究得到了较大发展[20-22],然而,逻辑公式的复杂性和结构化性质使其继续发展具有挑战性。2种最常用的保持公式结构性质的方法是Tree LSTM[18]和GNN(Graph Neural Network)[19]。当将逻辑公式表示为解析树时,Tree LSTM 会生成表示全局解析树的嵌入,但它们会遗漏逻辑公式中重要的信息,如共享子表达式等。相反,GNN能有效地捕捉共享子表达式,且由于逻辑公式可以转化为有向无环图DAG(Directed Acyclic Graph),GNN与前提选择结合势必有更广泛的应用前景。然而,主流图神经网络通过对图中单个节点的嵌入进行简单池化生成最终公式的图嵌入,其中每个节点仅包含了自身与邻居节点的信息,缺乏了表征一阶逻辑公式内部语义与语法的信息,如逻辑公式图(逻辑公式经转化得到的图)上的节点顺序信息等。

为解决图神经网络进行节点更新时忽略了节点顺序信息的问题,Wang等[23]提出一种面向高阶逻辑的保序方法,由于高阶逻辑公式中常元与变元可以作为值或函数,这与一阶逻辑公式不同,故该方法不适用于一阶逻辑。基于此,本文提出一阶逻辑保留逻辑公式图上节点顺序信息的方法,并基于此方法设计了适用于一阶逻辑公式前提选择任务的基于treelet的图神经网络TL-GNN(TreeLet-based Graph Neural Network)模型。实验分析表明：在相同的测试集上,与主流图神经网络模型相比,TL-GNN提高了约2% 的分类准确率;与同样为编码逻辑公式图的子节点顺序的图神经网络模型EW-GNN(Edge-Weighted Graph Neural Network)[24]相比,TL-GNN可提高约1%的分类准确率。

2 相关工作

2.1 一阶逻辑公式图表示

定义1[25]一阶逻辑中的项,被递归定义为：

(1)常量符号是项。

(2)变量符号是项。

(3)若f是n元函数符号,t1,t2,…,tn是项,则f(t1,t2,…,tn)是项。

(4)所有项都是有限次使用(1)～(3)生成的符号串。

定义2[25]若P(x1,x2,…,xn)是n元谓词符号,t1,t2,…,tn是项,则P(t1,t2,…,tn)是原子。

定义3[25]一阶逻辑中的公式,可递归定义为：

(1)原子是公式。

(2)若H和G是公式,则(H),(H∨G),(H∧G),(H→G)和(H↔G)是公式。

(3)若G是公式,x是G中的自由变量,则(∀x)G和(∃x)G是公式。

(4)所有公式都是有限次使用(1)～(3)生成的符号串。

由于一阶逻辑公式可以解析为树,为标记量词节点与其约束的变元节点,添加由量词节点指向被约束的变元节点的边,同时将具有相同子表达式的子树合并,可以得到一阶逻辑公式对应的有向无环图。

一阶逻辑公式可以通过如下过程转化为DAG：(1)将逻辑公式转化为解析树;(2)合并解析树中具有相同子表达式的子树;(3)将相同节点进行合并并以*替换。

图1展示了一阶逻辑公式Ф：∀X∀Y[(p(a,f(X))→q(b,Y))∨q(f(X),g(a,Y))]表示为DAG的全过程。

Figure 1 The process of representing Ф as a DAG图1 一阶逻辑公式Ф表示为DAG的过程

2.2 保序嵌入

Treelet[23]是为了保序嵌入而设计的特征。给定图G上的一个节点v,〈v,w〉表示v的一条出边,rv(w)∈{1,2,…}为〈v,w〉在v的所有出边中的排序。G上的treelet为三元组(u,v,w)∈V×V×V,满足〈v,u〉和〈v,w〉均为G中的边,且在v的所有出边的排序中,〈v,u〉排在〈v,w〉之前。换言之,一个treelet是一个包含顶部节点v、左子节点u和右子节点w的子图。若τG表示G上treelet的集合,τG={(u,v,w)：〈v,u〉∈E,〈v,w〉∈E,rv(u)

假设图2为某图上截取的一个子图,在图2中,有3个treelets,分别为(u3,u1,v),(v,u2,u4),(u5,v,u6)。在(u3,u1,v)中,v为右子节点;在(v,u2,u4)中,v为左子节点;在(u5,v,u6)中,v为顶部节点。

Figure 2 A subgraph containing three treelets图2 包含3个treelets的子图

3 基于TL-GNN的前提选择模型

本文为保留图中子节点顺序信息提出了TL-GNN,基于TL-GNN的前提选择模型结构如图3所示,TL-GNN包含状态向量初始化、信息聚合、信息传播以及图聚合4个部分。TL-GNN在信息聚合中聚集来自邻接节点和treelet的信息,迭代地更新节点的状态向量。最后,TL-GNN对图中所有节点的最终状态向量应用池化操作以获得前提与结论的图向量表示,再将前提与结论的图向量表示对(前提,结论)作为二元分类器的输入进行分类预测。

Figure 3 Premise selection model based on TL-GNN图3 基于TL-GNN的前提选择模型

3.1 TL-GNN

(1)

在节点信息聚合阶段,TL-GNN从2部分聚集邻居节点信息。第1部分聚集中心节点来自父节点与子节点的信息,第2部分以treelet的形式聚集中心节点的顺序信息,最后聚集2部分的信息。

(2)

(3)

因此,第1部分中心节点的父节点信息与子节点信息可汇总为：

(4)

G=(V,E)为公式的有向图,令τT(v)、τL(v)和τR(v)分别表示节点v作为treelet中顶部节点、左子节点及右子节点的treelet集合：

τT(v)={(u,v,w)|〈v,u〉∈E,

〈v,w〉∈E,rv(u)

τL(v)={(v,u,w)|〈u,v〉∈E,

〈u,w〉∈E,ru(v)

τR(v)={(u,w,v)|〈w,u〉∈E,

〈w,v〉∈E,rw(u)

(5)

(6)

(7)

因此,第2部分聚合中心节点v的顺序信息中来自τT(v)∪τL(v)∪τR(v)的信息可汇总为：

(8)

(9)

(10)

Figure 4 Using central node C as an example to demonstrate the node initialization, information aggregation, and information dissemination process图4 以中心节点C为例展示初始化、信息聚合及信息传播过程

在图聚合阶段,TL-GNN对K次迭代后图中所有节点的最终状态向量进行平均池化,生成最终的逻辑公式图向量表示hg,如式(11)所示：

(11)

其中,hg∈Rdhv且AvgPool(·)表示对图中所有节点的最终状态向量进行平均池化。不同函数在实验中的网络配置如图5所示。

3.2 二元分类器与损失函数

在基于TL-GNN的前提选择模型中,二元分类器的输入是前提与结论的图表示向量对(hprem,hconj)。分类器通过Fclass(·)函数预测前提是否对相应结论的证明有用,如式(12)所示：

z=Fclass([hprem;hconj])

(12)

其中,z∈R2表示前提对相应结论的证明是否有用的得分。

Fclass(·)被简单地设计为多层感知机,如式(13)所示：

Fclass(·)=Wc2(ReLU(Wc1(·)+bc1))+bc2

(13)

(14)

(15)

(16)

对于数据集中的每一样本,采用交叉熵损失函数计算预测损失,如式(17)所示：

(17)

其中,y表示真实标签的独热编码;yp表示真实值y在第p类下对应的值。

4 实验与结果分析

4.1 数据集

本文数据集基于MPTP2078(a subset of 2078 Mizar theorems)问题库[16]而创建,与文献[24]中相同。

MPTP2078问题库中的2 078个问题均被形式化为一阶逻辑公式,问题中的每个结论对应一个大规模的前提集。本文将在结论证明过程中出现的前提记为有用前提,未出现在结论证明过程中的前提记为无用前提。由于前提集中通常包含大量的无用前提,导致有用前提与无用前提数量分布极不均衡。为此,本文使用K近邻算法[15]对无用前提排序,对于问题库中的每一结论,根据其对应的正样本数量,选择无用前提中排序靠前的相应数量的前提作为负样本,使得最终选用的无用前提数量与有用前提数量大致相同。表1展示了经处理后的数据集分布情况。

Table 1 Distribution of sample size of dataset

Table 2 Experimental parameter settings

4.2 实验参数

本文实验的软硬件配置如下：CenterOS 7.6 X64,Intel®至强®银牌4114,256 GB内存CPU。

模型利用Python实现,并通过Adam优化器[26]训练。模型训练过程中使用PyTorch[27]中的ReduceLROnPlateau策略自动调整学习率,以验证集上的损失为参考,若连续5轮损失不下降,则降低学习率,直至降低到最小学习率。设置节点状态向量维度为128,256,512训练模型,迭代次数K设置为1,2,3次。模型在训练集上每完成一轮训练将会在验证集上完成一次评估,记录验证集上的损失并保存每轮训练参数。训练100个轮次后,验证集上的损失不再下降,选择100轮中验证集上损失最小的轮次,调取该轮次对应的参数在测试集上进行评估。表 2列出了实验中所有的参数设置。实验结果表明,模型在节点状态向量维度为512,迭代训练1次时效果最佳。

4.3 评价指标

本文选择的实验评价指标为准确率(Accuracy)、召回率(Recall)、精确度(Precision)和F1,其计算方式分别如式(18)～式(21)所示：

(18)

(19)

(20)

(21)

其中,Total表示所有样本的数量,TP表示正样本中分类正确的数量,TN表示负样本中分类正确的数量,FP表示正样本中分类错误的数量,FN表示负样本中分类错误的数量。

4.4 实验结果分析

本文将TL-GNN与主流的图神经网络以及同样旨在编码一阶逻辑公式子节点顺序的图神经网络进行比较,包括图卷积神经网络GCN(Graph Convolutional Network)[28]、简化图卷积神经网络SGC(Simplifying Graph Convolutional network)[29]、切比雪夫Chebyshev[30]谱图卷积神经网络、图抽样聚合神经网络GraphSAGE(Graph SAmple and aggreGatE)[31]、图注意力神经网络GAT(Graph ATtention network)[32]和EW-GNN。表3展示了对比实验结果,TL-GNN代表了模型在节点状态向量维度为512,迭代训练1次时的结果。

Table 3 Comparison of experimental results

实验对比结果表明,TL-GNN在前提选择任务中的表现明显优于其他主流图神经网络模型。同时,与同样旨在编码一阶逻辑公式子节点顺序的EW-GNN相比,TL-GNN高出约1%的分类准确率。在忽略略高的计算复杂度的情况下,这不仅说明了一阶逻辑公式的子节点顺序信息对前提选择任务是重要的,也说明了TL-GNN相较于其他图神经网络模型具有更强的表征一阶逻辑公式的能力。

5 结束语

本文将一种面向高阶逻辑的可保序的嵌入treelet延伸到一阶逻辑公式中。根据treelet的特性,设计并实现了基于treelet的图神经网络模型TL-GNN。与当前主流图神经网络模型以及同样旨在编码一阶逻辑公式子节点顺序信息的图神经网络模型相比,本文提出的模型明显在前提选择任务中更具有优势。当前模型中仅聚合了邻居节点与子节点顺序信息,一阶逻辑公式的语义与语法性质未被充分考虑。未来将考虑更多一阶逻辑公式的语义与语法信息,提出更加有针对性的模型。