Edge-Weighted-Based Graph Neural Network for First-Order Premise Selection
-
摘要:
为提高自动定理证明器在大规模问题中证明问题的能力，前提选择任务应运而生. 由于公式图的有向性，主流的图神经网络框架只能单向地对节点进行更新，且无法编码公式图中子节点间的顺序. 针对以上问题，提出了带有边类型的双向公式图表示方法，并提出了一种基于边权重的图神经网络（edge-weight-based graph neural network，EW-GNN）模型用于编码一阶逻辑公式. 该模型首先利用相连节点的信息来更新对应边类型的特征表示，随后利用更新后的边类型特征计算邻接节点对中心节点的权重，最后利用邻接节点的信息双向地对中心节点进行更新. 实验比较分析表明：基于边权重的图神经网络模型在前提选择任务中表现得更加优越，其在相同的测试集上比当前最优模型的分类准确率高了约1%.
Abstract:In order to improve the ability of automated theorem provers, the premise selection task emerges. Due to the directional nature of formula graphs, most current graph neural networks can only update nodes in one direction, and cannot encode the order of sub-nodes in the formula graph. To address the above problems, a bidirectional graph with edge types to represent logical formulae and a edge-weight-based graph neural network (EW-GNN) model to encode first-order logic formulae are proposed. The model firstly uses the information of connected nodes to update the feature representation of the corresponding edge type, then calculates the weight of the adjacent node to the central node with the updated edge type feature, and finally uses the information of the adjacent node to update the target node in both directions. The experimental results show the edge-weighted-based graph neural network model performs better in the premise selection task, which can improve the classification accuracy by 1% compared to the best model on the same test dataset.
-
自动推理作为计算机科学和数理逻辑的交叉学科，是人工智能的核心分支. 一阶逻辑（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 （edge-weight-based graph neural network）. 对图中的每一个方向，EW-GNN首先利用节点的信息更新对应边类型的特征表示，随后利用更新后的边类型特征计算邻接节点对中心节点的权重. 传递给中心节点的信息是邻接节点信息的加权和. EW-GNN最后汇聚中心节点来自两个方向上的信息，并对节点进行更新. 实验比较分析表明：当前主流模型在测试集上的分类准确率两两之差均小于1%，而提出的EW-GNN在相同的测试集上比表现最优的模型还能提高约1%的分类准确率. 因此，EW-GNN能够在前提选择任务中表现得更加优越.
1. 一阶逻辑公式图表示
1.1 一阶逻辑公式
在一阶逻辑中[20]，给定一个变量符号集
$ \mathcal{V} $ ，一个函数符号集$ \mathcal{F} $ ，以及一个谓词符号集$ \mathcal{P} $ . 一阶逻辑项（term）是一个变量项$ v\in \mathcal{V} $ 或者形如$ f \left({t}_{1}, \right. \left.{t}_{2},\cdots ,{t}_{n}\right) $ 的函数项，其中，$ f\in \mathcal{F} $ 为$n $ （$n\geqslant 0$ ）元函数符，$ {t}_{1} $ ，$ {t}_{2},\cdots , $ $ {t}_{n} $ 是项. 一阶逻辑原子（atom）形如$ P\left({t}_{1},{t}_{2},\cdots ,{t}_{n}\right) $ ，其中，$ P\in \mathcal{P} $ 为$ n $ （$n\geqslant 1$ ）元谓词符. 一阶逻辑公式是由一阶逻辑联结词$\mathcal{C}=\{ \sim ,{\wedge} ,{\vee} ,{\to} ,{\leftrightarrow} \}$ 、量词$ \mathcal{Q}=\{\forall ,\exists \} $ 和原子联结而成.1.2 图定义
带有边类型的双向图定义为
$ \;\;\;\;G=\left(V,E,{R}_{E}\right) $ ，其中：节点集$ V={\{v}_{1},{v}_{2},\cdots ,{v}_{n}\}$ 包含G中所有节点；边集$ E=\{ 〈 {v}_{i},{v}_{j} 〉 |{v}_{i},{v}_{j}\in V\} $ 包含G中所有边，有向对$ {e}_{ij}= 〈 {v}_{i},{v}_{j} 〉 $ 表示从节点vi到节点vj的有向边；边类型集${R}_{E}=\left\{{r}_{{e}_{ij}}|{e}_{ij}\in E \right\}$ 包含G中所有边对应的边类型. 节点vi的邻接节点集定义为$ \mathcal{N}\left({v}_{i}\right)=$ $\left\{{v}_{j}|{e}_{ji}\in E \right\}$ . 图中的每一个节点v都伴随着一个初始节点特征向量${\boldsymbol{x}}_{v}\in {\bf{R}}^{{d}_{v}}$ ，每一条边e也伴随着一个初始边特征向量${\boldsymbol{x}}_{e}\in {\bf{R}}^{{d}_{e}}$ ，表示其对应的边类型. dv和de分别为xv和xe的初始向量维度.1.3 表 示
一阶逻辑公式能够自然地表示为语义解析树（abstract semantic tree，AST）. 通过添加从量词节点指向到相应被约束的变量节点的边以及合并所有相同的子表达式对应的子树，可以将表示公式的AST扩展为含有根节点的DAG.
为了保持逻辑公式图中部分节点之间有序性以及双向传递邻接节点的信息，设计了双向图表示，其中图中相邻的两个节点由方向不同的两条边连接且每条边都具有一种对应的边类型.
逻辑公式图中的节点大致可分为5种类型：量词、逻辑联结词、谓词、函数和变量. 在定义边类型时，逻辑连接词节点、量词节点和特殊的相等谓词（=）节点的名称为其类型，而其他谓词、函数以及变量节点的类型为其对应的类型，分别记为pred、func和var.
然而，对逻辑公式图中的子节点进行排序仍是一个难题. 利用文献[16]中提出的排序方案，从上往下单向地定义节点顺序，即在给定相应父节点类型的情况下，对其子节点进行排序：
1） 如果父节点是逻辑联结词 ~、
$ \wedge $ 、$ \vee $ 、${\leftrightarrow}$ 或 =，则它们对应的子节点的顺序一样；2） 如果父节点是量词
$ \forall $ 或$ \exists $ ，则其变量子节点具有相同的顺序，而其他子节点是线性排序的；3） 如果父节点是其他谓词、逻辑连接词或函数，则其子节点是线性排序的.
正式地，一阶逻辑表达式s的双向图表示
$ {G}_{s}=\left({V}_{s},{E}_{s},{R}_{s}\right) $ 构造如下：1） 如果s是一个变量项或常量项（0元函数项），则
$ {V}_{s}=\left\{s\right\} $ ，$ {E}_{s}=\left\{\varnothing \right\} $ ；2） 如果
$s=f\left({s}_{1},{s}_{2},\cdots ,{s}_{n}\right)$ ，其中，$ f\in \mathcal{F}\cup \mathcal{P}\cup \mathcal{C} $ 且$ {s}_{1} $ ,$ {s}_{2} ,\cdots,$ $ {s}_{n} $ 为子表达式，则$ {V}_{s}\in {\bigcup }_{i=1}^{n}{V}_{{s}_{i}}\cup \left\{f\right\} $ ，$ {E}_{s}= {\bigcup }_{i=1}^{n}\left({E}_{{s}_{i}}\cup \{ 〈 f,{H(s}_{i}) 〉 \}\cup \{ 〈 {H(s}_{i}),f 〉 \}\right) $ ，其中，$ {H(s}_{i}) $ 为表达式si的最外层符号. 如果s包含相同的子表达式，则在Gs上合并（merge）相同的子图；3） 如果
$ s={\phi }\hat{s} $ ，其中，$ \phi \in \mathcal{Q} $ ，$ \hat{s} $ 是包含变量x的表达式，则$ {V}_{s}={V}_{\hat{s}}\cup \left\{\phi \right\} $ ，${E}_{s}={E}_{\hat{s}}\cup \{ 〈 \phi ，H\left(\hat{s}\right) 〉 \}\cup \{ 〈 H\left(\hat{s}\right)，\phi 〉 \}\cup \{ 〈 \phi ,x 〉 \}\cup \{ 〈 x,\phi 〉 \}$ . 随后，在Gs上合并所有由量词$ \phi $ 约束的变量x；4） 在递归构造完Gs后，用统一的标记 * 更替Gs中所有变量节点的名称；
5） Rs中的每一个边类型由对应连接的两个节点的类型和节点顺序决定.
图1为一阶逻辑公式
${\forall }x,y{(p(f(x),a) { \vee}} { q(a,f(y)))}$ 的双向图表示，其中：$ y({\text{•}}) $ 为变量；$p( {\text{•}})$ 和$ q({\text{•}}) $ 为谓词函数；$f({\text{•}})$ 和$ a $ 分别为一元函数和零元函数（常元）.
图 1 一阶逻辑公式的双向图表示Figure 1. Bidirectional graph representation of first-order logical formula在图1中，变量节点
$ x $ 和$ y $ 被替换成了统一的标记 *，替换后的双向图能在变量更名下保持一致. 两种不同颜色的边分别代表了图中两个不同的方向. 与单向图相比，双向图中的每个节点有来自两个方向上邻接节点，如$ \forall $ 、P和Q都是图中的节点$ \vee $ 的邻接节点. 通过给图中的边添加类型，可以在一定程度上对图中的相关节点进行排序. 如在节点$ \forall $ 下，变量节点x和y （即节点*）的顺序相同且记为1，因此节点$ \vee $ 的顺序自然地记为2. 连接节点$ \forall $ 和$ \vee $ 的两条边上的顺序均为$ \vee $ 在从上到下的单向图的中作为$ \forall $ 的子节点的顺序. 除此之外，边类型同样也反映出了边的方向. 边类型$ \forall $ _$ \vee $ _2和$ \vee $ _$ \forall $ _2分别表示从节点$ \forall $ 指向节点$ \vee $ 的边和从节点$ \vee $ 指向节点$ \forall $ 的边.2. 模 型
所有前提选择模型都具有相似的框架，即，对逻辑公式进行表示并计算公式间的相关性. 其正式定义如下：
定义1[11] 给定一个结论c和其前提集
$ A $ ，前提选择需要预测并选择$ A $ 中可能对证明c有用的前提.如图2所示，一个完整的端到端基于图神经网络的前提选择模型应包含以下3部分：公式图表示、图神经网络模型和二元分类器. 在本文中，首先，将一阶逻辑公式转化为带有边类型的双向图；其次，通过使用新提出的EW-GNN模型，将逻辑公式图编码为特征向量；最后，二元分类器将一个结论向量和一个候选前提向量的拼接作为输入，并输出一个
$ \left[\mathrm{0,1}\right] $ 之间的实数得分，该得分表明在证明结论中使用候选前提的概率.给定一个大理论问题和训练后的前提选择模型，可以将所有的{结论,前提}对反馈给前提选择模型，并输出每个前提对结论有用（无用）的概率. 根据输出的概率，可以对前提进行排序，并从排序中选择出前
$ {n}_{{\rm{p}}} $ 个前提作为给定结论的有用前提. 最后，ATP将使用$ {n}_{{\rm{p}}} $ 个选定的前提自动地证明对应的结论，从而解决ATP搜索空间爆炸增长的问题.2.1 基于边权重的图神经网络
EW-GNN模型包括4个阶段：初始化、消息聚合、消息传播（节点更新）以及图聚合.
在初始化阶段，模型通过不同的嵌入函数
$ {F}_{v} $ 和$ {F}_{e} $ 将任意初始节点特征向量$ {\boldsymbol{x}}_{v} $ 和初始边特征向量$ {\boldsymbol{x}}_{e} $ 分别映射为初始节点状态向量$ {\boldsymbol{h}}_{v}^{\left(0\right)} $ 和初始边状态向量$ {\boldsymbol{h}}_{e}^{\left(0\right)} $ ：h(0)v=Fv(xv), (1) h(0)e=Fe(xe), (2) 式中：
${\boldsymbol{h}}_{v}^{\left(0\right)}\in {{\bf{{R}}}}^{{d}_{{h}_{v}}}$ ；${\boldsymbol{h}}_{e}^{\left(0\right)}\in {{\bf{{R}}}}^{{d}_{{h}_{e}}}$ ；$ {d}_{{h}_{v}} $ 和$ {d}_{{h}_{e}} $ 分别为节点状态向量和边状态向量的维度.$ {F}_{v} $ 和$ {F}_{e} $ 在本文中被设计为不同的查找表，用于存储固定字典和大小的嵌入，并将用热独（one-hot）向量表示的$ {\boldsymbol{x}}_{v} $ 和$ {\boldsymbol{x}}_{e} $ 分别编码为固定大小的初始状态向量.在第
$ k $ （$k=\mathrm{1,2},\cdots ,K$ ）次信息聚集阶段，EW-GNN根据边的方向，分别聚集目标节点$ {v}_{i} $ 来自两个方向上的邻接节点$ {v}_{j} $ 的信息. 这里，简单地把边的方向分为从上往下和从下往上. 为计算$ {v}_{j} $ 对$ {v}_{i} $ 的权重，首先利用$ {v}_{j} $ 和$ {v}_{i} $ 第k − 1次状态向量$ {\boldsymbol{h}}_{{v}_{j}}^{\left(k-1\right)} $ 和$ {\boldsymbol{h}}_{{v}_{i}}^{\left(k-1\right)} $ ，以及第k − 1次边状态向量$ {\boldsymbol{h}}_{{e}_{ji}}^{\left(k-1\right)} $ 对第k次边状态向量$ {\boldsymbol{h}}_{{e}_{ji}}^{\left(k\right)} $ 进行更新：如果
$ {e}_{ji} $ 的方向是从上往下的，则h(k)eji=W(k)i([h(k−1)vj;h(k−1)eji;h(k−1)vi]), (3) 如果
$ {e}_{ji} $ 的方向是从下往上的，则h(k)eji=W(k)o([h(k−1)vj;h(k−1)eji;h(k−1)vi]), (4) 式中：
${\boldsymbol{W}}_{{\rm{i}}}^{\left(k\right)}、{\boldsymbol{W}}_{{\rm{o}}}^{\left(k\right)}$ 分别为第k次入边、出边的学习矩阵，$ {\boldsymbol{W}}_{{\rm{i}}}^{\left(k\right)},{\boldsymbol{W}}_{{\rm{o}}}^{\left(k\right)}\in {\bf{{{R}}}}^{{d}_{{h}_{e}}}{\times {\bf{{R}}}}^{2{d}_{{h}_{v}} + {d}_{{h}_{e}}}$ .利用更新后的边状态向量，领接节点
$ {v}_{j} $ 对中心节点$ {v}_{i} $ 的权重$ {a}_{ji}^{\left(k\right)} $ 的计算如下：如果
$ {e}_{ji} $ 的方向是从上往下的，则a(k)ji=σ(W(k)wi(h(k)eji)), (5) 如果
$ {e}_{ji} $ 的方向是从下往上的，则a(k)ji=σ(W(k)wo(h(k)eji)), (6) 式中：
${\boldsymbol{W}}_{{{\rm{wi}}}}^{\left(k\right)}、{\boldsymbol{W}}_{{{\rm{wo}}}}^{\left(k\right)}$ 分别为权重计算时第k次入边、出边的学习矩阵，$ {\boldsymbol{W}}_{{{\rm{wi}}}}^{\left(k\right)},{\boldsymbol{W}}_{{{\rm{wo}}}}^{\left(k\right)}\in {{\bf{{R}}}}^{{d}_{{h}_{e}}}$ ；$ \sigma \left(x\right) = \dfrac{1}{1 + {{\rm{e}}}^{-x}} $ 为sigmoid激活函数.节点
$ {v}_{i} $ 来自邻接节点$ {v}_{j} $ 的聚合信息为m(k)vi=∑vj∈N(vi)a(k)jiF(k)m(h(k−1)vj), (7) 式中：
$ {F}_{m}^{\left(k\right)} $ 为第m层的全连接层.$ {e}_{ji} $ 的方向不同，$ {F}_{m}^{\left(k\right)} $ 也随之不同：如果
$ {e}_{ji} $ 的方向是从上往下的，则F(k)m(h(k−1)vj)=W(k)mih(k−1)vj+b(k)mi, (8) 如果
$ {e}_{ji} $ 的方向是从下往上的，则F(k)m(h(k−1)vj)=W(k)moh(k−1)vj+b(k)mo, (9) 式中：
${\boldsymbol{W}}_{{m{\rm{i}}}}^{\left(k\right)}、{\boldsymbol{W}}_{{m{\rm{o}}}}^{\left(k\right)}$ 和${\boldsymbol{b}}_{m{\rm{i}}}^{\left(k\right)}$ 、${\boldsymbol{b}}_{m{\rm{o}}}^{\left(k\right)}$ 分别为权重计算时第m层第k次入边、出边的学习矩阵和偏差向量，$ {\boldsymbol{W}}_{{m{\rm{i}}}}^{\left(k\right)},{\boldsymbol{W}}_{{m{\rm{o}}}}^{\left(k\right)}\in {\mathbf{R}}^{{d}_{{h}_{v}}}\times {\mathbf{R}}^{{d}_{{h}_{v}}}，{\boldsymbol{b}}_{m{\rm{i}}}^{\left(k\right)},{\boldsymbol{b}}_{m{\rm{o}}}^{\left(k\right)}\in {\mathbf{R}}^{{d}_{{h}_{v}}}$ .因此，节点
$ {v}_{i} $ 的状态向量的第$ k $ 次更新为h(k)vi=m(k)vi+h(k−1)vi. (10) 第K次迭代后，EW-GNN在图聚合阶段对图中所有节点状态向量进行池化，以生成最后的公式图向量：
hG=1|V|K∑k=1h(k)vi,vi∈V. (11) 这里，采用了平均池化对整个节点维度上的节点特征求平均值.
2.2 二元分类器
分类模型的输入是图向量对
$({\boldsymbol{h}}_{{\rm{conj}}},{\boldsymbol{h}}_{{\rm{prem}}})$ ，分别表示结论和候选的前提. EW-GNN通过分类函数${F}_{{\rm{class}}}$ 对前提在结论证明中的有用性进行预测：ˆz=Fclass([hconj;hprem]), (12) 式中：
$\hat{\textit{z}}\in {\bf{R}}^{2}$ 为候选前提在给定结论有用和无用类别的对应得分.${F}_{{\rm{class}}}$ 在本文中被设计为多层感知机（multi-layer perceptron，MLP）. 具体为Fclass(•)=W2(ReLU(W1(•)+b1))+b2, (13) 式中：
${\boldsymbol{W}}_{1}\in {{{\bf{R}}}}^{{d}_{{h}_{v}}}\times {{{\bf{R}}}}^{2{d}_{{h}_{v}}}$ 和${\boldsymbol{W}}_{2}\in {{{\bf{R}}}}^{2}\times {{{\bf{R}}}}^{{d}_{{h}_{v}}}$ 为不同的学习矩阵；${\boldsymbol{b}}_{1}\in {{{\bf{R}}}}^{{d}_{{h}_{v}}}$ 和${\boldsymbol{b}}_{1}\in {{{\bf{R}}}}^{2}$ 为学习偏差向量.$ \mathrm{R}\mathrm{e}\mathrm{L}\mathrm{U}({\text{•}}) $ 为修正线性单元（rectified linear unit，ReLU）函数：ReLU(x)={x,x>0,0,x⩽ (14) 因此，前提在两个类别下的预测概率为
\hat{\boldsymbol{y}}={\rm{softmax}}\left(\hat{\textit{z}}\right), (15) 式中：
$ \mathrm{s}\mathrm{o}\mathrm{f}\mathrm{t}\mathrm{m}\mathrm{a}\mathrm{x} ({\text{•}})$ 为归一化函数.$\hat{\boldsymbol{y}}$ 中的每一元素$\hat{y}_{a}$ 在$ \mathrm{s}\mathrm{o}\mathrm{f}\mathrm{t}\mathrm{m}\mathrm{a}\mathrm{x} ({\text{•}})$ 函数中的计算为\hat{{y}}_{a}=\dfrac{{{\rm{e}}}^{\hat{{\textit{z}}}_{a}}}{{\displaystyle \sum\limits_b }{{\rm{e}}}^{\hat{{\textit{z}}}_{b}}}, (16) 式中：
${\hat{{\textit{z}}}_{a}} $ 、${\hat{{\textit{z}}}_{b}} $ 分别为${\hat{{\textit{z}}}} $ 中第a、b个元素.2.3 损失函数
在均衡数据集下，对于每一个{结论,前提}对，损失函数
$ \mathcal{L} $ 定义为预测值$ \hat{\boldsymbol{y}} $ 和真实值y之间的交叉熵：\mathcal{ L}\left(\boldsymbol{y},\hat{\boldsymbol{y}}\right)=\displaystyle\sum \limits_{C}{y}_{C}\mathrm{ln}\left({\hat{y}}_{C}\right) + \left(1-{y}_{C}\right)\mathrm{ln}\left(1-{\hat{y}}_{C}\right), (17) 式中：
$ \boldsymbol{y} $ 为真实值的一个独热编码；${y}_{C}$ 和${\hat{y}}_{C}$ 分别为真实值$ \boldsymbol{y} $ 和预测值$ \hat{\boldsymbol{y}} $ 在第$C$ 类别下的对应值.在非均衡数据集下，对于每一个{结论，前提}对，损失函数
$ \mathcal{L} $ 定义为预测值$ \hat{\boldsymbol{y}} $ 和真实值$ \boldsymbol{y} $ 之间的加权交叉熵：\mathcal{L}\left(\boldsymbol{y},\hat{\boldsymbol{y}}\right)=\displaystyle\sum\limits _{C}{w}_{ + }{y}_{C}\mathrm{ln}\left({\hat{y}}_{C}\right) + {w}_-\left(1-{y}_{C}\right)\mathrm{ln}\left(1-{\hat{y}}_{C}\right), (18) 式中：
$ {w}_{ + } $ 、$ {w}_{-} $ 分别为正、负样本的权重，且$ {w}_{ + } > {w}_{-} $ .在本文的模型训练中，
$ {w}_{ + } $ 和$ {w}_{-} $ 分别设置为{w}_{ + }=\dfrac{N_{\rm{P}} + N_{\rm{N}}}{N_{\rm{P}}}, (19) {w}_-=\frac{N_{\rm{P}} + N_{\rm{N}}}{N_{\rm{N}}}, (20) 式中：
$ N_{\rm{P}} $ 、$ N_{\rm{N}} $ 分别为数据集中正、负样本的数量.3. 数据集
本文基于MPTP2078问题库[11]建立了一个用于训练、验证和测试前提选择模型的数据集.
MPTP2078问题库中一共包含2 078个问题，均来自Mizar数学库（Mizar Mathematical Library，MML）[21]中与Bolzano-Weierstrass公理相关的问题. 问题库所有问题的前提和结论均被TPTP系统形式化为一阶逻辑公式，且公式按照它们在Mizar数学库中出现的顺序线性排序. 即，出现在每一个结论之前的公式（前提和其他结论）均可作为证明该结论的前提. 问题的前提数量在区间[10, 4563]中，且前提的平均数量为1 876. 表1具体地描述了问题库中结论和前提的情况.
表 1 MPTP2078问题库描述Table 1. Description of MPTP2078 benchmark条 名称 公式 结论 最小前提 最大前提 平均前提 数量 4 564 2 078 10 4 563 1 876 数据集中每一个例子是一个三元组{结论,前提,标签}. 其中：前提是给定结论的候选前提，标签是二元分类中的类别；标记为1的样本记为正样本，表示前提对结论有用；标记为0的样本记为负样本，表示前提对结论无用. 在问题库中，ATPboost[13]证明了1469个结论并一共产生了24087个证明，这意味着一个结论可能对应多个证明.
正式地，每一个被证明的结论
$ c $ 有${n_{\rm c}}$ （${n_{\rm c}}\geqslant 1$ ）个证明$ {P}_{1} $ ，$ {P}_{2} ,\cdots,{P}_{r},\cdots,$ $ {P}_{n_{{\rm c}}} $ ，且$ {P}_{r}=\{{p}_{r1},{p}_{r2},\cdots, {p}_{rt},$ $ \cdots,{p}_{r{n_{{\rm c }r}}}\}$ ，其中：$ {p}_{rt} $ 为构造证明$ {P}_{r} $ 的一个前提，$ {n_{{\rm c}r}} $ 是$ {P}_{r} $ 中有用前提的总数. 因此，有用前提集$ {\mathcal{U}}_{P}\left(c\right)= {\bigcup }_{r=1}^{n_{\rm c}}{P}_{r} $ 包含至少在结论$ c $ 的所有证明中出现一次的前提.在数据集的构造中，对每一个已证明结论
$ c $ ，其对应的正样本中的前提来自$ {\mathcal{U}}_{P}\left(c\right) $ . 因此，结论$ c $ 对应的正样本为$ \left(c,p,1\right) $ （$ \forall p\in {\mathcal{U}}_{P}\left(c\right) $ ）且正样本的总数为$ \left|{\mathcal{U}}_{P}\left(c\right)\right| $ .然而，问题库中极大部分结论都对应了一个大规模的前提集且
$ {\mathcal{U}}_{P}\left(c\right) $ 包含的有用前提数量仅仅只占总前提数量非常小的一部分. 例如，MPTP2078问题库中的结论$ \mathrm{t}12\_\mathrm{y}\mathrm{e}\mathrm{l}\mathrm{l}\mathrm{o}\mathrm{w}\_6 $ 一共包含3836个前提，但只有5个前提被用于证明结论. 这表明结论对应的无用前提数量远远大于有用前提数量. 因此，如果使用$ c $ 的所有无用前提来构造负样本，则正负样本的分布将极度不平衡.为构建与正样本数量相等的负样本，使用文献[22]设计的手工特征表示公式，并使用K近邻（K-nearest neighbor，KNN）[23]算法粗略地对结论的所有前提进行排序. 随后，选择对结论无用但排名靠前的前提构造负样本，其中，无用前提的数量和有用前提大致相同. 最终，整理得到的数据集如表2所示.
表 2 数据集划分Table 2. Division of datasets个 样本 训练集 验证集 测试集 正 27663 3417 3432 负 27556 3485 3471 总样本 55219 6902 6903 4. 实验结果与分析
本文使用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 参数设置Table 3. Setting of parameters参数 设置 节点向量维度$ {d}_{{h}_{v}} $ 64 边向量维度$ {d}_{{h}_{e}} $ 32 迭代次数 K/次 1 学习率 0.0010 学习率衰减系数 0.1 学习率衰减步长 50 轮次/轮 100 权重衰减 0.0001 批量大小/个 8 4.2 评价指标
为评估所提EW-GNN模型的性能，将该模型与具有代表性的图神经网络模型进行比较. 在前提选择任务中，需要根据模型的输出概率对前提进行排序. 因此，需要同时评估正、负样本的正确预测率. 若仅关心正样本的正确预测率，则过多的负样本被错误预测为正时会严重地影响前提的排序，即无用的前提可能会在排序的前列. 当数据集中正、负样本分布均衡时，本文选择准确率
$ {A}_{{\rm{ccuracy}}} $ 指标对模型进行对比分析.$ {A}_{{\rm{ccuracy}}} $ 代表模型判断当前前提对给定结论是否有用的准确程度：{A}_{{\rm{ccuracy}}}=\frac{{T}_{{\rm{P}}} + {T}_{{\rm{N}}}}{{T}_{{\rm{otal}}}}, (21) 式中：
$ {T}_{{\rm{otal}}} $ 为数据集中所有样本的数量；$ {T}_{{\rm{P}}} $ 为分类正确的正样本的数量；$ {T}_{{\rm{N}}} $ 为分类正确的负样本的数量.本文同时增加召回率
$ {R}_{{\rm{ecall}}} $ 、精确度$ {P}_{{\rm{recision}}} $ 和F1指标F1对模型进行评估：{R}_{{\rm{ecall}}}=\frac{{T}_{{\rm{P}}}}{{T}_{{\rm{P}}} + {F}_{{\rm{N}}}}, (22) {P}_{{\rm{recision}}}=\frac{{T}_{{\rm{P}}}}{{T}_{{\rm{P}}} + {F}_{{\rm{P}}}}, (23) {F}_{1}=\frac{2{P}_{{\rm{recision}}} {R}_{{\rm{ecall}}}}{{P}_{{\rm{recision}}} + {R}_{{\rm{ecall}}}}, (24) 式中：
$ {F}_{{\rm{N}}} $ 为分类错误的负样本的数量；$ {F}_{{\rm{P}}} $ 为分类错误的正样本的数量.4.3 实验结果分析
为保证对比结果的有效性，实验过程中，只改变前提选择模型中图神经网络模型的部分，而不改变初始化模型以及二元分类模型. 所有方法在均衡数据集上的评估结果如表4所示，最佳结果以黑体突出显示.
表 4 数据集上的对比实验结果Table 4. Comparision of experimental results on datasets实验结果表明，所提出的基于边权重的图神经网络EW-GNN在前提选择任务中明显优于目前其他流行的图神经网络模型：EW-GNN在相同的测试集上至少提高了1%的分类准确率. 从表3中可以看出：除了本文提出的EW-GNN模型，没有另一个模型的分类准确率能够高于其他模型1%. 这说明双向地传播邻接节点的信息有助于帮助图神经网络模型生成更有表征能力的逻辑公式图向量. EW-GNN在更新节点状态向量之间，会首先对边状态向量进行更新. 根据对边类型的构造，边向量既能反映由对应边连接的节点类型，也能反映出节点的顺序. 这对表征一阶逻辑公式非常重要. 因为在一阶逻辑公式图中，不同类型的邻接节点对中心节点的贡献度是不同的. 直觉地，函数节点的贡献明显要大于变量节点，因为变量在一阶逻辑公式的表征中通常都被忽略. 同样地，节点的顺序同样也是逻辑公式图表征不可忽略的重要特性. 如，
$ \forall xp(x,a) $ 和$ \forall xp(a,x) $ 是两个不同的逻辑公式，如果忽略了$ x $ 和$ a $ 的顺序，会导致这两个逻辑公式最终生成的图向量是一样的. 因此，EW-GNN根据更新后的边状态向量为中心节点的每个邻接节点赋予权重，更加符合一阶逻辑公式的特性. 相比之下，本文所提出的EW-GNN模型更加适用于一阶逻辑中的前提选择任务.5. 结 论
1） 本文针对一阶逻辑公式的特性，提出了双向图表示方法，并对每条边设计了能够表示对应节点类型和顺序的边类型.
2） 根据双向图的特性，本文设计并实现了一种基于边权重的图神经网络模型EW-GNN. 该模型既能够双向地传播节点信息，也能利用边向量编码对应节点的类型和顺序.
3） 与当前流行的图神经网络模型相比，本文提出的模型明显在前提选择任务中更具有优势.
4） 针对一阶逻辑公式的特性，未来计划提出更加具有针对性的表征学习模型.
-
图 1 一阶逻辑公式的双向图表示
Figure 1. Bidirectional graph representation of first-order logical formula
表 1 MPTP2078问题库描述
Table 1. Description of MPTP2078 benchmark
条 名称 公式 结论 最小前提 最大前提 平均前提 数量 4 564 2 078 10 4 563 1 876 
下载: 导出CSV
表 2 数据集划分
Table 2. Division of datasets
个 样本 训练集 验证集 测试集 正 27663 3417 3432 负 27556 3485 3471 总样本 55219 6902 6903
下载: 导出CSV
表 3 参数设置
Table 3. Setting of parameters
参数 设置 节点向量维度$ {d}_{{h}_{v}} $ 64 边向量维度$ {d}_{{h}_{e}} $ 32 迭代次数 K/次 1 学习率 0.0010 学习率衰减系数 0.1 学习率衰减步长 50 轮次/轮 100 权重衰减 0.0001 批量大小/个 8
下载: 导出CSV
-
[1] KERN C, GREENSTREET M R. Formal verification in hardware design: a survey[J]. ACM Transactions on Design Automation of Electronic Systems (TODAES), 1999, 4(2): 123-193. doi: 10.1145/307988.307989 [2] KLEIN G, ELPHINSTONE K, HEISER G, et al. seL4: Formal verification of an OS kernel[C]//Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. Big Sky: ACM, 2009: 207-220. [3] LEROY X. Formal verification of a realistic compiler[J]. Communications of the ACM, 2009, 52(7): 107-115. doi: 10.1145/1538788.1538814 [4] KOVÁCS L, VORONKO A. First-order theorem proving and vampire[C]//25th International Conference on Computer Aided Verification. Saint Petersburg: [s.n.], 2013: 1-35. [5] SCHULZ S. E – a brainiac theorem prover[J]. Ai Communications, 2002, 15(2/3): 111-126. [6] SUTCLIFFE G. The TPTP problem library and associated infrastructure[J]. Journal of Automated Reasoning, 2017, 59(4): 483-502. doi: 10.1007/s10817-017-9407-7 [7] KALISZYK C, URBAN J. MizAR 40 for mizar 40[J]. Journal of Automated Reasoning, 2015, 55(3): 245-256. doi: 10.1007/s10817-015-9330-8 [8] MCCUNE W W. Otter 3.0 reference manual and guide[R]. Chicago: Argonne National Lab., 1994. [9] MENG J, PAULSON L C. Lightweight relevance filtering for machine-generated resolution problems[J]. Journal of Applied Logic, 2009, 7(1): 41-57. doi: 10.1016/j.jal.2007.07.004 [10] HODER K, VORONKOV A. Sine qua non for large theory reasoning[C]//23th International Conference on Automated Deduction. Wroclaw: [s.n.], 2011: 299-314. [11] ALAMA J, HESKES T, KÜHLWEIN D, et al. Premise selection for mathematics by corpus analysis and kernel methods[J]. Journal of Automated Reasoning, 2014, 52(2): 191-213. doi: 10.1007/s10817-013-9286-5 [12] KALISZYK C, URBAN J, VYSKOČIL J. Efficient semantic features for automated reasoning over large theories[C]//Proceedings of the 24th International Conference on Artificial Intelligence. [S.l.]: AAAI Press, 2015: 3084-3090. [13] PIOTROWSKI B, URBAN J. ATPboost: learning premise selection in binary setting with ATP feedback[C]//International Joint Conference on Automated Reasoning. Cham: Springer, 2018: 566-574. [14] ALEMI A A, CHOLLET F, EEN N, et al. DeepMath-deep sequence models for premise selection[C]// Proceedings of the 30th International Conference on Neural Information Processing Systems. Barcelona: Curran Associates Inc., 2016: 2243-2251. [15] WANG M, TANG Y, WANG J, et al. Premise selection for theorem proving by deep graph embedding[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. Long Beach: Curran Associates Inc., 2017: 2783-2793. [16] CROUSE M, ABDELAZIZ I, CORNELIO C, et al. Improving graph neural network representations of logical formulae with subgraph pooling[EB/OL]. (2019-11-15). https://arxiv.org/abs/1911.06904. [17] PALIWAL A, LOOS S, RABE M, et al. Graph representations for higher-order logic and theorem proving[C]//34th Proceedings of the AAAI Conference on Artificial Intelligence. Palo Alto: AAAI Press, 2020: 2967-2974. [18] KIPF T N, WELLING M. Semi-supervised classification with graph convolutional networks[DB/OL]. (2016-09-09). https://doi.org/10.48550/arXiv.1609.02907. [19] VELIČKOVIĆ P, CUCURULL G, CASANOVA A, et al. Graph attention networks[DB/OL]. (2017-10-30). https://doi.org/10.48550/arXiv.1710.10903. [20] ROBINSON A J, VORONKOV A. Handbook of automated reasoning[M]. [S.l.]: Elsevier, 2001. [21] Rudnicki P. An overview of the Mizar project[C]//Proceedings of the 1992 Workshop on Types for Proofs and Programs. [S.l.]: Chalmers University of Technology, 1992: 311-330. [22] JAKUBŮVJ, URBAN J. ENIGMA: efficient learning-based inference guiding machine[C]//International Conference on Intelligent Computer Mathematics. Cham: Springer, 2017: 292-302. [23] COVER T, HART P. Nearest neighbor pattern classification[J]. IEEE Transactions on Information Theory, 1967, 13(1): 21-27. [24] PASZKE A, GROSS S, MASSA F, et al. PyTorch: an imperative style, high-performance deep learning library[DB/OL]. (2019-12-03). https://arxiv.org/abs/1912.01703 [25] FEY M, LENSSEN J E. Fast graph representation learning with PyTorch geometric[DB/OL]. (2019-03-06). https://arxiv.org/abs/1903.02428 [26] KINGMA D P, BA J. Adam: a method for stochastic optimization[DB/OL]. (2014-12-22). https://arxiv.org/abs/1412.6980. [27] HAMILTON W L, YING R, LESKOVEC J. Inductive representation learning on large graphs[C]//Proceedings of the 31st International Conference on Neural Information Processing Systems. Long Beach: [s.n.], 2017: 1025-1035. [28] WU F L, SOUZA A H, ZHANG T Y, et al. Simplifying graph convolutional networks[C]// International Conference on Machine Learning. [S.l.]: PMLR, 2019: 6861-6871. [29] DEFFERRARD M, BRESSON X, VANDERGHEYNST P. Convolutional neural networks on graphs with fast localized spectral filtering[C]//Proceedings of the 30th International Conference on Neural Information Processing Systems. Barcelona: [s.n.], 2016: 3844-3852. -
下载:
下载:
点击查看大图
计量
- 文章访问数: 503
- HTML全文浏览量: 308
- PDF下载量: 36
- 被引次数: 0