最近阅读了一篇题为《Towards Generalizable and Faithful Logic Reasoning over Natural Language via Resolution Refutation》的研究论文，作者包括孙洲浩、丁效*、杜理、蔡碧波、高靖龙、刘挺、秦兵。文章的核心观点十分明确：大型语言模型在自然语言逻辑推理中容易产生“想当然”的错误，即出现幻觉，导致推理过程缺乏可靠性。现有的分步推理方法（如前向链和后向链）虽然在一定程度上缓解了这一问题，但在复杂场景下仍然力不从心，甚至不如直接让大模型随机猜测。为此，研究团队提出了一套全新的框架——GFaiR，其核心思路是将逻辑学中的“归结反演”方法迁移至自然语言层面，使推理既具备完备性，又保持忠实性。下面我们进行详细解读。

1 引言

基于自然语言的逻辑推理任务要求模型理解声明之间的抽象逻辑关系，并判断某个假设的真假。这类任务之所以受到广泛关注，是因为它将自然语言处理与抽象逻辑思维相结合——而后者在解决复杂问题时至关重要。然而，大型语言模型在这类任务上表现欠佳，主要问题在于幻觉：推理过程中可能生成错误的中间步骤，导致最终结论不可靠。更严重的是，如果我们将大模型视为一个推理系统，幻觉会破坏系统的完备性。完备的推理系统意味着任何具有确定真值的假设都能被证明；而幻觉使得系统无法通过合法规则得出结论，从而破坏了完备性。

为了减少幻觉并提升忠实性，前人提出了分步推理方法，大致分为两类：前向链和后向链。前向链从已知规则出发，检查是否存在规则的所有前提都被事实满足，满足则推出新结论，直到无法推出新内容或假设被证明。后向链则相反，从假设出发逆向推理，得出需要满足的事实集，再检查这些事实是否已经存在。通过引入中间推理步骤，LLM推理的忠实性确实有所改善。

然而，问题在于这些方法在复杂逻辑推理场景下依然表现不佳。在某些情况下，它们的性能甚至低于直接使用LLM或随机猜测。原因很简单：前向链和后向链不完备。它们仅适用于相对简单的推理场景，许多有确定标签的假设会被判定为Unknown。以前向链为例，它只有在“某个规则的所有条件都能被已知事实证明为真”时才能进行推理。但实际推理中经常出现特殊情况，比如图1中的假设1——规则里包含“kind people”这一条件，而已知事实无法证明它成立，因此前向链推不出任何结论，假设1就被当作Unknown了。后向链同样如此，假设1“not kind”并未出现在规则右侧，同样无法推理，结果仍是Unknown。

图1：基于自然语言的逻辑推理问题样例

受符号逻辑领域的启发，论文引入了一种在一阶逻辑下完备的推理范式——归结反演，其推理过程不受上述条件约束，并在此基础上提出了GFaiR框架。图2展示了归结反演的推理过程。针对图1的问题，通过运用归结规则，GFaiR可以在自然语言层面逐步推导出“Everyone is not kind”，然后反演发现“Bob is kind”与已知信息矛盾，从而证明假设1为真。这样一来，归结反演让LLM能够处理更复杂的逻辑推理场景，泛化能力自然得到提升。

图2：图1问题样例的归结反演推理过程

实验结果表明，GFaiR在复杂推理场景下取得了最优性能，同时保持了在简单场景下的表现。此外，它的推理过程更加忠实——中间步骤经得起推敲。

2 背景

一阶逻辑下的自然语言推理：给定一个假设H和一个包含事实与规则的自然语言理论，目标是在不借助外部知识的前提下，仅凭该理论判断H是True、False还是Unknown。每条事实、规则和假设都对应唯一的一阶逻辑表示，H的标签也是根据这些一阶逻辑表示推理得出的。一个简单的例子如下图所示：

归结反演：在符号逻辑推理中，归结反演是一阶逻辑下的完备推理方法——任何真值为True或False的假设，都能通过它推导出来。具体过程：设F为前提集对应的一阶逻辑公式集，Q为假设的一阶逻辑公式，且Q在F下为True。要证明Q为True，先对Q取反得到¬Q，并入F得到{F, ¬Q}；然后对其中每条公式进行Skolem标准化，转换为子句集；接着应用归结原理，从子句集中不断归结出新子句（中间结论），直到出现空子句——说明理论集合存在矛盾，从而证明Q为真。反过来，如果{F, Q}存在矛盾而{F, ¬Q}没有，则Q为False；两者都不矛盾则Q为Unknown。

3 方法

如图2所示，GFaiR包含五个模块：转换器、前选择器、后选择器、知识组装器、验证器。

图2：GFaiR框架图

3.1 转换器

推理开始前，基于T5的转换器首先将假设转换为它的否定形式，用于后续反演。接着，它把给定的自然语言理论和假设（或假设的否定）转换成Skolem范式对应的自然语言表示，方便后续执行归结推理。经过转换后，所有内容构成一个理论集合T，其中每条语句统称为“理论”。

3.2 前选择器

每一步推理中，基于XLNET的前选择器先从理论集合T中选择一条理论，作为下一步归结的对象。

3.3 后选择器

前选择器选定一条理论后，基于XLNET的后选择器再根据T以及已选理论，选出另一条用于归结的理论。设计这个模块的目的，是显式地建模已选理论与其余理论之间的关系，并利用这些信息指导选择。

3.4 知识组装器

基于T5的知识组装器能从数据中隐式地学习归结推理规则，并在自然语言层面对前、后选择器选出的两条理论应用这些规则，生成新的推论。

3.5 验证器

前人基于Transformer的选择模块对于归结反演来说不够精确，可能导致选出的两条理论不相关，理论上无法推出符合逻辑的结论。如果知识组装器对这样的两条理论进行归结，生成的推论一定不合逻辑——这就会产生幻觉。更麻烦的是，后续推理步骤可能用到这个错误的推论，最终导致整个推理偏离正确方向。为此，论文引入基于合法性对比损失的验证器，专门验证前、后选择器选出的两条理论能否在逻辑上得出合理的推论，从而为归结推理提供保障，从源头减少幻觉、提高忠实性。

3.6 推理过程

正式推理时，转换器先把自然语言理论和假设（或假设的否定）转换成两个理论集合，每个集合中的理论都是Skolem范式对应的自然语言表示。一个集合包含理论+假设，另一个包含理论+假设的否定。然后对这两个集合分别应用图2中的推理模型，判断是否存在矛盾，进而决定假设的真值。

对于某个理论集合T，前选择器先选一条理论，然后在验证器的指导下，后选择器寻找能与之组成合法理论对的另一条理论。如果找不到，就认为T中无矛盾，停止；如果找到，知识组装器就对这两条理论进行自然语言层面的归结，得出新推论。若这个推论为空字符串（对应空子句），则说明存在矛盾，停止；否则将新推论并入T，继续下一轮推理。

4 实验

4.1 数据集与评测指标

为了验证GFaiR，论文使用RuleTaker-3ext-sat数据集进行训练，然后在RuleTaker-3ext-sat、RuleTaker-depth-5以及更复杂的Hard RuleTaker数据集上测试。由于Hard RuleTaker没有Unknown标签的数据，作者按前人方法采样了Unknown数据，构造出标签平衡的Hard RuleTaker*数据集。另外，为了评估复杂场景下的in-domain性能，又将Hard RuleTaker*按8.5:0.5:1拆分出训练、验证、测试集，称为Hard RuleTaker**。

评测指标有两个：（1）Entailment Accuracy（EA）：模型预测假设标签的准确率；（2）Full Accuracy（FA）：模型预测的假设标签和推理过程同时正确的准确率。

4.2 主实验

将GFaiR与基于预训练模型的方法以及分步推理方法IBR、FaiRR、NLProofs进行对比，结果如表1所示。可以看到，GFaiR在简单场景下保持了原有性能，而在复杂场景下远远超过其他方法。这说明引入归结反演后，GFaiR的完备性大幅提升，zero-shot泛化能力更强。另外，从EA与FA的差值来看，GFaiR的推理过程也更加忠实。虽然NLProofs和FaiRR在Hard RT和Hard RT*数据集上EA与FA的差值更小，但它们的EA本身很低——这种情况下单纯看忠实性没有意义。

表1：主实验结果

4.3 推理深度泛化实验

各模型在推理深度≤3的RuleTaker-3ext-sat上训练，然后在深度≤5的RuleTaker-depth-5上测试，结果如表2所示。当深度增加时，GFaiR的性能下降最小：EA仅下降了1.6%，而FaiRR下降了14.4%，NLProofs更是下降了24.5%。说明GFaiR对推理深度的泛化能力显著更强。

表2：推理深度泛化实验

4.4 复杂推理场景下的in-domain实验

各模型在Hard RuleTaker**上训练并测试，结果如表3所示。GFaiR实现了最佳性能，证明在复杂推理场景中，引入归结反演能带来实实在在的效果提升。

表3：复杂推理场景下的in-domain性能

5 总结

通过引入归结反演和基于合法性对比损失的验证器，GFaiR成为一个泛化能力强且忠实的推理方法，能够有效处理复杂的逻辑推理场景。实验数据表明，在Hard RuleTaker和Hard RuleTaker*这类复杂数据集上，GFaiR实现了更好的性能，为后续研究提供了一个扎实的方向。