刘清华，徐 扬，吴贯锋，李瑞杰
（1.西南交通大学信息科学与技术学院，四川 成都 611756；
2.西南交通大学系统可信性自动验证国家地方联合工程实验室，四川 成都 610031；
3.西南交通大学数学学院，四川 成都 611756；
4.西南交通大学交通运输与物流学院，四川 成都 611756）
自动推理作为计算机科学和数理逻辑的交叉学科，是人工智能的核心分支.一阶逻辑（first-order logic，FOL）自动定理证明最初仅为了自动地证明数学定理，而目前已广泛地应用于其他领域，例如电路设计、软件验证、硬件验证和管理等[1-3].先进的一阶逻辑自动定理证明器（automated theorem prover，ATP），如Vampire[4]和E[5]，擅长在TPTP （thousands of problems for theorem provers）[6]的某些限定领域中证明问题，但却很难高效地证明大型问题库中的问题（如，MizAR数学库[7]）.这些大规模的问题被称为大理论问题，其通常包含成千上万个前提，但只有极少部分的前提能对问题结论的证明起到有效作用.
在FOL中，问题的前提和结论被形式化为一阶逻辑公式.大多数ATP主要基于Given Clause算法[8]对从公式转换而来的子句（合取范式）进行证明搜索.证明搜索是在两个集合上执行：未处理子句集和已处理子句集.在证明搜索开始前，所有输入子句都是未处理的.Given Clause算法反复地从未处理子句集中选择一个子句作为给定子句，并将所有可能的推理规则应用于该子句和已处理子句集中的其他子句；
最后，新选择的给定子句被放入已处理子句集中，新生成的子句被置于未处理子句中.此证明搜索过程将一直持续直到超出计算资源限制，或推断出空子句或已处理子句集变得饱和（无法推断出任何新子句）.
传统ATP在证明大理论时，由于问题包含了数量极多的前提，在上述证明搜索的过程中，搜索空间会呈爆炸型增长.因此，计算机资源会很快地被耗尽，进而导致ATP证明问题的性能大幅降低.该问题导致了ATP无法在证明大理论问题时充分发挥作用.解决该问题的一种有效方法是在ATP试图找到结论的证明之前，尽可能地选择出最可能参与证明构造的前提.该过程被称为前提选择，通常作为ATP预处理的一部分，其对解决大规模问题至关重要.
起初，前提选择通常采用基于公式中符号的启发式方法[9-10]，主要通过计算和比较公式中的符号，对公式的相关性进行分析.最近，结合传统机器学习技术[11-13]的前提选择模型展现了具有竞争力的结果，但基于传统机器学习的前提选择在编码逻辑公式时强烈地依赖于手工设计的特征（如，符号和子项等）.因为深度学习方法，如长短期记忆神经网络（long-short term memory，LSTM）[14]和图神经网络（graph neural network，GNN）[15-17]，在编码逻辑公式时不需要依赖于任何人工设计的特征，得到了越来越多学者的关注.又因为逻辑公式可以自然而然地表示为能够保留公式句法和语义信息的有向无环图（directed acyclic graph，DAG），所以定理证明与GNN的结合是当前最热门的研究主题之一.
目前，主流的图神经网络框架通常通过聚集邻接节点的信息来更新目标节点的特征表示.在此框架下的图神经网络模型常用于处理无向图，如图卷积神经网络（graph convolutional network，GCN）[18]、图注意力神经网络（graph attention network，GAT）[19]等.然而，公式图是有向，当前的图神经网络模型只能单向地沿着公式图的边进行信息传播.除此之外，逻辑图中相应的子节点之间是有顺序的，而目前的图神经网络模型的信息聚集操作通常与子节点的顺序无关.为发挥逻辑公式图表示的优势，理想的方法是根据公式的特性对公式图中的节点进行排序并双向地传递邻接节点的信息.
针对上述问题，提出一种带有边类型的双向图用于表示一阶逻辑公式.图中相邻的两个节点由不同方向的两条边连接且每条边都有一种对应的边类型.通过确定每条边特定的边类型，可以对双向图中的节点进行排序.基于新的公式图表示，提出了一种基于边权重的图神经网络模型，即EW-GNN （edgeweight-based graph neural network）.对图中的每一个方向，EW-GNN首先利用节点的信息更新对应边类型的特征表示，随后利用更新后的边类型特征计算邻接节点对中心节点的权重.传递给中心节点的信息是邻接节点信息的加权和.EW-GNN最后汇聚中心节点来自两个方向上的信息，并对节点进行更新.实验比较分析表明：当前主流模型在测试集上的分类准确率两两之差均小于1%，而提出的EW-GNN在相同的测试集上比表现最优的模型还能提高约1%的分类准确率.因此，EW-GNN能够在前提选择任务中表现得更加优越.
1.1 一阶逻辑公式
在一阶逻辑中[20]，给定一个变量符号集 V，一个函数符号集 F，以及一个谓词符号集 P.一阶逻辑项（term）是一个变量项v∈V或者形如f(t1,t2,···,tn)的函数项，其中，f∈F为n（n≥0）元函数符，t1，t2,···,tn是项.一阶逻辑原子（atom）形如P(t1,t2,···,tn)，其中，P∈P为n（n≥1）元谓词符.一阶逻辑公式是由一阶逻辑联结词 C={∼,∧,∨,→,↔}、量词 Q={∀,∃}和原子联结而成.
1.2 图定义
带有边类型的双向图定义为G=(V,E,RE)，其中：节点集V={v1,v2,···,vn} 包含G中所有节点；
边集E={〈vi,vj〉|vi,vj∈V} 包含G中所有边，有向对eij=〈vi,vj〉 表示从节点vi到节点vj的有向边；
边类型集包含G中所有边对应的边类型.节点vi的邻接节点集定义为 N(vi)= {vj|eji∈E}.图中的每一个节点v都伴随着一个初始节点特征向量xv∈Rdv，每一条边e也伴随着一个初始边特征向量xe∈Rde，表示其对应的边类型.dv和de分别为xv和xe的初始向量维度.
1.3 表 示
一阶逻辑公式能够自然地表示为语义解析树（abstract semantic tree，AST）.通过添加从量词节点指向到相应被约束的变量节点的边以及合并所有相同的子表达式对应的子树，可以将表示公式的AST扩展为含有根节点的DAG.
为了保持逻辑公式图中部分节点之间有序性以及双向传递邻接节点的信息，设计了双向图表示，其中图中相邻的两个节点由方向不同的两条边连接且每条边都具有一种对应的边类型.
逻辑公式图中的节点大致可分为5种类型：量词、逻辑联结词、谓词、函数和变量.在定义边类型时，逻辑连接词节点、量词节点和特殊的相等谓词（=）节点的名称为其类型，而其他谓词、函数以及变量节点的类型为其对应的类型，分别记为pred、func和var.
然而，对逻辑公式图中的子节点进行排序仍是一个难题.利用文献[16]中提出的排序方案，从上往下单向地定义节点顺序，即在给定相应父节点类型的情况下，对其子节点进行排序：
1）如果父节点是逻辑联结词 ～、∧、∨、↔ 或 =，则它们对应的子节点的顺序一样；
2）如果父节点是量词 ∀ 或 ∃，则其变量子节点具有相同的顺序，而其他子节点是线性排序的；
3）如果父节点是其他谓词、逻辑连接词或函数，则其子节点是线性排序的.
正式地，一阶逻辑表达式s的双向图表示Gs=(Vs,Es,Rs)构造如下：
1）如果s是一个变量项或常量项（0元函数项），则Vs={s}，Es={∅}；
2）如果s=f(s1,s2,···,sn)，其中，f∈F∪P∪C且s1,s2,···,sn为子表达式，则，其中，H(si)为表达式si的最外层符号.如果s包含相同的子表达式，则在Gs上合并（merge）相同的子图；
3）如果s=，其中， ϕ∈Q，是包含变量x的表达式，则Vs=Vsˆ∪{ϕ}，Es=Esˆ∪{〈ϕ，H()〉}∪{〈H()，ϕ〉}∪{〈ϕ,x〉}∪{〈x,ϕ〉}.随后，在Gs上合并所有由量词 ϕ 约束的变量x；
4）在递归构造完Gs后，用统一的标记 * 更替Gs中所有变量节点的名称；
5）Rs中的每一个边类型由对应连接的两个节点的类型和节点顺序决定.
图1为一阶逻辑公式 ∀x,y(p(f(x),a)∨q(a,f(y)))的双向图表示，其中：y(•)为变量；
p(•)和q(•)为谓词函数；
f(•)和a分别为一元函数和零元函数（常元）.
图1 一阶逻辑公式的双向图表示Fig.1 Bidirectional graph representation of first-order logical formula
在图1中，变量节点x和y被替换成了统一的标记 *，替换后的双向图能在变量更名下保持一致.两种不同颜色的边分别代表了图中两个不同的方向.与单向图相比，双向图中的每个节点有来自两个方向上邻接节点，如 ∀、P和Q都是图中的节点 ∨的邻接节点.通过给图中的边添加类型，可以在一定程度上对图中的相关节点进行排序.如在节点 ∀ 下，变量节点x和y（即节点*）的顺序相同且记为1，因此节点 ∨ 的顺序自然地记为2.连接节点 ∀ 和 ∨ 的两条边上的顺序均为 ∨ 在从上到下的单向图的中作为 ∀ 的子节点的顺序.除此之外，边类型同样也反映出了边的方向.边类型 ∀_∨_2和 ∨ _∀_2分别表示从节点 ∀ 指向节点 ∨ 的边和从节点 ∨ 指向节点 ∀ 的边.
所有前提选择模型都具有相似的框架，即，对逻辑公式进行表示并计算公式间的相关性.其正式定义如下：
定义1[11]给定一个结论c和其前提集A，前提选择需要预测并选择A中可能对证明c有用的前提.
如图2所示，一个完整的端到端基于图神经网络的前提选择模型应包含以下3部分：公式图表示、图神经网络模型和二元分类器.在本文中，首先，将一阶逻辑公式转化为带有边类型的双向图；
其次，通过使用新提出的EW-GNN模型，将逻辑公式图编码为特征向量；
最后，二元分类器将一个结论向量和一个候选前提向量的拼接作为输入，并输出一个 [0,1]之间的实数得分，该得分表明在证明结论中使用候选前提的概率.
图2 基于图神经网络的前提选择模型Fig.2 Premise selection model based on graph neural network
给定一个大理论问题和训练后的前提选择模型，可以将所有的{结论,前提}对反馈给前提选择模型，并输出每个前提对结论有用（无用）的概率.根据输出的概率，可以对前提进行排序，并从排序中选择出前np个前提作为给定结论的有用前提.最后，ATP将使用np个选定的前提自动地证明对应的结论，从而解决ATP搜索空间爆炸增长的问题.
2.1 基于边权重的图神经网络
EW-GNN模型包括4个阶段：初始化、消息聚合、消息传播（节点更新）以及图聚合.
在初始化阶段，模型通过不同的嵌入函数Fv和Fe将任意初始节点特征向量xv和初始边特征向量xe分别映射为初始节点状态向量和初始边状态向量：
Fv和Fe在本文中被设计为不同的查找表，用于存储固定字典和大小的嵌入，并将用热独（one-hot）向量表示的xv和xe分别编码为固定大小的初始状态向量.
在第k（k=1,2,···,K）次信息聚集阶段，EWGNN根据边的方向，分别聚集目标节点vi来自两个方向上的邻接节点vj的信息.这里，简单地把边的方向分为从上往下和从下往上.为计算vj对vi的权重，首先利用vj和vi第k− 1次状态向量和，以及第k− 1次边状态向量对第k次边状态向量进行更新：
如果eji的方向是从上往下的，则
如果eji的方向是从下往上的，则
利用更新后的边状态向量，领接节点vj对中心节点vi的权重的计算如下：
如果eji的方向是从上往下的，则
如果eji的方向是从下往上的，则
节点vi来自邻接节点vj的聚合信息为
eji的方向不同，也随之不同：
如果eji的方向是从上往下的，则
如果eji的方向是从下往上的，则
因此，节点vi的状态向量的第k次更新为
第K次迭代后，EW-GNN在图聚合阶段对图中所有节点状态向量进行池化，以生成最后的公式图向量：
这里，采用了平均池化对整个节点维度上的节点特征求平均值.
2.2 二元分类器
分类模型的输入是图向量对 (hconj,hprem)，分别表示结论和候选的前提.EW-GNN通过分类函数Fclass对前提在结论证明中的有用性进行预测：
Fclass在本文中被设计为多层感知机（multi-layer perceptron，MLP）.具体为
式中：W1∈Rdhv×R2dhv和W2∈R2×Rdhv为不同的学习矩阵；
b1∈Rdhv和b1∈R2为学习偏差向量.ReLU(•)为修正线性单元（rectified linear unit，ReLU）函数：
因此，前提在两个类别下的预测概率为
2.3 损失函数
在均衡数据集下，对于每一个{结论,前提}对，损失函数 L 定义为预测值和真实值y之间的交叉熵：
式中：y为真实值的一个独热编码；
yC和分别为真实值y和预测值在第C类别下的对应值.
在非均衡数据集下，对于每一个{结论，前提}对，损失函数 L 定义为预测值和真实值y之间的加权交叉熵：
式中：w+、w−分别为正、负样本的权重，且w+>w−.
在本文的模型训练中，w+和w−分别设置为
式中：NP、NN分别为数据集中正、负样本的数量.
本文基于MPTP2078问题库[11]建立了一个用于训练、验证和测试前提选择模型的数据集.
MPTP2078问题库中一共包含2 078个问题，均来自Mizar数学库（Mizar Mathematical Library，MML）[21]中与Bolzano-Weierstrass公理相关的问题.问题库所有问题的前提和结论均被TPTP系统形式化为一阶逻辑公式，且公式按照它们在Mizar数学库中出现的顺序线性排序.即，出现在每一个结论之前的公式（前提和其他结论）均可作为证明该结论的前提.问题的前提数量在区间[10, 4563]中，且前提的平均数量为1 876.表1具体地描述了问题库中结论和前提的情况.
表1 MPTP2078问题库描述Tab.1 Description of MPTP2078 benchmark条
数据集中每一个例子是一个三元组{结论,前提,标签}.其中：前提是给定结论的候选前提，标签是二元分类中的类别；
标记为1的样本记为正样本，表示前提对结论有用；
标记为0的样本记为负样本，表示前提对结论无用.在问题库中，ATPboost[13]证明了1469个结论并一共产生了24087个证明，这意味着一个结论可能对应多个证明.
正式地，每一个被证明的结论c有nc（nc≥1）个证明P1，P2,···,Pr,···,Pnc，且Pr={pr1,pr2,···,prt,···,prncr}，其中：prt为构造证明Pr的一个前提，ncr是Pr中有用前提的总数.因此，有用前提集 UP(c)=包含至少在结论c的所有证明中出现一次的前提.
在数据集的构造中，对每一个已证明结论c，其对应的正样本中的前提来自 UP(c).因此，结论c对应的正样本为 (c,p,1)（∀p∈UP(c)）且正样本的总数为 |UP(c)|.
然而，问题库中极大部分结论都对应了一个大规模的前提集且 UP(c)包含的有用前提数量仅仅只占总前提数量非常小的一部分.例如，MPTP2078问题库中的结论 t12_yellow_6一共包含3836个前提，但只有5个前提被用于证明结论.这表明结论对应的无用前提数量远远大于有用前提数量.因此，如果使用c的所有无用前提来构造负样本，则正负样本的分布将极度不平衡.
为构建与正样本数量相等的负样本，使用文献[22]设计的手工特征表示公式，并使用K近邻（K-nearest neighbor，KNN）[23]算法粗略地对结论的所有前提进行排序.随后，选择对结论无用但排名靠前的前提构造负样本，其中，无用前提的数量和有用前提大致相同.最终，整理得到的数据集如表2所示.
表2 数据集划分Tab.2 Division of datasets个
本文使用Python编程实现了本模型.在模型搭建的过程中，使用Pytorch库[24]进行深度学习算法的实现，并使用Pytorch_Geometric库[25]处理数据和对实现文中提及的所有图神经网络.本次实验在超微4029GP-TRT服务器上进行，具体软硬件配置环境如下：CenterOS7.6 X64，Intel至强银牌4114，256 GB内存，2 TB SSD, 所用GPU为NViDIA RTX 2080Ti.
4.1 实验参数
使用Adam[26]优化器对模型进行训练.初始化的学习率为0.0010，在50个训练轮次后，学习率衰减为0.0001.在每个轮次后，对模型进行保存并在验证集上进行评估.经过所有轮次的训练和验证后，选择在验证集上表现最佳（损失最小）的模型作为最优模型，并在测试集上对其进行评估.为了保证实验结果的公平性，文章中所有涉及到的模型参数设置均一致.具体参数如表3所示.
表3 参数设置Tab.3 Setting of parameters
4.2 评价指标
为评估所提EW-GNN模型的性能，将该模型与具有代表性的图神经网络模型进行比较.在前提选择任务中，需要根据模型的输出概率对前提进行排序.因此，需要同时评估正、负样本的正确预测率.若仅关心正样本的正确预测率，则过多的负样本被错误预测为正时会严重地影响前提的排序，即无用的前提可能会在排序的前列.当数据集中正、负样本分布均衡时，本文选择准确率Accuracy指标对模型进行对比分析.Accuracy代表模型判断当前前提对给定结论是否有用的准确程度：
式中：Total为数据集中所有样本的数量；
TP为分类正确的正样本的数量；
TN为分类正确的负样本的数量.
本文同时增加召回率Recall、精确度Precision和F1指标F1对模型进行评估：
式中：FN为分类错误的负样本的数量；
FP为分类错误的正样本的数量.
4.3 实验结果分析
为保证对比结果的有效性，实验过程中，只改变前提选择模型中图神经网络模型的部分，而不改变初始化模型以及二元分类模型.所有方法在均衡数据集上的评估结果如表4所示，最佳结果以黑体突出显示.
表4 数据集上的对比实验结果Tab.4 Comparision of experimental results on datasets
实验结果表明，所提出的基于边权重的图神经网络EW-GNN在前提选择任务中明显优于目前其他流行的图神经网络模型：EW-GNN在相同的测试集上至少提高了1%的分类准确率.从表3中可以看出：除了本文提出的EW-GNN模型，没有另一个模型的分类准确率能够高于其他模型1%.这说明双向地传播邻接节点的信息有助于帮助图神经网络模型生成更有表征能力的逻辑公式图向量.EW-GNN在更新节点状态向量之间，会首先对边状态向量进行更新.根据对边类型的构造，边向量既能反映由对应边连接的节点类型，也能反映出节点的顺序.这对表征一阶逻辑公式非常重要.因为在一阶逻辑公式图中，不同类型的邻接节点对中心节点的贡献度是不同的.直觉地，函数节点的贡献明显要大于变量节点，因为变量在一阶逻辑公式的表征中通常都被忽略.同样地，节点的顺序同样也是逻辑公式图表征不可忽略的重要特性.如，∀xp(x,a) 和 ∀xp(a,x) 是两个不同的逻辑公式，如果忽略了x和a的顺序，会导致这两个逻辑公式最终生成的图向量是一样的.因此，EW-GNN根据更新后的边状态向量为中心节点的每个邻接节点赋予权重，更加符合一阶逻辑公式的特性.相比之下，本文所提出的EW-GNN模型更加适用于一阶逻辑中的前提选择任务.
1）本文针对一阶逻辑公式的特性，提出了双向图表示方法，并对每条边设计了能够表示对应节点类型和顺序的边类型.
2）根据双向图的特性，本文设计并实现了一种基于边权重的图神经网络模型EW-GNN.该模型既能够双向地传播节点信息，也能利用边向量编码对应节点的类型和顺序.
3）与当前流行的图神经网络模型相比，本文提出的模型明显在前提选择任务中更具有优势.
4）针对一阶逻辑公式的特性，未来计划提出更加具有针对性的表征学习模型.
猜你喜欢子句结论逻辑由一个简单结论联想到的数论题中等数学(2022年7期)2022-10-24刑事印证证明准确达成的逻辑反思法律方法(2022年2期)2022-10-20逻辑中学生百科·大语文(2021年11期)2021-12-05创新的逻辑纺织科学研究(2021年7期)2021-08-14立体几何中的一个有用结论中学生数理化·高一版(2021年1期)2021-03-19子句级别的自注意力机制的情感原因抽取模型中南民族大学学报（自然科学版）(2021年1期)2021-02-02汉语和泰语关系子句的对比研究海外文摘·艺术(2020年3期)2020-06-13西夏语的副词子句西夏学(2018年2期)2018-05-15女人买买买的神逻辑37°女人(2017年11期)2017-11-14结论小猕猴智力画刊(2016年5期)2016-05-14