mlsanityData to 7 Oct 2026

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

arXiv 2405.01379 ↗First posted 2 May 2024cs.CLcited by 35

Not on the map. Why?

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.

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

Builds on

33 of 55 references.

References · 33

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2023Llama 2: Open Foundation and Fine-Tuned Chat Modelscited by 12,865
  3. 2023Teaching Large Language Models to Self-Debugcited by 963
  4. 2023CRITIC: Large Language Models Can Self-Correct with Tool-Interactive Critiquingcited by 751
  5. 2018e-SNLI: Natural Language Inference with Natural Language Explanationscited by 468
  6. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 379
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  8. 2022Autoformalization with Large Language Modelscited by 252
  9. 2019QASC: A Dataset for Question Answering via Sentence Compositioncited by 248
  10. 2023Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategiescited by 236
  11. 2023REFINER: Reasoning Feedback on Intermediate Representationscited by 203
  12. 2023Is Self-Repair a Silver Bullet for Code Generation?cited by 191
21 more
  1. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 161
  2. 2021Teach Me to Explain: A Review of Datasets for Explainable Natural Language Processingcited by 126
  3. 2023Faithfulness Tests for Natural Language Explanationscited by 107
  4. 2023RL4F: Generating Natural Language Feedback with Reinforcement Learning for Repairing Model Outputscited by 104
  5. 2020NILE : Natural Language Inference with Faithful Natural Language Explanationscited by 96
  6. 2023Improving Language Models via Plug-and-Play Retrieval Feedbackcited by 87
  7. 2019Make Up Your Mind! Adversarial Generation of Inconsistent Natural Language Explanationscited by 71
  8. 2018WorldTree: A Corpus of Explanation Graphs for Elementary Science Questions supporting Multi-Hop Inferencecited by 60
  9. 2022A Comparative Study of Faithfulness Metrics for Model Interpretability Methodscited by 38
  10. 2022Natural Language Deduction through Search over Statement Compositionscited by 35
  11. 2021Back to Square One: Artifact Detection, Training and Commonsense Disentanglement in the Winograd Schemacited by 32
  12. 2024LeanReasoner: Boosting Complex Logical Reasoning with Leancited by 28
  13. 2023Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofscited by 27
  14. 2022Entailment Tree Explanations via Iterative Retrieval-Generation Reasonercited by 26
  15. 2021Hybrid Autoregressive Inference for Scalable Multi-hop Explanation Regenerationcited by 17
  16. 2022NELLIE: A Neuro-Symbolic Inference Engine for Grounded, Compositional, and Explainable Reasoningcited by 16
  17. 2024Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinementcited by 16
  18. 2021Toward Annotator Group Bias in Crowdsourcingcited by 14
  19. 2021Do Natural Language Explanations Represent Valid Logical Arguments? Verifying Entailment in Explainable NLI Gold Standardscited by 12
  20. 2023Abductive Commonsense Reasoning Exploiting Mutually Exclusive Explanationscited by 11
  21. 2024A Logical Pattern Memory Pre-trained Model for Entailment Tree Generationcited by 3

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 4; 2025: 19; 2026: 12.

35 papers.

Sort:

By area:

  1. 2025From Automation to Autonomy: A Survey on Large Language Models in Scientific Discoverycited by 86
  2. 2025From AI for Science to Agentic Science: A Survey on Autonomous Scientific Discoverycited by 74
  3. 2024Consistent Autoformalization for Constructing Mathematical Librariescited by 20
  4. 2025Autoformalization in the Wild: Assessing LLMs on Real-World Mathematical Definitionscited by 20
  5. 2025A Comprehensive Survey on Self-Interpretable Neural Networkscited by 18
  6. 2025Mitigating Content Effects on Reasoning in Language Models through Fine-Grained Activation Steeringcited by 18
  7. 2025Improving Chain-of-Thought Reasoning via Quasi-Symbolic Abstractionscited by 17
  8. 2024CoMAT: Chain of Mathematically Annotated Thought Improves Mathematical Reasoningcited by 16
  9. 2025Theorem Prover as a Judge for Synthetic Data Generationcited by 13
  10. 2025Towards Reliable Code-as-Policies: A Neuro-Symbolic Framework for Embodied Task Planningcited by 10
  11. 2025VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checkscited by 10
  12. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
23 more
  1. 2025Towards a Common Framework for Autoformalizationcited by 7
  2. 2025Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoningcited by 6
  3. 2025MASA: LLM-Driven Multi-Agent Systems for Autoformalizationcited by 6
  4. 2025LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervisioncited by 6
  5. 2024Eliciting Critical Reasoning in Retrieval-Augmented Language Models via Contrastive Explanationscited by 5
  6. 2026FormalScience: Scalable Human-in-the-Loop Autoformalisation of Science with Agentic Code Generation in Leancited by 4
  7. 2025Integrating Expert Knowledge into Logical Programs via LLMscited by 3
  8. 2026NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Modelscited by 3
  9. 2025Formalising Software Requirements using Large Language Modelscited by 2
  10. 2026SEF-CLGC at SemEval-2026 Task 11: Logical Notation Impact on Language Model Performancecited by 1
  11. 2024AUEB-Archimedes at RIRAG-2025: Is obligation concatenation really all you need?cited by 0
  12. 2025VizTrust: A Visual Analytics Tool for Capturing User Trust Dynamics in Human-AI Communicationcited by 0
  13. 2025Working Document -- Formalising Software Requirements with Large Language Modelscited by 0
  14. 2025Can LLM-Generated Textual Explanations Enhance Model Classification Performance? An Empirical Studycited by 0
  15. 2026Inferring Latent Intentions: Attributional Natural Language Inference in LLM Agentscited by 0
  16. 2026Decompose-and-Formalise: Recursively Verifiable Natural Language Inferencecited by 0
  17. 2026ITLC at SemEval-2026 Task 11: Normalization and Deterministic Parsing for Formal Reasoning in LLMscited by 0
  18. 2026AbstRAG: Learning to Abstract for Retrieval Problemscited by 0
  19. 2026Neurosymbolic Clinical Trial Matching via LLM-Driven Abduction and Logical Verificationcited by 0
  20. 2026HABIB_TAZ at SemEval-2026 Task 11: Disentangling Formal Logic from Content via Synthetic Training and Multi-Objective Optimizationcited by 0
  21. 2026Reference-Free Evaluation of Reasoning in Open-Ended Question Answeringcited by 0
  22. 2026Are you Talking Logic to Me? Assessing Language Models Syllogistic Reasoning Capabilitiescited by 0
  23. 2026LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solverscited by 0