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

arXiv: https://arxiv.org/abs/2405.01379 · HTML: https://mlsanity.com/paper/2405.01379/

## Key facts

- Cited by 35 papers in the map (data through 14 Oct 2026).
- Builds on 33 of its 55 references that are in the map.
- First posted on arXiv 2 May 2024.

## Builds on (most cited first, 30 of 33)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Teaching Large Language Models to Self-Debug](https://mlsanity.com/paper/2304.05128/) (2023)
- [CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquing](https://mlsanity.com/paper/2305.11738/) (2023)
- [e-SNLI: Natural Language Inference with Natural Language Explanations](https://mlsanity.com/paper/1812.01193/) (2018)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [QASC: A Dataset for Question Answering via Sentence Composition](https://mlsanity.com/paper/1910.11473/) (2019)
- [Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategies](https://mlsanity.com/paper/2308.03188/) (2023)
- [REFINER: Reasoning Feedback on Intermediate Representations](https://mlsanity.com/paper/2304.01904/) (2023)
- [Is Self-Repair a Silver Bullet for Code Generation?](https://mlsanity.com/paper/2306.09896/) (2023)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Teach Me to Explain: A Review of Datasets for Explainable Natural Language Processing](https://mlsanity.com/paper/2102.12060/) (2021)
- [Faithfulness Tests for Natural Language Explanations](https://mlsanity.com/paper/2305.18029/) (2023)
- [RL4F: Generating Natural Language Feedback with Reinforcement Learning for Repairing Model Outputs](https://mlsanity.com/paper/2305.08844/) (2023)
- [NILE : Natural Language Inference with Faithful Natural Language Explanations](https://mlsanity.com/paper/2005.12116/) (2020)
- [Improving Language Models via Plug-and-Play Retrieval Feedback](https://mlsanity.com/paper/2305.14002/) (2023)
- [Make Up Your Mind! Adversarial Generation of Inconsistent Natural Language Explanations](https://mlsanity.com/paper/1910.03065/) (2019)
- [WorldTree: A Corpus of Explanation Graphs for Elementary Science Questions supporting Multi-Hop Inference](https://mlsanity.com/paper/1802.03052/) (2018)
- [A Comparative Study of Faithfulness Metrics for Model Interpretability Methods](https://mlsanity.com/paper/2204.05514/) (2022)
- [Natural Language Deduction through Search over Statement Compositions](https://mlsanity.com/paper/2201.06028/) (2022)
- [Back to Square One: Artifact Detection, Training and Commonsense Disentanglement in the Winograd Schema](https://mlsanity.com/paper/2104.08161/) (2021)
- [LeanReasoner: Boosting Complex Logical Reasoning with Lean](https://mlsanity.com/paper/2403.13312/) (2024)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Entailment Tree Explanations via Iterative Retrieval-Generation Reasoner](https://mlsanity.com/paper/2205.09224/) (2022)
- [Hybrid Autoregressive Inference for Scalable Multi-hop Explanation Regeneration](https://mlsanity.com/paper/2107.11879/) (2021)
- [NELLIE: A Neuro-Symbolic Inference Engine for Grounded, Compositional, and Explainable Reasoning](https://mlsanity.com/paper/2209.07662/) (2022)
- [Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement](https://mlsanity.com/paper/2402.00745/) (2024)
- [Toward Annotator Group Bias in Crowdsourcing](https://mlsanity.com/paper/2110.08038/) (2021)

## Built on by (most cited first, 30 of 35)

- [From Automation to Autonomy: A Survey on Large Language Models in Scientific Discovery](https://mlsanity.com/paper/2505.13259/) (2025)
- [From AI for Science to Agentic Science: A Survey on Autonomous Scientific Discovery](https://mlsanity.com/paper/2508.14111/) (2025)
- [Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitions](https://mlsanity.com/paper/2502.12065/) (2025)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [A Comprehensive Survey on Self-Interpretable Neural Networks](https://mlsanity.com/paper/2501.15638/) (2025)
- [Mitigating Content Effects on Reasoning in Language Models through Fine-Grained Activation Steering](https://mlsanity.com/paper/2505.12189/) (2025)
- [Improving Chain-of-Thought Reasoning via Quasi-Symbolic Abstractions](https://mlsanity.com/paper/2502.12616/) (2025)
- [CoMAT: Chain of Mathematically Annotated Thought Improves Mathematical Reasoning](https://mlsanity.com/paper/2410.10336/) (2024)
- [Theorem Prover as a Judge for Synthetic Data Generation](https://mlsanity.com/paper/2502.13137/) (2025)
- [Towards Reliable Code-as-Policies: A Neuro-Symbolic Framework for Embodied Task Planning](https://mlsanity.com/paper/2510.21302/) (2025)
- [VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks](https://mlsanity.com/paper/2511.04662/) (2025)
- [Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks](https://mlsanity.com/paper/2505.20047/) (2025)
- [Towards a Common Framework for Autoformalization](https://mlsanity.com/paper/2509.09810/) (2025)
- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [MASA: LLM-Driven Multi-Agent Systems for Autoformalization](https://mlsanity.com/paper/2510.08988/) (2025)
- [LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision](https://mlsanity.com/paper/2512.18196/) (2025)
- [Eliciting Critical Reasoning in Retrieval-Augmented Language Models via Contrastive Explanations](https://mlsanity.com/paper/2410.22874/) (2024)
- [NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models](https://mlsanity.com/paper/2602.13237/) (2026)
- [FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Lean](https://mlsanity.com/paper/2604.23002/) (2026)
- [Integrating Expert Knowledge into Logical Programs via LLMs](https://mlsanity.com/paper/2502.12275/) (2025)
- [Formalising Software Requirements using Large Language Models](https://mlsanity.com/paper/2506.10704/) (2025)
- [SEF-CLGC at SemEval-2026 Task 11: Logical Notation Impact on Language Model Performance](https://mlsanity.com/paper/2606.09157/) (2026)
- [LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers](https://mlsanity.com/paper/2609.21492/) (2026)
- [AUEB-Archimedes at RIRAG-2025: Is obligation concatenation really all you need?](https://mlsanity.com/paper/2412.11567/) (2024)
- [VizTrust: A Visual Analytics Tool for Capturing User Trust Dynamics in Human-AI Communication](https://mlsanity.com/paper/2503.07279/) (2025)
- [Working Document -- Formalising Software Requirements with Large Language Models](https://mlsanity.com/paper/2506.14627/) (2025)
- [Can LLM-Generated Textual Explanations Enhance Model Classification Performance? An Empirical Study](https://mlsanity.com/paper/2508.09776/) (2025)
- [Inferring Latent Intentions: Attributional Natural Language Inference in LLM Agents](https://mlsanity.com/paper/2601.08742/) (2026)
- [Decompose-and-Formalise: Recursively Verifiable Natural Language Inference](https://mlsanity.com/paper/2601.19605/) (2026)
- [ITLC at SemEval-2026 Task 11: Normalization and Deterministic Parsing for Formal Reasoning in LLMs](https://mlsanity.com/paper/2603.02676/) (2026)

## Abstract (arXiv)

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.