让逻辑形式化可调节,提升大模型推理的可验证性与适应性。
Logic-Parametric Neuro-Symbolic NLI: Controlling Logical Formalisms for Verifiable LLM Reasoning
- 将逻辑形式化作为可调参数,实现神经符号推理的灵活控制。
- 内部逻辑策略比外部编码更高效,且在伦理领域表现更优。
- 适合关注可解释、可验证推理的AI研究者和系统设计者。
大语言模型(LLMs)与定理证明器(TPs)结合可用于可验证的自然语言推理(NLI)。然而现有方法依赖固定逻辑形式化,限制了鲁棒性与适应性。本文提出一种逻辑参数化框架,将底层逻辑视为可控组件。基于LogiKEy方法,我们将经典与非经典形式化嵌入高阶逻辑(HOL),系统比较推理质量、解释精度与证明行为。聚焦规范性推理,对比逻辑外(通过公理编码规范)与逻辑内(规范模式由逻辑结构自生)策略。实验表明,逻辑内策略持续提升性能,生成更高效的混合证明。此外,逻辑效果具有领域依赖性:一阶逻辑利于常识推理,而道义与模态逻辑在伦理领域更优。结果强调,应将逻辑作为神经符号架构中的第一类参数元素,以实现更鲁棒、模块化与适应性的推理。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。