This paper introduces a neuro-symbolic framework called Explanation-Refiner that integrates Large Language Models (LLMs) with Theorem Provers (TPs) to automatically verify and refine natural language explanations for Natural Language Inference (NLI) tasks. The framework generates and formalizes explanatory sentences, suggests inference strategies, and provides formal guarantees on the logical validity of explanations. The TP is used to verify the validity of explanations through deductive proofs and to generate feedback for subsequent improvements. The framework also includes a syntax error refiner that reduces syntax errors in LLM outputs. The paper evaluates the framework on three NLI datasets (e-SNLI, QASC, and WorldTree) and demonstrates that external feedback from TPs significantly improves the quality of natural language explanations, increasing logical validity from 36% to 84%, 12% to 55%, and 2% to 37% on the respective datasets. The results also show that integrating TPs with LLMs reduces errors in autoformalisation, with an average reduction of 68.67%, 62.31%, and 55.17%. The paper also highlights the performance differences across LLMs and NLI datasets, with closed-source LLMs (GPT-4 and GPT-3.5) outperforming open-source models (Mistral and Llama) in explanatory reasoning and autoformalisation. The framework is shown to be effective in refining explanations, reducing syntax errors, and improving the logical validity of explanations. The paper also discusses the limitations of the approach, including the need for further research on the connection between improved logical consistency and AI safety.This paper introduces a neuro-symbolic framework called Explanation-Refiner that integrates Large Language Models (LLMs) with Theorem Provers (TPs) to automatically verify and refine natural language explanations for Natural Language Inference (NLI) tasks. The framework generates and formalizes explanatory sentences, suggests inference strategies, and provides formal guarantees on the logical validity of explanations. The TP is used to verify the validity of explanations through deductive proofs and to generate feedback for subsequent improvements. The framework also includes a syntax error refiner that reduces syntax errors in LLM outputs. The paper evaluates the framework on three NLI datasets (e-SNLI, QASC, and WorldTree) and demonstrates that external feedback from TPs significantly improves the quality of natural language explanations, increasing logical validity from 36% to 84%, 12% to 55%, and 2% to 37% on the respective datasets. The results also show that integrating TPs with LLMs reduces errors in autoformalisation, with an average reduction of 68.67%, 62.31%, and 55.17%. The paper also highlights the performance differences across LLMs and NLI datasets, with closed-source LLMs (GPT-4 and GPT-3.5) outperforming open-source models (Mistral and Llama) in explanatory reasoning and autoformalisation. The framework is shown to be effective in refining explanations, reducing syntax errors, and improving the logical validity of explanations. The paper also discusses the limitations of the approach, including the need for further research on the connection between improved logical consistency and AI safety.