# Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving

Source: [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](<https://www.sota2.com/research/paper/68fa752f1e209131cea66324>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2025-10-26T03:28:08.430Z

Authors: Xin Quan, Marco Valentino, Louise A. Dennis, Andr\\'e Freitas

Published: 2024-05-02T15:20:01.000Z

## 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.

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

- [Logical Refinement of Natural Language Explanations on e-SNLI](<https://www.sota2.com/research/sota/logical-refinement-of-natural-language-explanations-on-e-snli.md>): Logical Refinement of Natural Language Explanations; E-SNLI; Initial Performance: 31.

- [Logical Refinement of Natural Language Explanations on QASC](<https://www.sota2.com/research/sota/logical-refinement-of-natural-language-explanations-on-qasc.md>): Logical Refinement of Natural Language Explanations; QASC; Initial Score: 4.

- [Logical Refinement of Natural Language Explanations on WorldTree](<https://www.sota2.com/research/sota/logical-refinement-of-natural-language-explanations-on-worldtree.md>): Logical Refinement of Natural Language Explanations; WorldTree; Initial Performance: 3.

- [Explanation Refinement on FOLIO](<https://www.sota2.com/research/sota/explanation-refinement-on-folio.md>): Explanation Refinement; FOLIO; Initial Score: 55.74.

- [Explanation Refinement on ProofWriter](<https://www.sota2.com/research/sota/explanation-refinement-on-proofwriter.md>): Explanation Refinement; ProofWriter; Initial Score: 64.

- [Explanation Refinement on EntailmentBank](<https://www.sota2.com/research/sota/explanation-refinement-on-entailmentbank.md>): Explanation Refinement; EntailmentBank; Initial Score: 16.67.

- [Explanation Refinement on PrOntoQA](<https://www.sota2.com/research/sota/explanation-refinement-on-prontoqa.md>): Explanation Refinement; PrOntoQA; Initial Score: 0.6467.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/2405.01379>)

[PDF](<https://arxiv.org/pdf/2405.01379.pdf>)