keyword
entailment trees
An entailment tree is a structured, hierarchical representation of multi-step logical deduction in natural language processing that illustrates how a target conclusion or hypothesis is derived from a collection of supporting facts. In this tree structure, leaf nodes contain initial premises or known background facts, intermediate nodes represent derived natural language conclusions produced through multi-premise textual entailment, and the root node represents the ultimate hypothesis or question-answer assertion being justified. Unlike systems that provide simple textual rationales or unstructured explanations, entailment trees make each step of the reasoning chain explicit, enabling the verification, error tracing, and systematic evaluation of complex deductive reasoning in automated question-answering and language models.
2 items
Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving
Xin Quan, Marco Valentino, Louise A. Dennis, André Freitas
Why you should read this
Proposes Explanation-Refiner, a neuro-symbolic framework that combines large language models with formal theorem provers to verify the logical validity of natural language inference explanations and iteratively repair reasoning errors through formal feedback.
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, automatisation, 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.
Added
2026-10-05
Entailer: Answering Questions with Faithful and Truthful Chains of Reasoning
Oyvind Tafjord, Bhavana Dalvi Mishra, Peter Clark
Why you should read this
Proposes a question-answering framework that couples backward-chaining entailment generation with self-query verification to construct multi-step reasoning trees directly reflecting a language model's internal beliefs.
Our goal is for a system to be able to answer questions and justify its answers with a faithful and truthful chain of reasoning. We present Entailer, a system that produces chains of reasoning by decomposing the question into subquestions and then answering each subquestion using a textual entailment model. The model is trained on a new dataset of 10K examples of multistep reasoning, and uses a novel method to generate the training data automatically from a large corpus. Entailer achieves state-of-the-art results on two multistep reasoning datasets, and its reasoning chains are more faithful and truthful than those of a large language model, as measured by human evaluation and a new automatic metric. We also show that Entailer can be used to improve the performance of a large language model by providing it with a faithful derivation of the answer.
Added
2026-10-03