# Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 48 references that are in the map.
- First posted on arXiv 30 May 2025.

## Builds on (most cited first, 23 of 23)

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [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)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [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)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [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)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [An In-Context Learning Agent for Formal Theorem-Proving](https://mlsanity.com/paper/2310.04353/) (2023)
- [WorldTree: A Corpus of Explanation Graphs for Elementary Science Questions supporting Multi-Hop Inference](https://mlsanity.com/paper/1802.03052/) (2018)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [LLMSTEP: LLM proofstep suggestions in Lean](https://mlsanity.com/paper/2310.18457/) (2023)
- [LeanReasoner: Boosting Complex Logical Reasoning with Lean](https://mlsanity.com/paper/2403.13312/) (2024)
- [Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation](https://mlsanity.com/paper/2502.06563/) (2025)
- [Logic-of-Thought: Injecting Logic into Contexts for Full Reasoning in Large Language Models](https://mlsanity.com/paper/2409.17539/) (2024)
- [Consistent Autoformalization for Constructing Mathematical Libraries](https://mlsanity.com/paper/2410.04194/) (2024)
- [Enhancing Ethical Explanations of Large Language Models through Iterative Symbolic Refinement](https://mlsanity.com/paper/2402.00745/) (2024)
- [LOGIC-LM++: Multi-Step Refinement for Symbolic Formulations](https://mlsanity.com/paper/2407.02514/) (2024)
- [Instantiation-based Formalization of Logical Reasoning Tasks using Language Models and Logical Solvers](https://mlsanity.com/paper/2501.16961/) (2025)
- [Inductive Learning of Logical Theories with LLMs: An Expressivity-Graded Analysis](https://mlsanity.com/paper/2408.16779/) (2024)

## Built on by (most cited first, 8 of 8)

- [Beyond Gold Standards: Epistemic Ensemble of LLM Judges for Formal Mathematical Reasoning](https://mlsanity.com/paper/2506.10903/) (2025)
- [LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision](https://mlsanity.com/paper/2512.18196/) (2025)
- [NL2LOGIC: AST-Guided Translation of Natural Language into First-Order Logic with Large Language Models](https://mlsanity.com/paper/2602.13237/) (2026)
- [FaithformBench: Benchmarking Faithfulness of Mathematical Chain-of-Thought Autoformalisation](https://mlsanity.com/paper/2608.10916/) (2026)
- [LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers](https://mlsanity.com/paper/2609.21492/) (2026)
- [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)
- [Reasoning without Gold Standards: A Proxy-Judge Theory of Autoformalization](https://mlsanity.com/paper/2606.09449/) (2026)

## Abstract (arXiv)

Natural language explanations play a fundamental role in Natural Language Inference (NLI) by revealing how premises logically entail hypotheses. Recent work has shown that the interaction of large language models (LLMs) with theorem provers (TPs) can help verify and improve the validity of NLI explanations. However, TPs require translating natural language into machine-verifiable formal representations, a process that introduces the risk of semantic information loss and unfaithful interpretation, an issue compounded by LLMs' challenges in capturing critical logical structures with sufficient precision. Moreover, LLMs are still limited in their capacity for rigorous and robust proof construction within formal verification frameworks. To mitigate issues related to faithfulness and robustness, this paper investigates strategies to (1) alleviate semantic loss during autoformalisation, (2) efficiently identify and correct syntactic errors in logical representations, (3) explicitly use logical expressions to guide LLMs in generating structured proof sketches, and (4) increase LLMs' capacity of interpreting TP's feedback for iterative refinement. Our empirical results on e-SNLI, QASC and WorldTree using different LLMs demonstrate that the proposed strategies yield significant improvements in autoformalisation (+18.46%, +34.2%, +39.77%) and explanation refinement (+29.5%, +51.5%, +41.25%) over the state-of-the-art model. Moreover, we show that specific interventions on the hybrid LLM-TP architecture can substantially improve efficiency, drastically reducing the number of iterations required for successful verification.