基于可满足性模理论的神经符号语言推理

自然语言理解需要交织文本与逻辑推理，但大语言模型在该任务上表现不稳定。现有神经符号系统虽结合了LLMs与求解器，但仅适用于完全形式化的任务，如数学或程序合成，而无法处理具有部分逻辑结构的自然文档。本文提出Logitext，一种神经符号语言，将文档表示为自然语言文本约束（NLTCs），使部分逻辑结构显式化。开发了一种算法，将基于LLM的约束评估与可满足性模理论（SMT）求解相结合，实现文本与逻辑的联合推理。实验表明，在新的内容审核基准、LegalBench和Super-Natural Instructions上的测试中，Logitext在准确性和覆盖率方面均有提升。这是首次将基于LLM的推理视为SMT理论，扩展了神经符号方法的应用范围，超越了完全形式化领域。