This paper addresses the challenge of verifying and refining natural language explanations for Natural Language Inference (NLI) models by integrating Large Language Models (LLMs) with Theorem Provers (TPs). The authors propose a neuro-symbolic framework called *Explanation-Refiner*, which uses LLMs to generate and formalize explanatory sentences and suggest inference strategies, while the TP provides formal guarantees on the logical validity of these explanations and generates feedback for improvement. The framework is evaluated on three NLI datasets (e-SNLI, QASC, and WorldTree) using state-of-the-art LLMs (GPT-4, GPT-3.5, Llama, and Mistral) and the Isabelle/HOL proof assistant. The results show that the integration of LLMs and TPs significantly improves the logical validity of explanations, reducing syntax errors by up to 68.67%, 62.31%, and 55.17% across the datasets. GPT-4 outperforms other models, improving validity by 48%, 43%, and 35% respectively. The study also highlights the impact of explanation complexity, with models performing better on simpler tasks like e-SNLI compared to more complex tasks like WorldTree. Additionally, the paper includes a human evaluation of refined explanations, confirming their factual correctness and avoiding triviality. The work contributes to the field by providing a novel method for enhancing the quality and reliability of natural language explanations in NLI tasks.This paper addresses the challenge of verifying and refining natural language explanations for Natural Language Inference (NLI) models by integrating Large Language Models (LLMs) with Theorem Provers (TPs). The authors propose a neuro-symbolic framework called *Explanation-Refiner*, which uses LLMs to generate and formalize explanatory sentences and suggest inference strategies, while the TP provides formal guarantees on the logical validity of these explanations and generates feedback for improvement. The framework is evaluated on three NLI datasets (e-SNLI, QASC, and WorldTree) using state-of-the-art LLMs (GPT-4, GPT-3.5, Llama, and Mistral) and the Isabelle/HOL proof assistant. The results show that the integration of LLMs and TPs significantly improves the logical validity of explanations, reducing syntax errors by up to 68.67%, 62.31%, and 55.17% across the datasets. GPT-4 outperforms other models, improving validity by 48%, 43%, and 35% respectively. The study also highlights the impact of explanation complexity, with models performing better on simpler tasks like e-SNLI compared to more complex tasks like WorldTree. Additionally, the paper includes a human evaluation of refined explanations, confirming their factual correctness and avoiding triviality. The work contributes to the field by providing a novel method for enhancing the quality and reliability of natural language explanations in NLI tasks.