一階邏輯中基于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。與當前主流圖神經網絡模型以及同樣旨在編碼一階邏輯公式子節點順序信息的圖神經網絡模型相比,本文提出的模型明顯在前提選擇任務中更具有優勢。當前模型中僅聚合了鄰居節點與子節點順序信息,一階邏輯公式的語義與語法性質未被充分考慮。未來將考慮更多一階邏輯公式的語義與語法信息,提出更加有針對性的模型。