Decompose-and-Formalise: Recursively Verifiable Natural Language Inference

TL;DR

This work introduces LLM-TP Tree, a decompose-and-formalise framework for recursively verifiable natural language inference that combines entailment-tree construction, atomic decomposition, and multi-step θ-substitution autoformalisation to produce solver-checkable explanations. By verifying the entailment tree bottom-up and performing localized refinement, the method isolates failures to small sets of nodes, reducing needless regeneration and improving robustness on long, multi-hop inferences. Using Neo-Davidsonian event semantics and Isabelle/HOL, atoms are formalised into axioms with local lemmas, enabling precise, auditable proofs and improved faithfulness of the autoformalised content. Across four datasets and five LLM backbones, LLM-TP Tree achieves the strongest verification/refinement performance, lowers refinement iterations and runtime, and maintains strong NLI accuracy, demonstrating the practicality of verifiable neuro-symbolic NLI and highlighting avenues for further efficiency improvements and broader naturalistic deployment.

Abstract

Recent work has shown that integrating large language models (LLMs) with theorem provers (TPs) in neuro-symbolic pipelines helps with entailment verification and proof-guided refinement of explanations for natural language inference (NLI). However, scaling such refinement to naturalistic NLI remains difficult: long, syntactically rich inputs and deep multi-step arguments amplify autoformalisation errors, where a single local mismatch can invalidate the proof. Moreover, current methods often handle failures via costly global regeneration due to the difficulty of localising the responsible span or step from prover diagnostics. Aiming to address these problems, we propose a decompose-and-formalise framework that (i) decomposes premise-hypothesis pairs into an entailment tree of atomic steps, (ii) verifies the tree bottom-up to isolate failures to specific nodes, and (iii) performs local diagnostic-guided refinement instead of regenerating the whole explanation. Moreover, to improve faithfulness of autoformalisation, we introduce $θ$-substitution in an event-based logical form to enforce consistent argument-role bindings. Across a range of reasoning tasks using five LLM backbones, our method achieves the highest explanation verification rates, improving over the state-of-the-art by 26.2%, 21.7%, 21.6% and 48.9%, while reducing refinement iterations and runtime and preserving strong NLI accuracy.

Figures (9)

• Figure 1: An illustration of the proposed framework for recursively verifiable natural language inference (NLI) via entailment trees, atomic decomposition, and $\theta$-substitution autoformalisation. The entailment tree is initially constructed from the given premises and hypothesis, including intermediate conclusions. Each sentence is then decomposed into atomic propositions and autoformalised into logical forms. By utilising an external theorem prover, we progressively verify and refine each subtree until the final hypothesis node is reached. The reasoning chain is considered logically sound and coherent once the entire entailment tree has been fully verified and refined.
• Figure 2: $\theta$-substitution autoformalisation example.
• Figure 3: Distribution of the autoformlisation errors (syntax, implication, quantifier, variable in Isabelle/HOL Theories.
• Figure 4: Proof depth alignment between gold and actual constructed proof depths across frameworks. The solid curve shows the mean used depth averaged over five LLMs, while the shaded band shows the range across backbones. Top: Trends in refined cases. Bottom: Trends in unrefined cases.
• Figure 5: Comparison on the logical reasoning accuracy tasks.