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.

翻译：自然语言理解需要交织文本与逻辑推理，然而大型语言模型往往难以可靠地执行此类推理。现有的神经符号系统将LLM与求解器结合，但仍局限于可完全形式化的任务（如数学或程序合成），未能处理仅具有部分逻辑结构的自然文档。我们提出Logitext，一种将文档表示为自然语言文本约束（NLTC）的神经符号语言，从而显式表达部分逻辑结构。我们开发了一种算法，将基于LLM的约束评估与可满足性模理论（SMT）求解相结合，实现了文本与逻辑的联合推理。在新构建的内容审核基准测试，以及LegalBench和Super-Natural Instructions上的实验表明，Logitext在准确率和覆盖率方面均有提升。本工作首次将基于LLM的推理视为一种SMT理论，从而将神经符号方法扩展至完全可形式化领域之外。