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.
Abstract (translated)
自然语言解释在自然语言推理（NLI）中扮演着核心角色，揭示了前提如何逻辑地推导出假设。近期的研究表明，大型语言模型（LLMs）与定理证明器（TPs）的交互可以有助于验证和改进NLI解释的有效性。然而，定理证明器需要将自然语言翻译成机器可验证的形式化表示，这一过程引入了语义信息丢失及不忠实解释的风险，而这种问题因大型语言模型在捕捉关键逻辑结构时精度不足的问题而进一步加剧。此外，LLMs在形式验证框架内的严谨且稳健的证明构造能力仍存在局限性。 为了缓解这些与准确性及稳健性相关的问题，本文探讨了以下策略：（1）减轻自动形式化过程中的语义损失；（2）高效识别和纠正逻辑表示中的语法错误；（3）利用逻辑表达式引导LLMs生成结构化的证明草图；以及（4）增强LLMs理解TP反馈的能力，以实现迭代改进。我们在e-SNLI、QASC和WorldTree数据集上使用不同的大型语言模型进行了实证研究，结果显示提出的策略在自动形式化（+18.46%、+34.20%、+39.77%）和解释细化（+29.50%、+51.50%、+41.25%）方面显著优于当前最先进的模型。此外，我们还展示了针对混合LLM-TP架构的特定干预措施可以大幅提升效率，大幅减少成功验证所需的迭代次数。
URL
https://arxiv.org/abs/2505.24264
