Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning

TL;DR

The paper tackles the problem of verifiable natural language inference (NLI) by removing the assumption of a fixed logical substrate and introducing a logic-parametric neuro-symbolic framework that embeds multiple logics into higher-order logic via LogiKEy. It formalizes NLI explanations as Θ_{ L} ⊢ ψ_{ L} and evaluates a four-stage pipeline (autoformalization, syntax check, theorem proving, explanation refinement) across four logics (FOL, KD, DDLE, DDL_CJ) using the BENR dataset. Empirical results show logic-internal approaches (notably KD and DDL_CJ) produce higher explanation success, greater refinement efficiency, and domain-dependent strengths (FOL for commonsense; modal/deontic logics for ethical domains) while highlighting trade-offs in syntactic robustness and computational cost. The findings argue for logic-adaptive reasoning in neuro-symbolic systems to achieve more robust, modular, and explainable AI, with practical implications for domains requiring normative and ethical verification; the framework provides a path toward dynamic logic selection guided by task needs. By mapping natural-language components to logic-specific theories in HOL, the work lays the groundwork for configurable, verifiable reasoning pipelines that can switch logics to suit domain demands and verification goals.

Abstract

Large language models (LLMs) and theorem provers (TPs) can be effectively combined for verifiable natural language inference (NLI). However, existing approaches rely on a fixed logical formalism, a feature that limits robustness and adaptability. We propose a logic-parametric framework for neuro-symbolic NLI that treats the underlying logic not as a static background, but as a controllable component. Using the LogiKEy methodology, we embed a range of classical and non-classical formalisms into higher-order logic (HOL), enabling a systematic comparison of inference quality, explanation refinement, and proof behavior. We focus on normative reasoning, where the choice of logic has significant implications. In particular, we compare logic-external approaches, where normative requirements are encoded via axioms, with logic-internal approaches, where normative patterns emerge from the logic's built-in structure. Extensive experiments demonstrate that logic-internal strategies can consistently improve performance and produce more efficient hybrid proofs for NLI. In addition, we show that the effectiveness of a logic is domain-dependent, with first-order logic favouring commonsense reasoning, while deontic and modal logics excel in ethical domains. Our results highlight the value of making logic a first-class, parametric element in neuro-symbolic architectures for more robust, modular, and adaptable reasoning.

Figures (8)

• Figure 1: Illustration of the logic-parametric neuro-symbolic NLI framework with LLMs. The framework generalizes neuro-symbolic architectures via LogiKEy, embedding classical and non-classical logics into higher-order logic (HOL). This enables the integration of LLMs and theorem provers (TPs) using diverse logical formalisms for iterative explanation refinement across tasks and domains.
• Figure 2: Success rates for valid explanation generation.
• Figure 3: Average number of refinement iterations required to reach a valid explanation.
• Figure 4: Explanation refinement performance across logical frameworks and domains for both DeepSeek-V1 and GPT-4o. Solving time is averaged over successful runs only.
• Figure 5: Average solving time (seconds) over successful explanation refinements.

Theorems & Definitions (1)

• Example : Autonomy requires competent choice