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

Abstract: 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.

## introduction a recent line of research in natural language inference (nli) focuses on developing models capable of generating natural language explanations in support of their predictions @xcite @xcite @xcite . since natural language explanations can be used as a proxy to evaluate the underlying reasoning process of nli models @xcite @xcite , researchers have proposed different methods for assessing their intrinsic quality @xcite @xcite @xcite , including the adoption of language generation metrics for a direct comparison between models' generated explanations and human-annotated explanations. however, this process is subject to different types of limitations. first, the use of language generation metrics requires the crowd-sourcing of explanation corpora to augment existing nli datasets @xcite , a process that is time-consuming and susceptible to errors @xcite @xcite . second, language generation metrics have been shown to fail capturing fine-grained properties that are fundamental for nli such as logical reasoning, faithfulness, and robustness @xcite @xcite . third, human explanations in nli datasets tend to be incomplete and contain logical errors that could heavily bias the evaluation @xcite . in this paper, we investigate the integration of state-of-the-art llm-based explanation generation models for nli with external logical solvers to jointly evaluate explanatory reasoning @xcite @xcite and enhance the quality of crowd-sourced explanations. in particular, we present a neuro-symbolic framework, named explanation-refiner, that integrates a theorem prover (tp) with large language models (llms) to investigate the following research questions: rq1: "can the integration of llms and tps provide a mechanism for automatic verification and refinement of natural language explanations?"; rq2: "can the integration of llms and tps improve the logical validity of humanannotated explanations?"; rq3: "to what extent are state-of-the-art llms capable of explanatory reasoning, autoformalisation, and error correction for nli in different domains?". to answer these questions, explanation-refiner employs llms to generate and formalise explanatory sentences and to suggest potential inference strategies for building non-redundant, complete, and logically valid explanations for nli. in turn, the tp is adopted to verify the validity of the explanations through the construction of deductive proofs and the generation of fine-grained feedback for llms. we instantiate explanation-refiner with state-ofthe-art llms (i.e., @xcite , gpt-3.5 @xcite , llama @xcite , and mistral @xcite ) and the isabelle/hol proof assistant @xcite utilising neo-davidsonian event semantics @xcite ) coupled with @xcite to effectively and systematically translate natural language sentences into logical forms. our empirical analysis, carried out on three nli datasets of variable complexity (i.e., e-snli @xcite , qasc @xcite , and worldtree @xcite ), reveals that external feedback from tps is effective in improving the quality of natural language explanations, leading to an increase in logical validity using gpt-4 from 36% to 84%, 12% to 55%, and 2% to 37% (on e-snli, qasc, and worldtree respectively). at the same time, the results demonstrate that integrating external tps with llms can reduce errors in autoformalisation, with an average reduction of syntax errors of 68.67%, 62.31%, and 55.17%. finally, we found notable differences in performance across llms and nli datasets, with closed-sourced llms (i.e., gpt-4 and gpt-3.5) significantly outperforming open-source models (i.e., mistral and llama) on both explanatory reasoning and autoformalisation, along with a shared tendency of llms to struggle with increasing explanation complexity. to summarise, the main contributions of this paper are: ## explanation verification and refinement explanation-based nli is widely adopted to evaluate the reasoning process of multi-step inference models via the construction of natural language explanations. in this work, we refer to the following formalisation for explanation-based nli: given a premise sentence p i , a hypothesis sentence h i , and an explanation e i consisting of a set of facts {f 1 , f 2 , ..., f n }, the explanation e i is logically valid if and only if the entailment p i ∪e i |= h i holds. this entailment is considered verifiable if {p i , e i , h i } can be translated into a set of logical formulae φ that compose a theory θ. the validity of the theory θ is subsequently determined by a theorem prover, verifying whether θ ⊨ ψ, where ψ represents a logical consequence derived from the logical form of h i . in this paper, we aim to automatically verify the logical validity of an explanation e i . to this end, if θ ⊨ ψ is rejected by the theorem prover, a further refinement stage should be initiated to refine the facts {f 1 , f 2 , ..., f n } based on external feedback, resulting in an updated explanation e ′ i . thus, an explanation is accepted if all the facts are logically consistent, complementary and non-redundant to support the derivation. ## explanation-refiner to verify the logical validity and refine any logical errors in explanatory sentences for nli tasks, we hypothesis: a man is public speaking. ## conclusion in this work, we present a novel neuro-symbolic framework, explanation-refiner, which integrates llms and theorem provers for automatic verification and refinement of natural language explanations through iterative cycles. extensive experiments on textual entailment and multiple-choice qa tasks showed improved logical validity of human-annotated explanations. we investigated the model's performance from simple to complex explanatory/sentence structures and introduced a method to prevent the loss of semantic information in autoformalisation tasks with error correction. in future work, we aspire to enhance the framework's robustness towards complex and unstructured explanations with fewer iterations required to improve the model's efficiency.