一階邏輯中基于treelet圖神經(jīng)網(wǎng)絡(luò)的前提選擇

馬 雪,何星星,蘭詠琪,李瑩芳

(1.西南交通大學(xué)數(shù)學(xué)學(xué)院,四川 成都 611756;2.西南財(cái)經(jīng)大學(xué)計(jì)算機(jī)與人工智能學(xué)院,四川 成都 611130)

1 引言

自動(dòng)推理是人工智能研究領(lǐng)域中的一個(gè)重要方向,其目標(biāo)是利用計(jì)算機(jī)實(shí)現(xiàn)人類(lèi)的推理過(guò)程。自動(dòng)定理證明是自動(dòng)推理領(lǐng)域中的重要課題,其任務(wù)是研究自動(dòng)化系統(tǒng)的設(shè)計(jì),利用設(shè)計(jì)的系統(tǒng)對(duì)數(shù)學(xué)中提出的定理或猜想進(jìn)行推理和證明[1]。其研究成果已成功應(yīng)用于多個(gè)實(shí)際領(lǐng)域,如操作系統(tǒng)[2,3]、分布式系統(tǒng)[4,5]、編譯器[6,7]、微處理器設(shè)計(jì)[8]和數(shù)學(xué)問(wèn)題的求解[9]等。

當(dāng)推理規(guī)則確定后,自動(dòng)定理證明本質(zhì)上是一個(gè)搜索問(wèn)題,其目標(biāo)是尋找從前提集到給定的定理或猜想的一個(gè)演繹序列。經(jīng)典的自動(dòng)定理證明器ATPs(Automatic Theorem Provers)對(duì)于解決需要在較小的公理集上執(zhí)行復(fù)雜的推理步驟的問(wèn)題是有效的,然而,對(duì)于一些包含數(shù)百到數(shù)千萬(wàn)個(gè)公理的問(wèn)題,證明它們時(shí)搜索空間呈爆炸型增長(zhǎng),超出了自動(dòng)定理證明器的能力,并且大型知識(shí)庫(kù)中通常只有一小部分公理與給定的定理或猜想的證明相關(guān)。隨著大型邏輯理論的研究變得越來(lái)越廣泛[10-12],這種缺陷變得更加明顯。前提選擇是避免這種缺陷的有效方法,其任務(wù)是在證明器的預(yù)處理階段,選擇對(duì)給定的定理或猜想的證明有用的公理,這對(duì)縮小搜索空間,提高ATPs的性能發(fā)揮了關(guān)鍵作用。

前提選擇的研究最早是基于比較和分析符號(hào)手工設(shè)計(jì)啟發(fā)式方法[13]。隨后,機(jī)器學(xué)習(xí)方法提供了一些替代方案,如樸素貝葉斯方法[14]、K近鄰算法[15]等。Alama等[16]使用詞袋特征訓(xùn)練了一個(gè)基于內(nèi)核的分類(lèi)器,取得了很好的實(shí)驗(yàn)結(jié)果。Alama等[17]首次將深度學(xué)習(xí)應(yīng)用于大規(guī)模理論的前提選擇,有效避免了機(jī)器學(xué)習(xí)中依賴(lài)大量手工設(shè)計(jì)的特征。該方法利用長(zhǎng)短期記憶網(wǎng)絡(luò)LSTM(Long Short-Term Memory)[18]和GRU(Gated Recurrent Unit)[19]對(duì)成對(duì)的公理和猜想進(jìn)行訓(xùn)練,以確定最有可能與自動(dòng)證明相關(guān)的公理,該模型在Mizar語(yǔ)料庫(kù)的前提選擇任務(wù)中取得了良好的效果。

目前,前提選擇與深度學(xué)習(xí)的融合研究得到了較大發(fā)展[20-22],然而,邏輯公式的復(fù)雜性和結(jié)構(gòu)化性質(zhì)使其繼續(xù)發(fā)展具有挑戰(zhàn)性。2種最常用的保持公式結(jié)構(gòu)性質(zhì)的方法是Tree LSTM[18]和GNN(Graph Neural Network)[19]。當(dāng)將邏輯公式表示為解析樹(shù)時(shí),Tree LSTM 會(huì)生成表示全局解析樹(shù)的嵌入,但它們會(huì)遺漏邏輯公式中重要的信息,如共享子表達(dá)式等。相反,GNN能有效地捕捉共享子表達(dá)式,且由于邏輯公式可以轉(zhuǎn)化為有向無(wú)環(huán)圖DAG(Directed Acyclic Graph),GNN與前提選擇結(jié)合勢(shì)必有更廣泛的應(yīng)用前景。然而,主流圖神經(jīng)網(wǎng)絡(luò)通過(guò)對(duì)圖中單個(gè)節(jié)點(diǎn)的嵌入進(jìn)行簡(jiǎn)單池化生成最終公式的圖嵌入,其中每個(gè)節(jié)點(diǎn)僅包含了自身與鄰居節(jié)點(diǎn)的信息,缺乏了表征一階邏輯公式內(nèi)部語(yǔ)義與語(yǔ)法的信息,如邏輯公式圖(邏輯公式經(jīng)轉(zhuǎn)化得到的圖)上的節(jié)點(diǎn)順序信息等。

為解決圖神經(jīng)網(wǎng)絡(luò)進(jìn)行節(jié)點(diǎn)更新時(shí)忽略了節(jié)點(diǎn)順序信息的問(wèn)題,Wang等[23]提出一種面向高階邏輯的保序方法,由于高階邏輯公式中常元與變?cè)梢宰鳛橹祷蚝瘮?shù),這與一階邏輯公式不同,故該方法不適用于一階邏輯?；诖?本文提出一階邏輯保留邏輯公式圖上節(jié)點(diǎn)順序信息的方法,并基于此方法設(shè)計(jì)了適用于一階邏輯公式前提選擇任務(wù)的基于treelet的圖神經(jīng)網(wǎng)絡(luò)TL-GNN(TreeLet-based Graph Neural Network)模型。實(shí)驗(yàn)分析表明：在相同的測(cè)試集上,與主流圖神經(jīng)網(wǎng)絡(luò)模型相比,TL-GNN提高了約2% 的分類(lèi)準(zhǔn)確率;與同樣為編碼邏輯公式圖的子節(jié)點(diǎn)順序的圖神經(jīng)網(wǎng)絡(luò)模型EW-GNN(Edge-Weighted Graph Neural Network)[24]相比,TL-GNN可提高約1%的分類(lèi)準(zhǔn)確率。

2 相關(guān)工作

2.1 一階邏輯公式圖表示

定義1[25]一階邏輯中的項(xiàng),被遞歸定義為：

(1)常量符號(hào)是項(xiàng)。

(2)變量符號(hào)是項(xiàng)。

(3)若f是n元函數(shù)符號(hào),t1,t2,…,tn是項(xiàng),則f(t1,t2,…,tn)是項(xiàng)。

(4)所有項(xiàng)都是有限次使用(1)～(3)生成的符號(hào)串。

定義2[25]若P(x1,x2,…,xn)是n元謂詞符號(hào),t1,t2,…,tn是項(xiàng),則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)生成的符號(hào)串。

由于一階邏輯公式可以解析為樹(shù),為標(biāo)記量詞節(jié)點(diǎn)與其約束的變?cè)?jié)點(diǎn),添加由量詞節(jié)點(diǎn)指向被約束的變?cè)?jié)點(diǎn)的邊,同時(shí)將具有相同子表達(dá)式的子樹(shù)合并,可以得到一階邏輯公式對(duì)應(yīng)的有向無(wú)環(huán)圖。

一階邏輯公式可以通過(guò)如下過(guò)程轉(zhuǎn)化為DAG：(1)將邏輯公式轉(zhuǎn)化為解析樹(shù);(2)合并解析樹(shù)中具有相同子表達(dá)式的子樹(shù);(3)將相同節(jié)點(diǎn)進(jìn)行合并并以*替換。

圖1展示了一階邏輯公式Ф：?X?Y[(p(a,f(X))→q(b,Y))∨q(f(X),g(a,Y))]表示為DAG的全過(guò)程。

Figure 1 The process of representing Ф as a DAG圖1 一階邏輯公式Ф表示為DAG的過(guò)程

2.2 保序嵌入

Treelet[23]是為了保序嵌入而設(shè)計(jì)的特征。給定圖G上的一個(gè)節(jié)點(diǎn)v,〈v,w〉表示v的一條出邊,rv(w)∈{1,2,…}為〈v,w〉在v的所有出邊中的排序。G上的treelet為三元組(u,v,w)∈V×V×V,滿(mǎn)足〈v,u〉和〈v,w〉均為G中的邊,且在v的所有出邊的排序中,〈v,u〉排在〈v,w〉之前。換言之,一個(gè)treelet是一個(gè)包含頂部節(jié)點(diǎn)v、左子節(jié)點(diǎn)u和右子節(jié)點(diǎn)w的子圖。若τG表示G上treelet的集合,τG={(u,v,w)：〈v,u〉∈E,〈v,w〉∈E,rv(u)

假設(shè)圖2為某圖上截取的一個(gè)子圖,在圖2中,有3個(gè)treelets,分別為(u3,u1,v),(v,u2,u4),(u5,v,u6)。在(u3,u1,v)中,v為右子節(jié)點(diǎn);在(v,u2,u4)中,v為左子節(jié)點(diǎn);在(u5,v,u6)中,v為頂部節(jié)點(diǎn)。

Figure 2 A subgraph containing three treelets圖2 包含3個(gè)treelets的子圖

3 基于TL-GNN的前提選擇模型

本文為保留圖中子節(jié)點(diǎn)順序信息提出了TL-GNN,基于TL-GNN的前提選擇模型結(jié)構(gòu)如圖3所示,TL-GNN包含狀態(tài)向量初始化、信息聚合、信息傳播以及圖聚合4個(gè)部分。TL-GNN在信息聚合中聚集來(lái)自鄰接節(jié)點(diǎn)和treelet的信息,迭代地更新節(jié)點(diǎn)的狀態(tài)向量。最后,TL-GNN對(duì)圖中所有節(jié)點(diǎn)的最終狀態(tài)向量應(yīng)用池化操作以獲得前提與結(jié)論的圖向量表示,再將前提與結(jié)論的圖向量表示對(duì)(前提,結(jié)論)作為二元分類(lèi)器的輸入進(jìn)行分類(lèi)預(yù)測(cè)。

Figure 3 Premise selection model based on TL-GNN圖3 基于TL-GNN的前提選擇模型

3.1 TL-GNN

(1)

在節(jié)點(diǎn)信息聚合階段,TL-GNN從2部分聚集鄰居節(jié)點(diǎn)信息。第1部分聚集中心節(jié)點(diǎn)來(lái)自父節(jié)點(diǎn)與子節(jié)點(diǎn)的信息,第2部分以treelet的形式聚集中心節(jié)點(diǎn)的順序信息,最后聚集2部分的信息。

(2)

(3)

因此,第1部分中心節(jié)點(diǎn)的父節(jié)點(diǎn)信息與子節(jié)點(diǎn)信息可匯總為：

(4)

G=(V,E)為公式的有向圖,令τT(v)、τL(v)和τR(v)分別表示節(jié)點(diǎn)v作為treelet中頂部節(jié)點(diǎn)、左子節(jié)點(diǎn)及右子節(jié)點(diǎn)的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部分聚合中心節(jié)點(diǎn)v的順序信息中來(lái)自τ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 以中心節(jié)點(diǎn)C為例展示初始化、信息聚合及信息傳播過(guò)程

在圖聚合階段,TL-GNN對(duì)K次迭代后圖中所有節(jié)點(diǎn)的最終狀態(tài)向量進(jìn)行平均池化,生成最終的邏輯公式圖向量表示hg,如式(11)所示：

(11)

其中,hg∈Rdhv且AvgPool(·)表示對(duì)圖中所有節(jié)點(diǎn)的最終狀態(tài)向量進(jìn)行平均池化。不同函數(shù)在實(shí)驗(yàn)中的網(wǎng)絡(luò)配置如圖5所示。

3.2 二元分類(lèi)器與損失函數(shù)

在基于TL-GNN的前提選擇模型中,二元分類(lèi)器的輸入是前提與結(jié)論的圖表示向量對(duì)(hprem,hconj)。分類(lèi)器通過(guò)Fclass(·)函數(shù)預(yù)測(cè)前提是否對(duì)相應(yīng)結(jié)論的證明有用,如式(12)所示：

z=Fclass([hprem;hconj])

(12)

其中,z∈R2表示前提對(duì)相應(yīng)結(jié)論的證明是否有用的得分。

Fclass(·)被簡(jiǎn)單地設(shè)計(jì)為多層感知機(jī),如式(13)所示：

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

(13)

(14)

(15)

(16)

對(duì)于數(shù)據(jù)集中的每一樣本,采用交叉熵?fù)p失函數(shù)計(jì)算預(yù)測(cè)損失,如式(17)所示：

(17)

其中,y表示真實(shí)標(biāo)簽的獨(dú)熱編碼;yp表示真實(shí)值y在第p類(lèi)下對(duì)應(yīng)的值。

4 實(shí)驗(yàn)與結(jié)果分析

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

本文數(shù)據(jù)集基于MPTP2078(a subset of 2078 Mizar theorems)問(wèn)題庫(kù)[16]而創(chuàng)建,與文獻(xiàn)[24]中相同。

MPTP2078問(wèn)題庫(kù)中的2 078個(gè)問(wèn)題均被形式化為一階邏輯公式,問(wèn)題中的每個(gè)結(jié)論對(duì)應(yīng)一個(gè)大規(guī)模的前提集。本文將在結(jié)論證明過(guò)程中出現(xiàn)的前提記為有用前提,未出現(xiàn)在結(jié)論證明過(guò)程中的前提記為無(wú)用前提。由于前提集中通常包含大量的無(wú)用前提,導(dǎo)致有用前提與無(wú)用前提數(shù)量分布極不均衡。為此,本文使用K近鄰算法[15]對(duì)無(wú)用前提排序,對(duì)于問(wèn)題庫(kù)中的每一結(jié)論,根據(jù)其對(duì)應(yīng)的正樣本數(shù)量,選擇無(wú)用前提中排序靠前的相應(yīng)數(shù)量的前提作為負(fù)樣本,使得最終選用的無(wú)用前提數(shù)量與有用前提數(shù)量大致相同。表1展示了經(jīng)處理后的數(shù)據(jù)集分布情況。

Table 1 Distribution of sample size of dataset

Table 2 Experimental parameter settings

4.2 實(shí)驗(yàn)參數(shù)

本文實(shí)驗(yàn)的軟硬件配置如下：CenterOS 7.6 X64,Intel?至強(qiáng)?銀牌4114,256 GB內(nèi)存CPU。

模型利用Python實(shí)現(xiàn),并通過(guò)Adam優(yōu)化器[26]訓(xùn)練。模型訓(xùn)練過(guò)程中使用PyTorch[27]中的ReduceLROnPlateau策略自動(dòng)調(diào)整學(xué)習(xí)率,以驗(yàn)證集上的損失為參考,若連續(xù)5輪損失不下降,則降低學(xué)習(xí)率,直至降低到最小學(xué)習(xí)率。設(shè)置節(jié)點(diǎn)狀態(tài)向量維度為128,256,512訓(xùn)練模型,迭代次數(shù)K設(shè)置為1,2,3次。模型在訓(xùn)練集上每完成一輪訓(xùn)練將會(huì)在驗(yàn)證集上完成一次評(píng)估,記錄驗(yàn)證集上的損失并保存每輪訓(xùn)練參數(shù)。訓(xùn)練100個(gè)輪次后,驗(yàn)證集上的損失不再下降,選擇100輪中驗(yàn)證集上損失最小的輪次,調(diào)取該輪次對(duì)應(yīng)的參數(shù)在測(cè)試集上進(jìn)行評(píng)估。表 2列出了實(shí)驗(yàn)中所有的參數(shù)設(shè)置。實(shí)驗(yàn)結(jié)果表明,模型在節(jié)點(diǎn)狀態(tài)向量維度為512,迭代訓(xùn)練1次時(shí)效果最佳。

4.3 評(píng)價(jià)指標(biāo)

本文選擇的實(shí)驗(yàn)評(píng)價(jià)指標(biāo)為準(zhǔn)確率(Accuracy)、召回率(Recall)、精確度(Precision)和F1,其計(jì)算方式分別如式(18)～式(21)所示：

(18)

(19)

(20)

(21)

其中,Total表示所有樣本的數(shù)量,TP表示正樣本中分類(lèi)正確的數(shù)量,TN表示負(fù)樣本中分類(lèi)正確的數(shù)量,FP表示正樣本中分類(lèi)錯(cuò)誤的數(shù)量,FN表示負(fù)樣本中分類(lèi)錯(cuò)誤的數(shù)量。

4.4 實(shí)驗(yàn)結(jié)果分析

本文將TL-GNN與主流的圖神經(jīng)網(wǎng)絡(luò)以及同樣旨在編碼一階邏輯公式子節(jié)點(diǎn)順序的圖神經(jīng)網(wǎng)絡(luò)進(jìn)行比較,包括圖卷積神經(jīng)網(wǎng)絡(luò)GCN(Graph Convolutional Network)[28]、簡(jiǎn)化圖卷積神經(jīng)網(wǎng)絡(luò)SGC(Simplifying Graph Convolutional network)[29]、切比雪夫Chebyshev[30]譜圖卷積神經(jīng)網(wǎng)絡(luò)、圖抽樣聚合神經(jīng)網(wǎng)絡(luò)GraphSAGE(Graph SAmple and aggreGatE)[31]、圖注意力神經(jīng)網(wǎng)絡(luò)GAT(Graph ATtention network)[32]和EW-GNN。表3展示了對(duì)比實(shí)驗(yàn)結(jié)果,TL-GNN代表了模型在節(jié)點(diǎn)狀態(tài)向量維度為512,迭代訓(xùn)練1次時(shí)的結(jié)果。

Table 3 Comparison of experimental results

實(shí)驗(yàn)對(duì)比結(jié)果表明,TL-GNN在前提選擇任務(wù)中的表現(xiàn)明顯優(yōu)于其他主流圖神經(jīng)網(wǎng)絡(luò)模型。同時(shí),與同樣旨在編碼一階邏輯公式子節(jié)點(diǎn)順序的EW-GNN相比,TL-GNN高出約1%的分類(lèi)準(zhǔn)確率。在忽略略高的計(jì)算復(fù)雜度的情況下,這不僅說(shuō)明了一階邏輯公式的子節(jié)點(diǎn)順序信息對(duì)前提選擇任務(wù)是重要的,也說(shuō)明了TL-GNN相較于其他圖神經(jīng)網(wǎng)絡(luò)模型具有更強(qiáng)的表征一階邏輯公式的能力。

5 結(jié)束語(yǔ)

本文將一種面向高階邏輯的可保序的嵌入treelet延伸到一階邏輯公式中。根據(jù)treelet的特性,設(shè)計(jì)并實(shí)現(xiàn)了基于treelet的圖神經(jīng)網(wǎng)絡(luò)模型TL-GNN。與當(dāng)前主流圖神經(jīng)網(wǎng)絡(luò)模型以及同樣旨在編碼一階邏輯公式子節(jié)點(diǎn)順序信息的圖神經(jīng)網(wǎng)絡(luò)模型相比,本文提出的模型明顯在前提選擇任務(wù)中更具有優(yōu)勢(shì)。當(dāng)前模型中僅聚合了鄰居節(jié)點(diǎn)與子節(jié)點(diǎn)順序信息,一階邏輯公式的語(yǔ)義與語(yǔ)法性質(zhì)未被充分考慮。未來(lái)將考慮更多一階邏輯公式的語(yǔ)義與語(yǔ)法信息,提出更加有針對(duì)性的模型。