基于歸結(jié)反演的大語言模型邏輯推斷系統(tǒng)

論文名稱：Towards Generalizable and Faithful Logic Reasoning over Natural Language via Resolution Refutation

論文作者：孫洲浩，丁效*，杜理，蔡碧波，高靖龍，劉挺，秦兵 ?

1 引言

基于自然語言的邏輯推理任務(wù)需要模型理解自然語言聲明（statements）之間的抽象邏輯關(guān)系并推理出假設(shè)的真值（標簽）。這類任務(wù)正在越來越受到關(guān)注，因為它將自然語言與抽象邏輯思維聯(lián)系起來，抽象邏輯思維在解決復(fù)雜問題和認知推理中發(fā)揮著關(guān)鍵作用。然而，這類任務(wù)對于LLM來說仍然較為困難，這是因為LLM存在幻覺問題，其在推理過程中可能會產(chǎn)生不正確的中間推理步驟，從而最終導(dǎo)致錯誤的推理結(jié)果，因此是不可靠的。同時，如果將LLM看作一個推理系統(tǒng)，那么幻覺會影響這個系統(tǒng)的完備性。如果一個推理系統(tǒng)是完備的，那么我們可以通過應(yīng)用推理系統(tǒng)中包含的合法推理規(guī)則來推理出具有確定標簽（True和False）的所有假設(shè)。然而，幻覺會阻止LLM通過運用合法的推理規(guī)則得出結(jié)論，從而導(dǎo)致推理系統(tǒng)不完備。

為了減少幻覺從而提升忠實性，前人提出了分步推理方法，這些分步推理方法是基于前向鏈或后向鏈進行設(shè)計的?；谇跋蜴湹姆椒◤囊阎?guī)則開始，檢查是否存在某一個規(guī)則其所有的前提條件都被給定的事實所滿足，如果存在，則應(yīng)用前向鏈的推理規(guī)則來推導(dǎo)出新的結(jié)論，這個過程一直持續(xù)直到不能得出新的結(jié)論或假設(shè)已經(jīng)被證明?；诤笙蜴湹姆椒◤募僭O(shè)開始以相反的方向進行推理，從而得出一組需要滿足的事實，然后檢查這些事實是否已經(jīng)被已知事實所滿足。通過引入了中間推理步驟，基于LLM的推理系統(tǒng)的忠實性得到了提升。

然而這些基于前向鏈或后向鏈的分步推理方法在復(fù)雜的邏輯推理場景下依然不盡如人意。在某些場景下，這些方法的性能可能會低于單獨使用LLMs，甚至低于隨機猜測（random guess）。這是因為基于前向鏈或后向鏈的分步推理方法是不完備的。這意味著一些具有確定標簽的假設(shè)被模型會被認為是Unknown。因此，它只能適應(yīng)于相對簡單的推理場景。以前向鏈為例，前向鏈是不完備的因為它當且僅當“某個規(guī)則的所有條件都可以被已知事實證明是真的”（條件1）時才能夠推理。然而，在推理過程中也存在一些特殊情況，前向鏈無法推理。對于圖1中的假設(shè)1，前向鏈無法推理出假設(shè)是正確的（True），因為規(guī)則中包含的“kind people”這一條件無法被已知事實證明是真的。因此，我們無法得出任何推論，假設(shè)1將被視為Unknown。類似地，對于后向鏈，假設(shè)1“not kind”沒有出現(xiàn)在規(guī)則的右側(cè)因此也無法進行推理，該假設(shè)也將被視為Unknown。

圖1：基于自然語言的邏輯推理問題樣例

受邏輯符號領(lǐng)域的邏輯推理方法的啟發(fā)，我們引入了一個在一階邏輯下完備的邏輯推理范式歸結(jié)反演（其推理過程不會受到條件1的約束）來提高完備性，并提出一個新的推理框架GFaiR。圖2展示了歸結(jié)反演的推理過程。對于圖1中的問題，通過利用歸結(jié)的推理規(guī)則，GFaiR可以在自然語言水平上進行歸結(jié)，從已知信息中逐步推導(dǎo)出“Everyone is not kind”。然后通過反演，“Bob is kind”出現(xiàn)在了已知信息中，進而我們能夠推導(dǎo)出一個矛盾（Everyone is?not kind 與?Bob is kind兩者互相矛盾），從而證明假設(shè)1是真的。因此，歸結(jié)反演的結(jié)合使LLM能夠處理更復(fù)雜的邏輯推理場景，從而增強了泛化能力。

圖2：圖1問題樣例的歸結(jié)反演推理過程

實驗結(jié)果表明，我們的方法在復(fù)雜的邏輯推理場景下取得了最優(yōu)性能，同時保持了在簡單推理場景下的性能。此外，我們觀察到GFaiR產(chǎn)生的推理過程更加忠實。

2 背景

一階邏輯下的自然語言推理: 給定一個假設(shè)H以及一個包含一系列事實和規(guī)則的自然語言理論，目標是在不利用外部知識和常識知識的條件下僅僅利用給定的自然語言理論來判斷假設(shè)H是正確的（True），錯誤的（False），還是無法確定的（Unknown）。每條事實，規(guī)則和假設(shè)都對應(yīng)唯一的一階邏輯表示。H的標簽是根據(jù)對事實和規(guī)則的一階邏輯表示進行推理得到的。一個簡單的例子如下圖所示：

歸結(jié)反演：在基于邏輯符號的推理場景下，歸結(jié)反演是一種在一階邏輯下完備的推理方法，也就是說，對于任何一個在一階邏輯語義下真值為True或者False的假設(shè)，應(yīng)用歸結(jié)反演的推理方法我們都能夠推理出假設(shè)的真值。假設(shè)F為給定前提集對應(yīng)的一階邏輯公式集合（在基于邏輯符號的推理場景下每一個前提都是一個一階邏輯公式），Q為一個以一階邏輯公式表示的假設(shè)且在假設(shè)F下Q的真值為True，則證明Q為True的過程如下所示：

將Q進行否定得到?Q，并且將其合并到F中得到{F,?Q}

將{F,?Q}中的每一條進行Skolem標準化，從而將其轉(zhuǎn)換為一個子句集

應(yīng)用歸結(jié)原理對子句集進行歸結(jié)，其中每一步都是根據(jù)子句集中的兩條子句歸結(jié)出一個新的子句（中間結(jié)論），這個子句會被合并到子句集中。這個歸結(jié)的過程是迭代式的，直到歸結(jié)出一個空子句時停止并說明這個理論集合中存在矛盾，從而進一步說明Q是正確的。

因此，我們可以首先通過對Q和?Q進行反演從而得到{F,?Q}以及{F,Q}，然后分別對{F,?Q}以及{F,Q}進行歸結(jié)推理并判斷其中是否存在矛盾來確定Q的真值。如果{F,?Q}不存在矛盾而{F,Q}存在矛盾，則Q為False，反之Q為True，如果都不存在矛盾，則Q為Unknown。

3 方法

如圖2所示，GFaiR包括5個模塊：轉(zhuǎn)換器，前選擇器，后選擇器，知識組裝器，驗證器。

圖2：GFaiR框架圖

3.1 轉(zhuǎn)換器

在執(zhí)行推理之前，基于T5的轉(zhuǎn)換器首先會將假設(shè)轉(zhuǎn)換為假設(shè)的否定用于后續(xù)進行反演推理。接下來，轉(zhuǎn)換器會將給定的自然語言理論和假設(shè)（或假設(shè)的否定）轉(zhuǎn)換成Skolem范式形式對應(yīng)的自然語言表示用于后續(xù)執(zhí)行歸結(jié)推理。為了方便起見，我們將經(jīng)過轉(zhuǎn)換器轉(zhuǎn)換后的自然語言理論和假設(shè)（或假設(shè)的否定）所組成的整體稱為理論集合T，其中的每一條都統(tǒng)一稱為理論。

3.2 前選擇器

在每一步推理的過程中，基于XLNET前選擇器首先根據(jù)理論集合T選擇一條理論用于后續(xù)執(zhí)行歸結(jié)推理。

3.3 后選擇器

在前選擇器選擇了用于歸結(jié)推理的一條理論之后，基于XLNET的后選擇器根據(jù)理論集合T以及前選擇器選擇的理論來選擇另一條用于后續(xù)執(zhí)行歸結(jié)推理的理論。我們設(shè)計這個模塊是為了顯式地建模前選擇器選擇的理論與其余理論之間的關(guān)系，并利用這一信息來指導(dǎo)后選擇器的理論選擇過程。

3.4 知識組裝器

基于T5的知識組裝器可以從數(shù)據(jù)中隱式地學習歸結(jié)推理規(guī)則，并在自然語言層面對前選擇器和后選擇器選擇的兩條理論應(yīng)用所學習的歸結(jié)推理規(guī)則來生成新的推論。

3.5 驗證器

由于前人的基于transformers的選擇模塊對于歸結(jié)反演來說不夠準確，可能會導(dǎo)致這兩個選擇器所選擇的理論不相關(guān)，進而導(dǎo)致理論上無法根據(jù)這兩條理論得出一個符合邏輯的推論（一個推論是符合邏輯的當且僅當這個推論可以根據(jù)這兩條理論推理出來）。如果知識組裝器根據(jù)這樣的兩條理論進行歸結(jié)推理，那么其生成的推論一定是不合邏輯的，這會導(dǎo)致歸結(jié)推理的失敗并產(chǎn)生不合邏輯的推論（產(chǎn)生幻覺）。由于在后續(xù)的推理步驟中我們可能會用到這個不合邏輯的推論，因此這可能會最終導(dǎo)致錯誤的推理結(jié)果。為此，我們使用基于合法性對比損失的驗證器來驗證前選擇器和后選擇器選擇的兩個理論，以確保在理論上可以通過對這兩條理論執(zhí)行邏輯推理來得出符合邏輯的推論，從而為歸結(jié)推理提供了保證，并通過減少幻覺來提高模型的忠實性。

3.6 推理過程

在推理時，轉(zhuǎn)換器首先將給定的自然語言理論和假設(shè)（或假設(shè)的否定）轉(zhuǎn)換成兩個理論集合，其中每條理論的表示都是Skolem范式形式對應(yīng)的自然語言表示。其中一個理論集合包括自然語言理論和假設(shè)，另一個包括自然語言理論和假設(shè)的否定。接下來我們對這兩個理論集合應(yīng)用圖2中的推理模型（Reasoning model）來推斷其是否存在矛盾，從而判斷假設(shè)的真值。

對于一個具體的理論集合T，前選擇器首先選擇一條理論，接下來，在驗證器的指導(dǎo)下，后選擇器選擇一個能夠與組成一個合法理論對的理論，如果不存在這樣的理論，則停止并認為T中不存在矛盾，否則，知識組裝器會對這兩條理論進行自然語言層面的歸結(jié)推理并得出一個新的推論，如果這個推論是一個空字符串（對應(yīng)空子句），則停止并認為這個理論集合存在矛盾。反之，新生成的推論會被合并到T中參與接下來的推理過程。

4 實驗

4.1 數(shù)據(jù)集&評測指標

為了驗證GFaiR，我們采用RuleTaker-3ext-sat數(shù)據(jù)集進行訓練，然后在RuleTaker-3ext-sat，Ruletaker-depth-5，以及更加復(fù)雜的Hard RuleTaker數(shù)據(jù)集上進行測試。此外，由于Hard RuleTaker數(shù)據(jù)集中沒有標簽為Unknown的數(shù)據(jù)，我們遵循前人的方法來采樣標簽為Unknown的數(shù)據(jù)并將其添加到Hard RuleTaker數(shù)據(jù)集中以構(gòu)造一個標簽平衡的數(shù)據(jù)集，并將這個新的數(shù)據(jù)集稱為Hard RuleTaker*。此外，為了比較我們的方法在復(fù)雜的邏輯推理場景下的in-domain性能，我們將Hard RuleTaker*數(shù)據(jù)集按照8.5,0.5,1的比例將其拆分為訓練集，驗證集，測試集。拆分后的數(shù)據(jù)集我們將其命名為Hard RuleTaker**。

我們的評價指標包括兩個方面：（1）Entailment accuracy (EA)：衡量模型預(yù)測假設(shè)標簽的準確率。（2）Full accuracy (FA): 衡量模型預(yù)測假設(shè)標簽和推理過程同時正確的準確率

4.2 主實驗

我們將GFaiR與基于預(yù)訓練模型的方法以及基于分步推理的方法IBR, FaiRR, NLProofs進行對比，主實驗結(jié)果如表1所示：可以看出，我們的方法在簡單的推理場景下保持了性能，同時在復(fù)雜的推理場景下性能遠遠超過基于預(yù)訓練模型的方法以及基于分步推理的方法，這說明通過結(jié)合歸結(jié)反演，GFaiR的完備性得到了改善，在復(fù)雜推理情境下的zero-shot泛化能力更強。根據(jù)EA和FA的差值，我們也可以看出GFaiR產(chǎn)生的推理過程是忠實的。雖然NLProofs和FaiRR在Hard RT和Hard RT*數(shù)據(jù)集上EA和FA之間的差值更小，但是它們的EA較低，在這種情況下單純考慮其忠實性是沒有意義的。

表1：主實驗結(jié)果

4.3 推理深度泛化實驗

我們通過將不同模型在推理深度小于等于3的RuleTaker-3ext-sat數(shù)據(jù)集進行訓練，然后在推理深度小于等于5的Ruletaker-depth-5數(shù)據(jù)集上進行測試來評估不同方法在推理深度上的泛化能力，結(jié)果如表2所示：可以看出，當推理深度增加時，GFaiR的性能下降更小，比如當推理深度從3增加到5時，GFaiR的EA值下降了1.6%，而FaiRR和NLProofs則分別下降了14.4%和24.5%，這說明GFaiR對于推理深度的泛化能力更強。

表2：推理深度泛化實驗

4.4 復(fù)雜推理場景下的in-domain實驗

我們通過將不同模型在Hard RuleTaker**數(shù)據(jù)集上進行訓練和測試來評價不同方法在復(fù)雜推理情景下的in-domain性能，實驗結(jié)果如表3所示：可以看出，GFaiR在Hard RuleTaker**數(shù)據(jù)集上實現(xiàn)了最佳性能，這說明通過引入歸結(jié)反演，GFaiR方法在復(fù)雜推理情景下更加有效。

表3：復(fù)雜推理場景下的in-domain性能

5 總結(jié)

在本文中，通過引入歸結(jié)反演和基于合法性對比損失的驗證器，我們提出了一個泛化能力強且忠實的推理方法GFaiR，該方法能夠處理復(fù)雜的邏輯推理場景。實驗結(jié)果還表明，在較為復(fù)雜的Hard RuleTaker和Hard RuleTaker*數(shù)據(jù)集上，GFaiR能夠?qū)崿F(xiàn)更好的性能。

審核編輯：黃飛

?