逻辑参数化的神经符号NLI：控制逻辑形式体系以实现可验证的LLM推理

大语言模型（LLM）与定理证明器（TP）可以有效结合，实现可验证的自然语言推断（NLI）。然而，现有方法依赖固定的逻辑形式体系，这一特点限制了鲁棒性和适应性。我们提出一个逻辑参数化的神经符号NLI框架，将底层逻辑不视为静态背景，而是当作可控组件。借助LogiKEy方法，我们将一系列经典与非经典形式体系嵌入高阶逻辑（HOL），从而系统比较推理质量、解释细化和证明行为。我们聚焦于规范推理，逻辑的选择在其中具有重要影响。特别地，我们比较了逻辑外置方法（通过公理编码规范要求）与逻辑内置方法（规范模式从逻辑的内置结构中产生）。大量实验表明，逻辑内置策略能够持续提升性能，并为NLI产生更高效的混合证明。此外，我们表明一种逻辑的有效性依赖于领域：一阶逻辑更利于常识推理，而义务逻辑和模态逻辑在伦理领域表现更佳。我们的结果凸显了在神经符号架构中将逻辑作为一等参数化元素的价值，以实现更鲁棒、更模块化、适应性更强的推理。