Decompose-and-Formalise: Recursively Verifiable Natural Language Inference
作者: Xin Quan, Marco Valentino, Louise A. Dennis, André Freitas
分类: cs.CL
发布日期: 2026-01-27
💡 一句话要点
提出分解与形式化框架，提升自然语言推理中神经符号推理的可验证性和局部修正能力。
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自然语言推理 神经符号推理 可验证性 自动形式化 局部修正 大型语言模型 定理证明器
📋 核心要点
- 现有神经符号方法在自然语言推理中面临自动形式化错误累积和难以定位错误的问题，导致验证困难和修正成本高昂。
- 论文提出分解与形式化框架，将推理分解为可验证的原子步骤，并进行局部诊断引导的修正，避免全局重新生成。
- 实验结果表明，该方法显著提高了自然语言推理的可验证性，减少了修正迭代次数，并保持了较高的推理准确率。
📝 摘要（中文）
本文提出了一种分解与形式化（decompose-and-formalise）框架，旨在提升神经符号流水线中大型语言模型（LLM）与定理证明器（TP）结合的自然语言推理（NLI）可验证性和解释修正能力。该框架将前提-假设对分解为原子步骤的蕴含树，自底向上验证树以隔离特定节点上的失败，并执行局部诊断引导的修正，而非全局重新生成解释。此外，为了提高自动形式化的忠实性，引入了基于事件的逻辑形式中的$θ$-替换，以强制执行一致的论元角色绑定。在五个LLM骨干网络上进行的一系列推理任务中，该方法实现了最高的解释验证率，相比最先进水平提高了26.2%、21.7%、21.6%和48.9%，同时减少了修正迭代次数和运行时间，并保持了强大的NLI准确性。
🔬 方法详解
问题定义：现有神经符号方法在处理自然语言推理任务时，特别是对于长文本和复杂推理链，容易出现自动形式化错误。这些错误会导致定理证明器无法验证推理过程，并且难以定位错误的具体位置。传统的修正方法通常需要全局重新生成解释，计算成本很高。
核心思路：论文的核心思路是将复杂的推理过程分解为一系列更小的、原子级别的蕴含步骤，形成一个蕴含树。通过自底向上地验证这个树，可以更容易地定位到出错的步骤。一旦发现错误，就只对出错的局部进行修正，而不是重新生成整个推理过程。
技术框架：该框架包含以下几个主要阶段：1) 分解（Decompose）：将前提-假设对分解为一系列原子蕴含步骤，构建蕴含树。2) 形式化（Formalise）：将每个原子步骤转化为逻辑形式，以便定理证明器进行验证。3) 验证（Verify）：自底向上地验证蕴含树，使用定理证明器检查每个步骤的有效性。4) 修正（Refine）：如果验证失败，则根据定理证明器的诊断信息，对出错的局部进行修正，例如修改逻辑形式或重新分解步骤。
关键创新：该论文的关键创新在于：1) 分解与局部修正：通过分解推理过程和局部修正策略，显著降低了修正的计算成本，并提高了可验证性。2) $θ$-替换：引入了基于事件的逻辑形式中的$θ$-替换，以强制执行一致的论元角色绑定，从而提高自动形式化的忠实性。这有助于减少由于论元不一致导致的错误。
关键设计：在形式化阶段，论文使用了基于事件的逻辑形式，并引入了$θ$-替换来确保论元角色的一致性。在修正阶段，论文利用定理证明器的诊断信息来指导局部修正，例如修改逻辑形式或重新分解步骤。具体的参数设置和网络结构取决于所使用的LLM骨干网络。
🖼️ 关键图片
📊 实验亮点
实验结果表明，该方法在多个推理任务上显著提高了说明验证率，相比最先进水平提高了26.2%、21.7%、21.6%和48.9%。同时，该方法还减少了修正迭代次数和运行时间，并保持了强大的NLI准确性。这些结果表明，分解与形式化框架是一种有效的提高神经符号推理可验证性和效率的方法。
🎯 应用场景
该研究成果可应用于需要高可信度和可解释性的自然语言推理场景，例如智能问答、文本蕴含识别、法律文本分析和医疗诊断辅助等。通过提高推理过程的可验证性，可以增强人们对AI系统决策的信任，并促进AI在关键领域的应用。
📄 摘要（原文）
Recent work has shown that integrating large language models (LLMs) with theorem provers (TPs) in neuro-symbolic pipelines helps with entailment verification and proof-guided refinement of explanations for natural language inference (NLI). However, scaling such refinement to naturalistic NLI remains difficult: long, syntactically rich inputs and deep multi-step arguments amplify autoformalisation errors, where a single local mismatch can invalidate the proof. Moreover, current methods often handle failures via costly global regeneration due to the difficulty of localising the responsible span or step from prover diagnostics. Aiming to address these problems, we propose a decompose-and-formalise framework that (i) decomposes premise-hypothesis pairs into an entailment tree of atomic steps, (ii) verifies the tree bottom-up to isolate failures to specific nodes, and (iii) performs local diagnostic-guided refinement instead of regenerating the whole explanation. Moreover, to improve faithfulness of autoformalisation, we introduce $θ$-substitution in an event-based logical form to enforce consistent argument-role bindings. Across a range of reasoning tasks using five LLM backbones, our method achieves the highest explanation verification rates, improving over the state-of-the-art by 26.2%, 21.7%, 21.6% and 48.9%, while reducing refinement iterations and runtime and preserving strong NLI accuracy.