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.

通过将大型语言模型（LLMs）与定理证明器（TPs）相结合，本文研究了自然语言解释的验证和改进，提出了一个名为 Explanation-Refiner 的神经符号框架，用于生成和形式化解释句子，并为自然语言推理（NLI）提供潜在的推理策略。同时，定理证明器用于提供解释逻辑有效性的形式保证，并针对改进提供反馈。展示了如何共同使用 Explanation-Refiner 来评估最先进的 LLMs 的解释推理、自动形式化和错误纠正机制，以及自动提高不同领域中复杂性不同的人工注释解释的质量。