通过LLM-符号定理证明进行自然语言解释的验证与精炼
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving
AI总结：
本文提出神经符号框架Explanation-Refiner，整合LLMs和定理证明器，实现自然语言解释的生成、形式化验证与反馈精炼，用于评估和提升NLI模型的解释质量。
摘要：
自然语言解释是评估基于解释和多步自然语言推理（NLI）模型的代理方法。然而，评估NLI解释的有效性具有挑战性，因为这通常涉及众包合适的数据集，该过程耗时且易产生逻辑错误。为了解决现有局限性，本文通过整合大型语言模型（LLMs）和定理证明器来研究自然语言解释的验证与精炼。具体而言，我们提出了一个神经符号框架，名为Explanation-Refiner，它将定理证明器与LLMs整合，以生成和形式化解释性句子，并为NLI建议潜在的推理策略。反过来，定理证明器被用于提供关于解释逻辑有效性的形式化保证，并生成反馈以供后续改进。我们展示了如何联合使用Explanation-Refiner来评估最先进LLMs的解释性推理、自动形式化和错误纠正机制，以及在不同领域自动提升不同复杂度解释的质量。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
