# Decompose-and-Formalise: Recursively Verifiable Natural Language Inference

arXiv: https://arxiv.org/abs/2601.19605 · HTML: https://mlsanity.com/paper/2601.19605/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 17 of its 27 references that are in the map.
- First posted on arXiv 27 Jan 2026.

## Builds on (most cited first, 17 of 17)

- [RoBERTa: A Robustly Optimized BERT Pretraining Approach](https://mlsanity.com/paper/1907.11692/) (2019)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Explaining Answers with Entailment Trees](https://mlsanity.com/paper/2104.08661/) (2021)
- [Faithful Logical Reasoning via Symbolic Chain-of-Thought](https://mlsanity.com/paper/2405.18357/) (2024)
- [NLProlog: Reasoning with Weak Unification for Question Answering in Natural Language](https://mlsanity.com/paper/1906.06187/) (2019)
- [Verification and Refinement of Natural Language Explanations through LLM-Symbolic Theorem Proving](https://mlsanity.com/paper/2405.01379/) (2024)
- [LeanReasoner: Boosting Complex Logical Reasoning with Lean](https://mlsanity.com/paper/2403.13312/) (2024)
- [Aristotle: Mastering Logical Reasoning with A Logic-Complete Decompose-Search-Resolve Framework](https://mlsanity.com/paper/2412.16953/) (2024)
- [Do Natural Language Explanations Represent Valid Logical Arguments? Verifying Entailment in Explainable NLI Gold Standards](https://mlsanity.com/paper/2105.01974/) (2021)
- [NLI under the Microscope: What Atomic Hypothesis Decomposition Reveals](https://mlsanity.com/paper/2502.08080/) (2025)
- [Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations](https://mlsanity.com/paper/2505.24264/) (2025)
- [PEIRCE: Unifying Material and Formal Reasoning via LLM-Driven Neuro-Symbolic Refinement](https://mlsanity.com/paper/2504.04110/) (2025)
- [Adaptive LLM-Symbolic Reasoning via Dynamic Logical Solver Composition](https://mlsanity.com/paper/2510.06774/) (2025)
- [LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision](https://mlsanity.com/paper/2512.18196/) (2025)

## Abstract (arXiv)

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.