# Neurosymbolic Language Reasoning as Satisfiability Modulo Theory

arXiv: https://arxiv.org/abs/2602.18095 · HTML: https://mlsanity.com/paper/2602.18095/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 15 of its 26 references that are in the map.
- First posted on arXiv 20 Feb 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 15 of 15)

- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [Tree of Thoughts: Deliberate Problem Solving with Large Language Models](https://mlsanity.com/paper/2305.10601/) (2023)
- [Super-NaturalInstructions: Generalization via Declarative Instructions on 1600+ NLP Tasks](https://mlsanity.com/paper/2204.07705/) (2022)
- [LegalBench: A Collaboratively Built Benchmark for Measuring Legal Reasoning in Large Language Models](https://mlsanity.com/paper/2308.11462/) (2023)
- [Measuring Compositional Generalization: A Comprehensive Method on Realistic Data](https://mlsanity.com/paper/1912.09713/) (2019)
- [COGS: A Compositional Generalization Challenge Based on Semantic Interpretation](https://mlsanity.com/paper/2010.05465/) (2020)
- [Logic-RL: Unleashing LLM Reasoning with Rule-Based Reinforcement Learning](https://mlsanity.com/paper/2502.14768/) (2025)
- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning](https://mlsanity.com/paper/2410.08047/) (2024)
- [Unlocking Reasoning Potential in Large Langauge Models by Scaling Code-form Planning](https://mlsanity.com/paper/2409.12452/) (2024)
- [Chain of Logic: Rule-Based Reasoning with Large Language Models](https://mlsanity.com/paper/2402.10400/) (2024)
- [LLM-ARC: Enhancing LLMs with an Automated Reasoning Critic](https://mlsanity.com/paper/2406.17663/) (2024)
- [Revisiting Compositional Generalization Capability of Large Language Models Considering Instruction Following Ability](https://mlsanity.com/paper/2506.15629/) (2025)

## Abstract (arXiv)

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.