Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving

📄 arXiv: 2405.01379v4 📥 PDF

作者: Xin Quan, Marco Valentino, Louise A. Dennis, André Freitas

分类: cs.CL

发布日期: 2024-05-02 (更新: 2024-10-11)

备注: Camera-ready for EMNLP 2024

💡 一句话要点

提出Explanation-Refiner框架，结合LLM与定理证明提升NLI解释的有效性。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 自然语言推理 可解释性AI 大型语言模型 定理证明 神经符号计算

📋 核心要点

  1. 现有NLI解释评估依赖众包，耗时且易出错，缺乏形式化验证。
  2. Explanation-Refiner结合LLM生成解释，TP进行形式化验证和反馈。
  3. 该框架能评估LLM的解释能力，并自动提升解释质量，适用于不同领域。

📝 摘要（中文）

自然语言解释是评估基于解释和多步自然语言推理(NLI)模型的代理。然而，评估NLI解释的有效性具有挑战性，因为它通常涉及众包相关数据集，这是一个耗时且容易出现逻辑错误的过程。为了解决现有局限性，本文研究了通过集成大型语言模型(LLM)和定理证明器(TP)来验证和改进自然语言解释。具体来说，我们提出了一个神经符号框架，名为Explanation-Refiner，它将TP与LLM集成，以生成和形式化解释性句子，并为NLI提出潜在的推理策略。反过来，TP被用来提供关于解释逻辑有效性的形式保证，并为后续改进生成反馈。我们展示了Explanation-Refiner如何被共同用于评估最先进的LLM的解释性推理、自动形式化和纠错机制，以及自动提高不同领域中可变复杂度的解释质量。

🔬 方法详解

问题定义：论文旨在解决自然语言推理（NLI）任务中，现有解释方法依赖人工标注，缺乏形式化验证，容易引入逻辑错误的问题。现有方法难以保证解释的可靠性和有效性，阻碍了NLI模型的可信度提升。

核心思路：论文的核心思路是将大型语言模型（LLM）的生成能力与定理证明器（TP）的形式化验证能力相结合。LLM负责生成自然语言解释和推理策略，TP负责对这些解释进行逻辑验证，并提供反馈以改进解释的质量。通过这种神经符号融合的方式，可以提高NLI解释的可靠性和准确性。

技术框架：Explanation-Refiner框架包含以下主要模块：1) LLM解释生成模块：利用LLM生成NLI任务的自然语言解释和推理步骤。2) 自动形式化模块：将LLM生成的自然语言解释转化为定理证明器可以理解的形式化语言。3) 定理证明模块：使用定理证明器对形式化后的解释进行逻辑验证，判断其是否有效。4) 反馈与改进模块：根据定理证明器的验证结果，向LLM提供反馈，指导LLM改进解释的生成。整个流程是一个迭代的过程，LLM不断生成新的解释，TP不断验证并提供反馈，直到生成满足逻辑要求的解释。

关键创新：该论文的关键创新在于将LLM的自然语言生成能力与定理证明器的形式化验证能力相结合，构建了一个神经符号融合的解释验证框架。这种方法不仅可以自动生成NLI任务的解释，还可以对解释的逻辑有效性进行形式化验证，从而提高解释的可靠性和准确性。这是与现有方法最本质的区别。

关键设计：论文中涉及的关键设计包括：1) 如何将自然语言解释转化为定理证明器可以理解的形式化语言，这需要设计合适的自动形式化方法。2) 如何选择合适的定理证明器，并针对NLI任务进行优化。3) 如何设计有效的反馈机制，将定理证明器的验证结果反馈给LLM，指导LLM改进解释的生成。具体的参数设置、损失函数和网络结构等技术细节在论文中可能没有详细描述，需要进一步查阅论文原文。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

Explanation-Refiner框架能够有效评估LLM的解释性推理能力，并自动提升解释质量。实验结果表明，该框架在不同领域和复杂度的解释任务中均表现出良好的性能，能够生成更可靠、更准确的NLI解释。

🎯 应用场景

该研究成果可应用于提升自然语言推理模型的可解释性和可信度，例如在医疗诊断、金融风控等领域，帮助用户理解模型的决策过程，从而更好地信任和使用AI系统。未来可扩展到其他需要可解释AI的领域，如法律、教育等。

📄 摘要（原文）

Natural language explanations represent a proxy for evaluating explanation-based and multi-step Natural Language Inference (NLI) models. However, assessing the validity of explanations for NLI is challenging as it typically involves the crowd-sourcing of apposite datasets, a process that is time-consuming and prone to logical errors. To address existing limitations, this paper investigates the verification and refinement of natural language explanations through the integration of Large Language Models (LLMs) and Theorem Provers (TPs). Specifically, we present a neuro-symbolic framework, named Explanation-Refiner, that integrates TPs with LLMs to generate and formalise explanatory sentences and suggest potential inference strategies for NLI. In turn, the TP is employed to provide formal guarantees on the logical validity of the explanations and to generate feedback for subsequent improvements. We demonstrate how Explanation-Refiner can be jointly used to evaluate explanatory reasoning, autoformalisation, and error correction mechanisms of state-of-the-art LLMs as well as to automatically enhance the quality of explanations of variable complexity in different domains.