Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Neurosymbolic Language Reasoning as Satisfiability Modulo Theory

Hyunseok Oh, Sam Stern, Youngki Lee, Matthai Philipose

TL;DR

This work develops an algorithm that integrates LLM-based constraint evaluation with satisfiability modulo theory (SMT) solving, enabling joint textual-logical reasoning and is the first that treats LLM-based reasoning as an SMT theory, extending neurosymbolic methods beyond fully formalizable domains.

Abstract

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.

Neurosymbolic Language Reasoning as Satisfiability Modulo Theory

TL;DR

This work develops an algorithm that integrates LLM-based constraint evaluation with satisfiability modulo theory (SMT) solving, enabling joint textual-logical reasoning and is the first that treats LLM-based reasoning as an SMT theory, extending neurosymbolic methods beyond fully formalizable domains.

Abstract

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.
Paper Structure (36 sections, 3 equations, 15 figures, 3 tables, 7 algorithms)

This paper contains 36 sections, 3 equations, 15 figures, 3 tables, 7 algorithms.

Table of Contents

  1. Introduction
  2. Interleaved text/logic reasoning in text understanding
  3. Compositional vs combinatorial reasoning in natural text
  4. Logical reasoning gaps
  5. Logitext: Language, representation and solver
  6. The Logitext language
  7. Natural language text constraints
  8. Solving natural language text constraints
  9. Evaluation
  10. Benchmarks and setup
  11. Results
  12. Related work
  13. Conclusion
  14. Appendix
  15. Definitions of gaps
  16. ...and 21 more sections

Figures (15)

  • Figure 1: Example: A content moderation policy (a) illustrates a fine-grained mix of logical and textual constraints. Combined with (b), it yields a prompt that requires compositional logical reasoning, and with (c-d), combinatorial reasoning.
  • Figure 2: Gaps in logical reasoning (see App. \ref{['sub:gap-defs']}) on content moderation across LLMs.
  • Figure 3: Content moderation policy example implemented as Logitext Document
  • Figure 5: End-to-End performance comparison per task.
  • Figure 6: NLSolver success rate vs num. iterations.
  • ...and 10 more figures

Theorems & Definitions (2)

  • Definition 1: Compositional gap $\Delta_{mp}$ of LLM $m$ on prompt $p$
  • Definition 2: Combinatorial gap $\Delta'_{mp}$ of model LLM $m$ on prompt $p$