Decompose-and-Formalise: Recursively Verifiable Natural Language Inference

• URL: http://arxiv.org/abs/2601.19605v1
• Date: Tue, 27 Jan 2026 13:43:30 GMT
• Title: Decompose-and-Formalise: Recursively Verifiable Natural Language Inference
• Abstract summary: 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)<n>We propose a decompose-and-formalise framework that decomposes premise-hypothesis pairs into an entailment tree of atomic steps.<n>We also introduce $$-substitution in an event-based logical form to enforce consistent argument-role bindings.
• Score: 34.505373718498014
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• 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.

Related papers

• Efficient Test-Time Optimization for Multi-Agent Proof Autoformalization [20.22828310618122]
  ToMap is a framework that structures proof autoformalization as a Decomposer-Formalizer-Prover pipeline.<n>We show that ToMap improves over the best previous method by 19.0% when evaluated by both syntactic correctness and semantic faithfulness.
  arXiv  Detail & Related papers  (2026-07-13T09:21:15Z)
• VeryTrace: Verifying Reasoning Traces through Compilable Formalism and Structured Verification [3.5959223920188776]
  Multi-step reasoning with Chain-of-Thought (CoT) prompting remains fragile.<n>This paper presents VeryTrace, a zero-shot verification-and-repair framework.
  arXiv  Detail & Related papers  (2026-06-23T04:15:48Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• ReLoop: Structured Modeling and Behavioral Verification for Reliable LLM-Based Optimization [6.572539312871392]
  Large language models (LLMs) can translate natural language into optimization code, but silent failures pose a critical risk.<n>We introduce ReLoop, addressing silent failures from two complementary directions.
  arXiv  Detail & Related papers  (2026-02-17T20:20:33Z)
• GHS-TDA: A Synergistic Reasoning Framework Integrating Global Hypothesis Space with Topological Data Analysis [27.271992201673083]
  Chain-of-Thought (CoT) has been shown to significantly improve the reasoning accuracy of large language models (LLMs)<n>Existing CoT methods suffer from two fundamental limitations.
  arXiv  Detail & Related papers  (2026-02-10T14:00:30Z)
• Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification [49.506412445511934]
  Large Language Models (LLMs) show remarkable capabilities, yet their next-token prediction creates logical inconsistencies and reward hacking.<n>We introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process.<n>We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization.
  arXiv  Detail & Related papers  (2026-01-30T07:01:25Z)
• Beyond Memorization: Testing LLM Reasoning on Unseen Theory of Computation Tasks [8.210112631285666]
  Large language models (LLMs) have demonstrated strong performance on formal language tasks.<n>We introduce a benchmark for deterministic finite automata (DFA) construction from regular languages.<n>We show that models achieve perfect accuracy on factual questions and 84-90% on seen tasks, but accuracy drops sharply on unseen problems.
  arXiv  Detail & Related papers  (2026-01-19T21:00:31Z)
• VIRO: Robust and Efficient Neuro-Symbolic Reasoning with Verification for Referring Expression Comprehension [51.76841625486355]
  Referring Expression (REC) aims to localize the image region corresponding to a natural-language query.<n>Recent neuro-symbolic REC approaches leverage large language models (LLMs) and vision-language models (VLMs) to perform compositional reasoning.<n>We introduce VIRO, a neuro-symbolic framework that embeds lightweight operator-level verifiers within reasoning steps.
  arXiv  Detail & Related papers  (2026-01-19T07:21:19Z)
• ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimization [73.0780809974414]
  We propose a Reflective Autoformalization method that integrates semantic consistency evaluation into the autoformalization process.<n>This enables the model to iteratively generate formal statements, assess its semantic fidelity, and self-correct identified errors.<n>Experiments show that ReForm achieves an average improvement of 22.6 percentage points over the strongest baselines.
  arXiv  Detail & Related papers  (2025-10-28T16:22:54Z)
• Arg-LLaDA: Argument Summarization via Large Language Diffusion Models and Sufficiency-Aware Refinement [27.673022970833163]
  We introduce Arg-LLaDA, a novel large language diffusion framework that iteratively improves summaries.<n>Our method combines a flexible masking controller with a sufficiency-checking module to identify and revise unsupported, redundant, or incomplete spans.<n> Empirical results on two benchmark datasets demonstrate that Arg-LLaDA surpasses state-of-the-art baselines in 7 out of 10 automatic evaluation metrics.
  arXiv  Detail & Related papers  (2025-07-25T09:07:52Z)
• CLATTER: Comprehensive Entailment Reasoning for Hallucination Detection [60.98964268961243]
  We propose that guiding models to perform a systematic and comprehensive reasoning process allows models to execute much finer-grained and accurate entailment decisions.<n>We define a 3-step reasoning process, consisting of (i) claim decomposition, (ii) sub-claim attribution and entailment classification, and (iii) aggregated classification, showing that such guided reasoning indeed yields improved hallucination detection.
  arXiv  Detail & Related papers  (2025-06-05T17:02:52Z)
• Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations [13.485604499678262]
  Natural language explanations play a fundamental role in Natural Language Inference (NLI)<n>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.<n>This paper investigates strategies to alleviate semantic loss during autoformalisation.
  arXiv  Detail & Related papers  (2025-05-30T06:38:39Z)
• Bridging Internal Probability and Self-Consistency for Effective and Efficient LLM Reasoning [53.25336975467293]
  We present the first theoretical error decomposition analysis of methods such as perplexity and self-consistency.<n>Our analysis reveals a fundamental trade-off: perplexity methods suffer from substantial model error due to the absence of a proper consistency function.<n>We propose Reasoning-Pruning Perplexity Consistency (RPC), which integrates perplexity with self-consistency, and Reasoning Pruning, which eliminates low-probability reasoning paths.
  arXiv  Detail & Related papers  (2025-02-01T18:09:49Z)
• Enhancing Systematic Decompositional Natural Language Inference Using Informal Logic [51.967603572656266]
  We introduce a consistent and theoretically grounded approach to annotating decompositional entailment. We find that our new dataset, RDTE, has a substantially higher internal consistency (+9%) than prior decompositional entailment datasets. We also find that training an RDTE-oriented entailment classifier via knowledge distillation and employing it in an entailment tree reasoning engine significantly improves both accuracy and proof quality.
  arXiv  Detail & Related papers  (2024-02-22T18:55:17Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.