将大模型推理转化为可求解的逻辑理论，提升文本与逻辑混合推理能力。
Neurosymbolic Language Reasoning as Satisfiability Modulo Theory
- 用自然语言约束显式表达文档中的部分逻辑结构
- 结合大模型评估与SMT求解，实现联合文本逻辑推理
- 在内容审核等任务中同时提升准确率与覆盖范围
自然语言理解需要融合文本与逻辑推理，但大语言模型在该方面表现不稳定。现有神经符号系统虽结合了大模型与求解器，但仍局限于数学或程序合成等完全可形式化任务，无法处理仅有部分逻辑结构的自然文档。本文提出Logitext，一种神经符号语言，将文档表示为自然语言文本约束（NLTC），使部分逻辑结构显式化。我们开发了一种算法，将基于大模型的约束评估与满足模理论（SMT）求解相结合，实现文本与逻辑的联合推理。在新提出的内容审核基准、LegalBench和Super-Natural Instructions上的实验表明，Logitext在准确率和覆盖范围上均有提升。这是首次将基于大模型的推理视为SMT理论，将神经符号方法扩展至完全可形式化之外的领域。
原文摘要 · Abstract (English)
Natural language understanding requires interleaving textual and logical reasoning, yet large language models often fail to perform such reasoning reliably. Existing neurosymbolic systems combine LLMs with solvers but remain limited to fully formalizable tasks such as math or program synthesis, leaving natural documents with only partial logical structure unaddressed. We introduce Logitext, a neurosymbolic language that represents documents as natural language text constraints (NLTCs), making partial logical structure explicit. We develop an algorithm that integrates LLM-based constraint evaluation with satisfiability modulo theory (SMT) solving, enabling joint textual-logical reasoning. Experiments on a new content moderation benchmark, together with LegalBench and Super-Natural Instructions, show that Logitext improves both accuracy and coverage. This work is the first that treats LLM-based reasoning as an SMT theory, extending neurosymbolic methods beyond fully formalizable domains.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。