劉清華，徐 揚，吳貫鋒，李瑞杰

（1.西南交通大學(xué)信息科學(xué)與技術(shù)學(xué)院，四川 成都 611756；2.西南交通大學(xué)系統(tǒng)可信性自動驗證國家地方聯(lián)合工程實驗室，四川 成都 610031；3.西南交通大學(xué)數(shù)學(xué)學(xué)院，四川 成都 611756；4.西南交通大學(xué)交通運輸與物流學(xué)院，四川 成都 611756）

自動推理作為計算機科學(xué)和數(shù)理邏輯的交叉學(xué)科，是人工智能的核心分支.一階邏輯（first-order logic，F(xiàn)OL）自動定理證明最初僅為了自動地證明數(shù)學(xué)定理，而目前已廣泛地應(yīng)用于其他領(lǐng)域，例如電路設(shè)計、軟件驗證、硬件驗證和管理等[1-3].先進的一階邏輯自動定理證明器（automated theorem prover，ATP），如Vampire[4]和E[5]，擅長在TPTP （thousands of problems for theorem provers）[6]的某些限定領(lǐng)域中證明問題，但卻很難高效地證明大型問題庫中的問題（如，MizAR數(shù)學(xué)庫[7]）.這些大規(guī)模的問題被稱為大理論問題，其通常包含成千上萬個前提，但只有極少部分的前提能對問題結(jié)論的證明起到有效作用.

在FOL中，問題的前提和結(jié)論被形式化為一階邏輯公式.大多數(shù)ATP主要基于Given Clause算法[8]對從公式轉(zhuǎn)換而來的子句（合取范式）進行證明搜索.證明搜索是在兩個集合上執(zhí)行：未處理子句集和已處理子句集.在證明搜索開始前，所有輸入子句都是未處理的.Given Clause算法反復(fù)地從未處理子句集中選擇一個子句作為給定子句，并將所有可能的推理規(guī)則應(yīng)用于該子句和已處理子句集中的其他子句； 最后，新選擇的給定子句被放入已處理子句集中，新生成的子句被置于未處理子句中.此證明搜索過程將一直持續(xù)直到超出計算資源限制，或推斷出空子句或已處理子句集變得飽和（無法推斷出任何新子句）.

傳統(tǒng)ATP在證明大理論時，由于問題包含了數(shù)量極多的前提，在上述證明搜索的過程中，搜索空間會呈爆炸型增長.因此，計算機資源會很快地被耗盡，進而導(dǎo)致ATP證明問題的性能大幅降低.該問題導(dǎo)致了ATP無法在證明大理論問題時充分發(fā)揮作用.解決該問題的一種有效方法是在ATP試圖找到結(jié)論的證明之前，盡可能地選擇出最可能參與證明構(gòu)造的前提.該過程被稱為前提選擇，通常作為ATP預(yù)處理的一部分，其對解決大規(guī)模問題至關(guān)重要.

起初，前提選擇通常采用基于公式中符號的啟發(fā)式方法[9-10]，主要通過計算和比較公式中的符號，對公式的相關(guān)性進行分析.最近，結(jié)合傳統(tǒng)機器學(xué)習(xí)技術(shù)[11-13]的前提選擇模型展現(xiàn)了具有競爭力的結(jié)果，但基于傳統(tǒng)機器學(xué)習(xí)的前提選擇在編碼邏輯公式時強烈地依賴于手工設(shè)計的特征（如，符號和子項等）.因為深度學(xué)習(xí)方法，如長短期記憶神經(jīng)網(wǎng)絡(luò)（long-short term memory，LSTM）[14]和圖神經(jīng)網(wǎng)絡(luò)（graph neural network，GNN）[15-17]，在編碼邏輯公式時不需要依賴于任何人工設(shè)計的特征，得到了越來越多學(xué)者的關(guān)注.又因為邏輯公式可以自然而然地表示為能夠保留公式句法和語義信息的有向無環(huán)圖（directed acyclic graph，DAG），所以定理證明與GNN的結(jié)合是當(dāng)前最熱門的研究主題之一.

目前，主流的圖神經(jīng)網(wǎng)絡(luò)框架通常通過聚集鄰接節(jié)點的信息來更新目標(biāo)節(jié)點的特征表示.在此框架下的圖神經(jīng)網(wǎng)絡(luò)模型常用于處理無向圖，如圖卷積神經(jīng)網(wǎng)絡(luò)（graph convolutional network，GCN）[18]、圖注意力神經(jīng)網(wǎng)絡(luò)（graph attention network，GAT）[19]等.然而，公式圖是有向，當(dāng)前的圖神經(jīng)網(wǎng)絡(luò)模型只能單向地沿著公式圖的邊進行信息傳播.除此之外，邏輯圖中相應(yīng)的子節(jié)點之間是有順序的，而目前的圖神經(jīng)網(wǎng)絡(luò)模型的信息聚集操作通常與子節(jié)點的順序無關(guān).為發(fā)揮邏輯公式圖表示的優(yōu)勢，理想的方法是根據(jù)公式的特性對公式圖中的節(jié)點進行排序并雙向地傳遞鄰接節(jié)點的信息.

針對上述問題，提出一種帶有邊類型的雙向圖用于表示一階邏輯公式.圖中相鄰的兩個節(jié)點由不同方向的兩條邊連接且每條邊都有一種對應(yīng)的邊類型.通過確定每條邊特定的邊類型，可以對雙向圖中的節(jié)點進行排序.基于新的公式圖表示，提出了一種基于邊權(quán)重的圖神經(jīng)網(wǎng)絡(luò)模型，即EW-GNN （edgeweight-based graph neural network）.對圖中的每一個方向，EW-GNN首先利用節(jié)點的信息更新對應(yīng)邊類型的特征表示，隨后利用更新后的邊類型特征計算鄰接節(jié)點對中心節(jié)點的權(quán)重.傳遞給中心節(jié)點的信息是鄰接節(jié)點信息的加權(quán)和.EW-GNN最后匯聚中心節(jié)點來自兩個方向上的信息，并對節(jié)點進行更新.實驗比較分析表明：當(dāng)前主流模型在測試集上的分類準(zhǔn)確率兩兩之差均小于1%，而提出的EW-GNN在相同的測試集上比表現(xiàn)最優(yōu)的模型還能提高約1%的分類準(zhǔn)確率.因此，EW-GNN能夠在前提選擇任務(wù)中表現(xiàn)得更加優(yōu)越.

1 一階邏輯公式圖表示

1.1 一階邏輯公式

在一階邏輯中[20]，給定一個變量符號集 V，一個函數(shù)符號集 F，以及一個謂詞符號集 P.一階邏輯項（term）是一個變量項v∈V或者形如f(t1,t2,···,tn)的函數(shù)項，其中，f∈F為n（n≥0）元函數(shù)符，t1，t2,···,tn是項.一階邏輯原子（atom）形如P(t1,t2,···,tn)，其中，P∈P為n（n≥1）元謂詞符.一階邏輯公式是由一階邏輯聯(lián)結(jié)詞 C={～,∧,∨,→,?}、量詞 Q={?,?}和原子聯(lián)結(jié)而成.

1.2 圖定義

帶有邊類型的雙向圖定義為G=(V,E,RE)，其中：節(jié)點集V={v1,v2,···,vn} 包含G中所有節(jié)點；邊集E={〈vi,vj〉|vi,vj∈V} 包含G中所有邊，有向?qū)ij=〈vi,vj〉 表示從節(jié)點vi到節(jié)點vj的有向邊；邊類型集包含G中所有邊對應(yīng)的邊類型.節(jié)點vi的鄰接節(jié)點集定義為 N(vi)= {vj|eji∈E}.圖中的每一個節(jié)點v都伴隨著一個初始節(jié)點特征向量xv∈Rdv，每一條邊e也伴隨著一個初始邊特征向量xe∈Rde，表示其對應(yīng)的邊類型.dv和de分別為xv和xe的初始向量維度.

1.3 表 示

一階邏輯公式能夠自然地表示為語義解析樹（abstract semantic tree，AST）.通過添加從量詞節(jié)點指向到相應(yīng)被約束的變量節(jié)點的邊以及合并所有相同的子表達式對應(yīng)的子樹，可以將表示公式的AST擴展為含有根節(jié)點的DAG.

為了保持邏輯公式圖中部分節(jié)點之間有序性以及雙向傳遞鄰接節(jié)點的信息，設(shè)計了雙向圖表示，其中圖中相鄰的兩個節(jié)點由方向不同的兩條邊連接且每條邊都具有一種對應(yīng)的邊類型.

邏輯公式圖中的節(jié)點大致可分為5種類型：量詞、邏輯聯(lián)結(jié)詞、謂詞、函數(shù)和變量.在定義邊類型時，邏輯連接詞節(jié)點、量詞節(jié)點和特殊的相等謂詞（=）節(jié)點的名稱為其類型，而其他謂詞、函數(shù)以及變量節(jié)點的類型為其對應(yīng)的類型，分別記為pred、func和var.

然而，對邏輯公式圖中的子節(jié)點進行排序仍是一個難題.利用文獻[16]中提出的排序方案，從上往下單向地定義節(jié)點順序，即在給定相應(yīng)父節(jié)點類型的情況下，對其子節(jié)點進行排序：

1）如果父節(jié)點是邏輯聯(lián)結(jié)詞 ～、∧、∨、? 或 =，則它們對應(yīng)的子節(jié)點的順序一樣；

2）如果父節(jié)點是量詞 ? 或 ?，則其變量子節(jié)點具有相同的順序，而其他子節(jié)點是線性排序的；

3）如果父節(jié)點是其他謂詞、邏輯連接詞或函數(shù)，則其子節(jié)點是線性排序的.

正式地，一階邏輯表達式s的雙向圖表示Gs=(Vs,Es,Rs)構(gòu)造如下：

1）如果s是一個變量項或常量項（0元函數(shù)項），則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）在遞歸構(gòu)造完Gs后，用統(tǒng)一的標(biāo)記 * 更替Gs中所有變量節(jié)點的名稱；

5）Rs中的每一個邊類型由對應(yīng)連接的兩個節(jié)點的類型和節(jié)點順序決定.

圖1為一階邏輯公式 ?x,y(p(f(x),a)∨q(a,f(y)))的雙向圖表示，其中：y(?)為變量；p(?)和q(?)為謂詞函數(shù)；f(?)和a分別為一元函數(shù)和零元函數(shù)（常元）.

圖1 一階邏輯公式的雙向圖表示Fig.1 Bidirectional graph representation of first-order logical formula

在圖1中，變量節(jié)點x和y被替換成了統(tǒng)一的標(biāo)記 *，替換后的雙向圖能在變量更名下保持一致.兩種不同顏色的邊分別代表了圖中兩個不同的方向.與單向圖相比，雙向圖中的每個節(jié)點有來自兩個方向上鄰接節(jié)點，如 ?、P和Q都是圖中的節(jié)點 ∨的鄰接節(jié)點.通過給圖中的邊添加類型，可以在一定程度上對圖中的相關(guān)節(jié)點進行排序.如在節(jié)點 ? 下，變量節(jié)點x和y（即節(jié)點*）的順序相同且記為1，因此節(jié)點 ∨ 的順序自然地記為2.連接節(jié)點 ? 和 ∨ 的兩條邊上的順序均為 ∨ 在從上到下的單向圖的中作為 ? 的子節(jié)點的順序.除此之外，邊類型同樣也反映出了邊的方向.邊類型 ?_∨_2和 ∨ _?_2分別表示從節(jié)點 ? 指向節(jié)點 ∨ 的邊和從節(jié)點 ∨ 指向節(jié)點 ? 的邊.

2 模 型

所有前提選擇模型都具有相似的框架，即，對邏輯公式進行表示并計算公式間的相關(guān)性.其正式定義如下：

定義1[11]給定一個結(jié)論c和其前提集A，前提選擇需要預(yù)測并選擇A中可能對證明c有用的前提.

如圖2所示，一個完整的端到端基于圖神經(jīng)網(wǎng)絡(luò)的前提選擇模型應(yīng)包含以下3部分：公式圖表示、圖神經(jīng)網(wǎng)絡(luò)模型和二元分類器.在本文中，首先，將一階邏輯公式轉(zhuǎn)化為帶有邊類型的雙向圖；其次，通過使用新提出的EW-GNN模型，將邏輯公式圖編碼為特征向量；最后，二元分類器將一個結(jié)論向量和一個候選前提向量的拼接作為輸入，并輸出一個 [0,1]之間的實數(shù)得分，該得分表明在證明結(jié)論中使用候選前提的概率.

圖2 基于圖神經(jīng)網(wǎng)絡(luò)的前提選擇模型Fig.2 Premise selection model based on graph neural network

給定一個大理論問題和訓(xùn)練后的前提選擇模型，可以將所有的{結(jié)論,前提}對反饋給前提選擇模型，并輸出每個前提對結(jié)論有用（無用）的概率.根據(jù)輸出的概率，可以對前提進行排序，并從排序中選擇出前np個前提作為給定結(jié)論的有用前提.最后，ATP將使用np個選定的前提自動地證明對應(yīng)的結(jié)論，從而解決ATP搜索空間爆炸增長的問題.

2.1 基于邊權(quán)重的圖神經(jīng)網(wǎng)絡(luò)

EW-GNN模型包括4個階段：初始化、消息聚合、消息傳播（節(jié)點更新）以及圖聚合.

在初始化階段，模型通過不同的嵌入函數(shù)Fv和Fe將任意初始節(jié)點特征向量xv和初始邊特征向量xe分別映射為初始節(jié)點狀態(tài)向量和初始邊狀態(tài)向量：

Fv和Fe在本文中被設(shè)計為不同的查找表，用于存儲固定字典和大小的嵌入，并將用熱獨（one-hot）向量表示的xv和xe分別編碼為固定大小的初始狀態(tài)向量.

在第k（k=1,2,···,K）次信息聚集階段，EWGNN根據(jù)邊的方向，分別聚集目標(biāo)節(jié)點vi來自兩個方向上的鄰接節(jié)點vj的信息.這里，簡單地把邊的方向分為從上往下和從下往上.為計算vj對vi的權(quán)重，首先利用vj和vi第k? 1次狀態(tài)向量和，以及第k? 1次邊狀態(tài)向量對第k次邊狀態(tài)向量進行更新：

如果eji的方向是從上往下的，則

如果eji的方向是從下往上的，則

利用更新后的邊狀態(tài)向量，領(lǐng)接節(jié)點vj對中心節(jié)點vi的權(quán)重的計算如下：

如果eji的方向是從上往下的，則

如果eji的方向是從下往上的，則

節(jié)點vi來自鄰接節(jié)點vj的聚合信息為

eji的方向不同，也隨之不同：

如果eji的方向是從上往下的，則

如果eji的方向是從下往上的，則

因此，節(jié)點vi的狀態(tài)向量的第k次更新為

第K次迭代后，EW-GNN在圖聚合階段對圖中所有節(jié)點狀態(tài)向量進行池化，以生成最后的公式圖向量：

這里，采用了平均池化對整個節(jié)點維度上的節(jié)點特征求平均值.

2.2 二元分類器

分類模型的輸入是圖向量對 (hconj,hprem)，分別表示結(jié)論和候選的前提.EW-GNN通過分類函數(shù)Fclass對前提在結(jié)論證明中的有用性進行預(yù)測：

Fclass在本文中被設(shè)計為多層感知機（multi-layer perceptron，MLP）.具體為

式中：W1∈Rdhv×R2dhv和W2∈R2×Rdhv為不同的學(xué)習(xí)矩陣；b1∈Rdhv和b1∈R2為學(xué)習(xí)偏差向量.ReLU(?)為修正線性單元（rectified linear unit，ReLU）函數(shù)：

因此，前提在兩個類別下的預(yù)測概率為

2.3 損失函數(shù)

在均衡數(shù)據(jù)集下，對于每一個{結(jié)論,前提}對，損失函數(shù) L 定義為預(yù)測值和真實值y之間的交叉熵：

式中：y為真實值的一個獨熱編碼；yC和分別為真實值y和預(yù)測值在第C類別下的對應(yīng)值.

在非均衡數(shù)據(jù)集下，對于每一個{結(jié)論，前提}對，損失函數(shù) L 定義為預(yù)測值和真實值y之間的加權(quán)交叉熵：

式中：w+、w?分別為正、負(fù)樣本的權(quán)重，且w+>w?.

在本文的模型訓(xùn)練中，w+和w?分別設(shè)置為

式中：NP、NN分別為數(shù)據(jù)集中正、負(fù)樣本的數(shù)量.

3 數(shù)據(jù)集

本文基于MPTP2078問題庫[11]建立了一個用于訓(xùn)練、驗證和測試前提選擇模型的數(shù)據(jù)集.

MPTP2078問題庫中一共包含2 078個問題，均來自Mizar數(shù)學(xué)庫（Mizar Mathematical Library，MML）[21]中與Bolzano-Weierstrass公理相關(guān)的問題.問題庫所有問題的前提和結(jié)論均被TPTP系統(tǒng)形式化為一階邏輯公式，且公式按照它們在Mizar數(shù)學(xué)庫中出現(xiàn)的順序線性排序.即，出現(xiàn)在每一個結(jié)論之前的公式（前提和其他結(jié)論）均可作為證明該結(jié)論的前提.問題的前提數(shù)量在區(qū)間[10, 4563]中，且前提的平均數(shù)量為1 876.表1具體地描述了問題庫中結(jié)論和前提的情況.

表1 MPTP2078問題庫描述Tab.1 Description of MPTP2078 benchmark條

數(shù)據(jù)集中每一個例子是一個三元組{結(jié)論,前提,標(biāo)簽}.其中：前提是給定結(jié)論的候選前提，標(biāo)簽是二元分類中的類別；標(biāo)記為1的樣本記為正樣本，表示前提對結(jié)論有用；標(biāo)記為0的樣本記為負(fù)樣本，表示前提對結(jié)論無用.在問題庫中，ATPboost[13]證明了1469個結(jié)論并一共產(chǎn)生了24087個證明，這意味著一個結(jié)論可能對應(yīng)多個證明.

正式地，每一個被證明的結(jié)論c有nc（nc≥1）個證明P1，P2,···,Pr,···,Pnc，且Pr={pr1,pr2,···,prt,···,prncr}，其中：prt為構(gòu)造證明Pr的一個前提，ncr是Pr中有用前提的總數(shù).因此，有用前提集 UP(c)=包含至少在結(jié)論c的所有證明中出現(xiàn)一次的前提.

在數(shù)據(jù)集的構(gòu)造中，對每一個已證明結(jié)論c，其對應(yīng)的正樣本中的前提來自 UP(c).因此，結(jié)論c對應(yīng)的正樣本為 (c,p,1)（?p∈UP(c)）且正樣本的總數(shù)為 |UP(c)|.

然而，問題庫中極大部分結(jié)論都對應(yīng)了一個大規(guī)模的前提集且 UP(c)包含的有用前提數(shù)量僅僅只占總前提數(shù)量非常小的一部分.例如，MPTP2078問題庫中的結(jié)論 t12_yellow_6一共包含3836個前提，但只有5個前提被用于證明結(jié)論.這表明結(jié)論對應(yīng)的無用前提數(shù)量遠遠大于有用前提數(shù)量.因此，如果使用c的所有無用前提來構(gòu)造負(fù)樣本，則正負(fù)樣本的分布將極度不平衡.

為構(gòu)建與正樣本數(shù)量相等的負(fù)樣本，使用文獻[22]設(shè)計的手工特征表示公式，并使用K近鄰（K-nearest neighbor，KNN）[23]算法粗略地對結(jié)論的所有前提進行排序.隨后，選擇對結(jié)論無用但排名靠前的前提構(gòu)造負(fù)樣本，其中，無用前提的數(shù)量和有用前提大致相同.最終，整理得到的數(shù)據(jù)集如表2所示.

表2 數(shù)據(jù)集劃分Tab.2 Division of datasets個

4 實驗結(jié)果與分析

本文使用Python編程實現(xiàn)了本模型.在模型搭建的過程中，使用Pytorch庫[24]進行深度學(xué)習(xí)算法的實現(xiàn)，并使用Pytorch_Geometric庫[25]處理數(shù)據(jù)和對實現(xiàn)文中提及的所有圖神經(jīng)網(wǎng)絡(luò).本次實驗在超微4029GP-TRT服務(wù)器上進行，具體軟硬件配置環(huán)境如下：CenterOS7.6 X64，Intel至強銀牌4114，256 GB內(nèi)存，2 TB SSD, 所用GPU為NViDIA RTX 2080Ti.

4.1 實驗參數(shù)

使用Adam[26]優(yōu)化器對模型進行訓(xùn)練.初始化的學(xué)習(xí)率為0.0010，在50個訓(xùn)練輪次后，學(xué)習(xí)率衰減為0.0001.在每個輪次后，對模型進行保存并在驗證集上進行評估.經(jīng)過所有輪次的訓(xùn)練和驗證后，選擇在驗證集上表現(xiàn)最佳（損失最?。┑哪Ｐ妥鳛樽顑?yōu)模型，并在測試集上對其進行評估.為了保證實驗結(jié)果的公平性，文章中所有涉及到的模型參數(shù)設(shè)置均一致.具體參數(shù)如表3所示.

表3 參數(shù)設(shè)置Tab.3 Setting of parameters

4.2 評價指標(biāo)

為評估所提EW-GNN模型的性能，將該模型與具有代表性的圖神經(jīng)網(wǎng)絡(luò)模型進行比較.在前提選擇任務(wù)中，需要根據(jù)模型的輸出概率對前提進行排序.因此，需要同時評估正、負(fù)樣本的正確預(yù)測率.若僅關(guān)心正樣本的正確預(yù)測率，則過多的負(fù)樣本被錯誤預(yù)測為正時會嚴(yán)重地影響前提的排序，即無用的前提可能會在排序的前列.當(dāng)數(shù)據(jù)集中正、負(fù)樣本分布均衡時，本文選擇準(zhǔn)確率Accuracy指標(biāo)對模型進行對比分析.Accuracy代表模型判斷當(dāng)前前提對給定結(jié)論是否有用的準(zhǔn)確程度：

式中：Total為數(shù)據(jù)集中所有樣本的數(shù)量；TP為分類正確的正樣本的數(shù)量；TN為分類正確的負(fù)樣本的數(shù)量.

本文同時增加召回率Recall、精確度Precision和F1指標(biāo)F1對模型進行評估：

式中：FN為分類錯誤的負(fù)樣本的數(shù)量；FP為分類錯誤的正樣本的數(shù)量.

4.3 實驗結(jié)果分析

為保證對比結(jié)果的有效性，實驗過程中，只改變前提選擇模型中圖神經(jīng)網(wǎng)絡(luò)模型的部分，而不改變初始化模型以及二元分類模型.所有方法在均衡數(shù)據(jù)集上的評估結(jié)果如表4所示，最佳結(jié)果以黑體突出顯示.

表4 數(shù)據(jù)集上的對比實驗結(jié)果Tab.4 Comparision of experimental results on datasets

實驗結(jié)果表明，所提出的基于邊權(quán)重的圖神經(jīng)網(wǎng)絡(luò)EW-GNN在前提選擇任務(wù)中明顯優(yōu)于目前其他流行的圖神經(jīng)網(wǎng)絡(luò)模型：EW-GNN在相同的測試集上至少提高了1%的分類準(zhǔn)確率.從表3中可以看出：除了本文提出的EW-GNN模型，沒有另一個模型的分類準(zhǔn)確率能夠高于其他模型1%.這說明雙向地傳播鄰接節(jié)點的信息有助于幫助圖神經(jīng)網(wǎng)絡(luò)模型生成更有表征能力的邏輯公式圖向量.EW-GNN在更新節(jié)點狀態(tài)向量之間，會首先對邊狀態(tài)向量進行更新.根據(jù)對邊類型的構(gòu)造，邊向量既能反映由對應(yīng)邊連接的節(jié)點類型，也能反映出節(jié)點的順序.這對表征一階邏輯公式非常重要.因為在一階邏輯公式圖中，不同類型的鄰接節(jié)點對中心節(jié)點的貢獻度是不同的.直覺地，函數(shù)節(jié)點的貢獻明顯要大于變量節(jié)點，因為變量在一階邏輯公式的表征中通常都被忽略.同樣地，節(jié)點的順序同樣也是邏輯公式圖表征不可忽略的重要特性.如，?xp(x,a) 和 ?xp(a,x) 是兩個不同的邏輯公式，如果忽略了x和a的順序，會導(dǎo)致這兩個邏輯公式最終生成的圖向量是一樣的.因此，EW-GNN根據(jù)更新后的邊狀態(tài)向量為中心節(jié)點的每個鄰接節(jié)點賦予權(quán)重，更加符合一階邏輯公式的特性.相比之下，本文所提出的EW-GNN模型更加適用于一階邏輯中的前提選擇任務(wù).

5 結(jié) 論

1）本文針對一階邏輯公式的特性，提出了雙向圖表示方法，并對每條邊設(shè)計了能夠表示對應(yīng)節(jié)點類型和順序的邊類型.

2）根據(jù)雙向圖的特性，本文設(shè)計并實現(xiàn)了一種基于邊權(quán)重的圖神經(jīng)網(wǎng)絡(luò)模型EW-GNN.該模型既能夠雙向地傳播節(jié)點信息，也能利用邊向量編碼對應(yīng)節(jié)點的類型和順序.

3）與當(dāng)前流行的圖神經(jīng)網(wǎng)絡(luò)模型相比，本文提出的模型明顯在前提選擇任務(wù)中更具有優(yōu)勢.

4）針對一階邏輯公式的特性，未來計劃提出更加具有針對性的表征學(xué)習(xí)模型.