Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations
作者: Xin Quan, Marco Valentino, Louise A. Dennis, André Freitas
分类: cs.CL, cs.AI
发布日期: 2025-05-30
备注: Camera-ready for ACL 2025
💡 一句话要点
提出基于LLM与定理证明器的NLI解释框架，提升忠实性和鲁棒性
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 自然语言推理 可解释性AI 大型语言模型 定理证明器 自动形式化
📋 核心要点
- 现有NLI解释方法依赖自然语言到形式化语言的转换，易造成语义损失，且LLM在逻辑推理上存在局限。
- 论文提出结合LLM和定理证明器，通过减轻语义损失、纠正语法错误、引导证明生成等策略提升解释的忠实性和鲁棒性。
- 实验表明，该方法在自动形式化和解释改进方面均优于现有方法，并显著提高了验证效率。
📝 摘要（中文）
自然语言解释在自然语言推理（NLI）中起着至关重要的作用，它揭示了前提如何逻辑地蕴含假设。最近的研究表明，大型语言模型（LLM）与定理证明器（TP）的交互可以帮助验证和改进NLI解释的有效性。然而，TP需要将自然语言翻译成机器可验证的形式化表示，这个过程引入了语义信息丢失和不忠实解释的风险，而LLM在以足够的精度捕获关键逻辑结构方面面临挑战，更使得这个问题复杂化。此外，LLM在形式验证框架内进行严谨和鲁棒的证明构建的能力仍然有限。为了缓解与忠实性和鲁棒性相关的问题，本文研究了以下策略：（1）减轻自动形式化过程中的语义损失，（2）有效识别和纠正逻辑表示中的语法错误，（3）显式地使用逻辑表达式来指导LLM生成结构化的证明草图，以及（4）提高LLM解释TP反馈以进行迭代改进的能力。在使用不同LLM对e-SNLI、QASC和WorldTree进行的实证结果表明，所提出的策略在自动形式化（+18.46%，+34.2%，+39.77%）和解释改进（+29.5%，+51.5%，+41.25%）方面，相对于最先进的模型，产生了显著的改进。此外，我们表明，对混合LLM-TP架构的特定干预可以显著提高效率，大幅减少成功验证所需的迭代次数。
🔬 方法详解
问题定义：论文旨在解决自然语言推理（NLI）解释中，由于自然语言到形式化语言转换造成的语义信息损失，以及大型语言模型（LLM）在逻辑推理能力上的不足，导致解释不忠实和鲁棒性差的问题。现有方法在自动形式化和证明构建方面存在局限性，难以保证解释的质量。
核心思路：论文的核心思路是构建一个混合的LLM-定理证明器（TP）架构，利用LLM生成自然语言解释，并将其转换为形式化表示，然后使用TP进行验证。通过迭代优化，提高自动形式化的准确性，并利用TP的反馈指导LLM生成更严谨的证明草图，从而提升解释的忠实性和鲁棒性。
技术框架：整体框架包含以下几个主要模块：1) 自动形式化模块：将自然语言文本转换为机器可验证的逻辑表达式，目标是减少语义损失。2) 语法纠错模块：识别并纠正逻辑表达式中的语法错误，确保TP能够正确解析。3) 证明引导模块：利用逻辑表达式指导LLM生成结构化的证明草图，提高证明的严谨性。4) 迭代优化模块：LLM根据TP的反馈信息，迭代改进解释和证明，直至验证成功。
关键创新：论文的关键创新在于：1) 提出了一系列策略来减轻自动形式化过程中的语义损失，例如使用更精确的转换规则和上下文信息。2) 设计了一种高效的语法纠错方法，能够快速识别和纠正逻辑表达式中的错误。3) 显式地使用逻辑表达式来引导LLM生成结构化的证明草图，提高了证明的质量和效率。4) 提出了一种迭代优化机制，利用TP的反馈信息指导LLM改进解释和证明，实现了闭环优化。
关键设计：论文中涉及的关键设计包括：1) 自动形式化模块中使用的转换规则，需要根据具体的NLI数据集进行调整和优化。2) 语法纠错模块中使用的错误检测和纠正算法，需要考虑逻辑表达式的语法特点。3) 证明引导模块中使用的逻辑表达式编码方式，需要能够有效地传递逻辑信息给LLM。4) 迭代优化模块中使用的反馈机制和优化策略，需要平衡效率和效果。
📊 实验亮点
实验结果表明，所提出的策略在e-SNLI、QASC和WorldTree数据集上，自动形式化准确率分别提升了18.46%、34.2%和39.77%，解释改进效果分别提升了29.5%、51.5%和41.25%，显著优于现有方法。此外，通过对混合LLM-TP架构的干预，验证所需的迭代次数大幅减少，提高了效率。
🎯 应用场景
该研究成果可应用于自然语言推理、问答系统、智能客服等领域，提升系统的可解释性和可靠性。通过提供更清晰、更准确的推理过程，可以增强用户对AI系统的信任，并促进人机协作。未来，该方法有望应用于更复杂的逻辑推理任务，例如法律文本分析、科学文献理解等。
📄 摘要（原文）
Natural language explanations play a fundamental role in Natural Language Inference (NLI) by revealing how premises logically entail hypotheses. Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. However, TPs require translating natural language into machine-verifiable formal representations, a process that introduces the risk of semantic information loss and unfaithful interpretation, an issue compounded by LLMs' challenges in capturing critical logical structures with sufficient precision. Moreover, LLMs are still limited in their capacity for rigorous and robust proof construction within formal verification frameworks. To mitigate issues related to faithfulness and robustness, this paper investigates strategies to (1) alleviate semantic loss during autoformalisation, (2) efficiently identify and correct syntactic errors in logical representations, (3) explicitly use logical expressions to guide LLMs in generating structured proof sketches, and (4) increase LLMs' capacity of interpreting TP's feedback for iterative refinement. Our empirical results on e-SNLI, QASC and WorldTree using different LLMs demonstrate that the proposed strategies yield significant improvements in autoformalisation (+18.46%, +34.2%, +39.77%) and explanation refinement (+29.5%, +51.5%, +41.25%) over the state-of-the-art model. Moreover, we show that specific interventions on the hybrid LLM-TP architecture can substantially improve efficiency, drastically reducing the number of iterations required for successful verification.