Natural language explanations have become a proxy for evaluating explainable 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 augments a TP 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 human-annotated explanations of variable complexity in different domains.

翻译：自然语言解释已成为评估可解释及多步自然语言推理（NLI）模型的重要代理指标。然而，验证NLI解释有效性极具挑战性，因为这一过程通常需要众包构建相关数据集，耗时且易产生逻辑错误。针对现有局限，本文探究通过整合大语言模型（LLM）与定理证明器（TP）实现自然语言解释的验证与精炼。具体而言，我们提出名为Explanation-Refiner的神经符号框架，通过TP与LLM的协同增强，生成并形式化解说性语句，同时为NLI推理策略提供建议。该框架利用TP对解释的逻辑有效性提供形式化保证，并生成改进反馈。我们展示了如何联合运用Explanation-Refiner评估前沿LLM的解释推理、自动形式化及错误修正机制，并自动提升不同领域可变复杂度的人工标注解释质量。