논리 매개변수형 신경-기호 NLI: 검증 가능한 LLM 추론을 위한 논리 형식 제어

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

대규모 언어 모델(LLM)과 정리 증명기(TP)는 검증 가능한 자연어 추론(NLI)을 위해 효과적으로 결합될 수 있다. 그러나 기존 접근 방식들은 고정된 논리 형식에 의존하며, 이는 견고성과 적응성을 제한하는 요인이 된다. 본 연구에서는 기저 논리를 정적인 배경이 아닌 제어 가능한 구성 요소로 취급하는 신경-기호 NLI를 위한 논리 매개변수형 프레임워크를 제안한다. LogiKEy 방법론을 활용하여 다양한 고전 및 비고전 형식들을 고차 논리(HOL)에 임베딩함으로써 추론 품질, 설명 정제, 증명 동작을 체계적으로 비교할 수 있게 하였다. 우리는 특히 논리의 선택이 중대한 영향을 미치는 규범적 추론에 초점을 맞춘다. 구체적으로, 규범적 요구사항이 공리를 통해 인코딩되는 논리-외부적 접근 방식과, 규범적 패턴이 논리의 내장 구조에서 발현되는 논리-내부적 접근 방식을 비교한다. 광범위한 실험 결과, 논리-내부적 전략이 일관되게 성능을 향상시키고 NLI를 위한 더 효율적인 하이브리드 증명을 생성할 수 있음을 입증하였다. 또한, 논리의 효율성은 도메인에 따라 달라짐을 확인했는데, 1차 논리는 상식 추론에 유리한 반면, 의무 논리와 양상 논리는 윤리적 도메인에서 우수한 성능을 보였다. 우리의 결과는 더 견고하고 모듈화되며 적응 가능한 추론을 위해 신경-기호 아키텍처에서 논리를 일급(first-class) 매개변수 요소로 다루는 것의 가치를 강조한다.

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.