# Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations Source: [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations]() Collection index: [llms.txt]() Data updated: 2026-01-04T04:22:37.350Z Authors: Xin Quan, Marco Valentino, Louise A. Dennis, Andr\\'e Freitas Published: 2025-05-30T06:38:39.000Z ## Abstract 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. ## 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. - [Explanation Refinement on EntailmentBank](): Explanation Refinement; EntailmentBank; Initial Score: 25.33. - [Logical Refinement of Natural Language Explanations on e-SNLI](): Logical Refinement of Natural Language Explanations; E-SNLI; Initial Performance: 41. - [Logical Refinement of Natural Language Explanations on QASC](): Logical Refinement of Natural Language Explanations; QASC; Initial Score: 17. - [Logical Refinement of Natural Language Explanations on WorldTree](): Logical Refinement of Natural Language Explanations; WorldTree; Initial Performance: 9. - [Explanation Refinement on FOLIO](): Explanation Refinement; FOLIO; Initial Score: 71.31. - [Explanation Refinement on ProofWriter](): Explanation Refinement; ProofWriter; Initial Score: 84. - [Explanation Refinement on PrOntoQA](): Explanation Refinement; PrOntoQA; Initial Score: 0.8533. ## Original sources and implementation [Original paper]() [PDF]() [Implementation]()