Decompose-and-Formalise: Recursively Verifiable Natural Language Inference

TL;DR

This paper introduces a recursive, decompositional framework for natural language inference that enhances verification accuracy, localizes failures, and reduces costly reprocessing by breaking down complex inputs into atomic steps and refining explanations locally.

Contribution

It proposes a novel decompose-and-formalise approach that decomposes NLI tasks into entailment trees, verifies them bottom-up, and refines explanations locally, improving verification rates and efficiency.

Findings

Achieves up to 48.9% improvement in explanation verification rates.

Reduces refinement iterations and runtime significantly.

Maintains strong NLI accuracy across multiple reasoning tasks.

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 $\theta$-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.