逻辑参数化神经符号自然语言推理：为可验证的LLM推理控制逻辑形式体系

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