From Prompts to Proofs: When Language Becomes an SMT Theory

Policy is where language stops being poetry and starts becoming liability.

A content moderation policy, a warranty clause, a procurement rule, a safety instruction, a legal test: all of them look like ordinary prose until someone asks the system to apply them consistently. Then the prose turns into a machine with hidden gears. Some gears are logical: this condition and that condition, this exception unless that threshold is met. Other gears are semantic: whether a message is threatening, whether a disclosure is meaningful, whether a clause covers a warranty period. Humans navigate this mixture badly but socially. LLMs navigate it fluently but not always reliably. Solvers navigate it reliably but only after the world has been turned into formal symbols. Which is, inconveniently, not how most business documents arrive.

The paper Neurosymbolic Language Reasoning as Satisfiability Modulo Theory proposes a useful change in perspective: stop treating the LLM as the whole decision-maker, and stop treating the symbolic solver as a backend that only receives a fully formalized problem. Instead, treat language judgment itself as a theory inside an SMT-style solving process.¹

That sounds abstract. It is not. It is the difference between asking an LLM, “Does this post violate the policy?” and building a system that says: “Here are the logical possibilities allowed by the policy; now generate or verify the pieces of text needed to satisfy those possibilities; if a piece fails, block that assignment and try another.” The LLM is no longer the judge, jury, and slightly overconfident intern. It becomes one component in a constraint-solving loop.

The paper’s framework, Logitext, is designed for documents that are only partly formalizable. That phrase matters. Many neurosymbolic systems work by translating a problem into formal logic and then letting a solver execute it. That is elegant when the problem is math, logic puzzles, or program synthesis. It is less elegant when a policy contains phrases such as “immediate threat,” “abusive content,” “best-practice disclosure,” or “the context is enough to suggest risk.” These are not clean Boolean predicates waiting politely to be translated. They are natural-language judgments embedded inside logical structure.

Logitext’s bet is that we should formalize what can be formalized, keep semantic clauses as natural language constraints, and let logical propagation and LLM-based judgment interact repeatedly. The important shift is not that the paper “adds logic to prompting.” That would be too small. The shift is that LLM reasoning is placed inside a satisfiability process.

The real problem is not one hard question, but many interacting small ones

Consider a policy saying that a post contains disruptive behavior if it is addressed at a group, targets a protected group attribute, and matches at least one sub-rule such as bias, violence, or genocide. A further rule says that a post is an immediate threat if it expresses violent or genocidal intention and the context suggests risk to safety or life.

A raw prompt asks the model to read the policy and answer directly. In easy cases, that works. In harder cases, the model must do two different things at once.

First, it must make semantic judgments about the text. Is the message addressed to a group? Does it refer to nationality? Does it imply violence? Is the context enough to suggest real risk?

Second, it must combine those judgments according to the policy’s logic. A single clause may not decide the outcome. One clause may matter only because another clause is true. A wrong interpretation may or may not affect the final decision depending on whether it sits inside an and, an or, or an exception.

The paper calls attention to two reasoning gaps.

The first is a compositional gap: the model can often evaluate individual clauses, but it may fail to combine them correctly. This gap narrows as models improve, but it does not disappear. Larger models are better at keeping the symbolic structure in mind, which is reassuring in the same way that a taller stack of papers is better at stopping a door. Useful, but not a principle.

The second is a combinatorial gap: when the task is not merely classification but constrained generation or coverage generation, the model must explore many valid combinations of clause values. For example, generate a message that violates the policy but does not involve violence or genocide. Or generate examples covering every valid combination of policy criteria. Here, the paper reports a much harsher result: even frontier models can miss more than 99% of satisfying assignments that an SMT solver can enumerate. This is the part business readers should not skip.

Classification asks: “Is this one case valid?”

Coverage asks: “What are all the kinds of valid cases we should test?”

The second question is exactly where compliance, safety, legal, and quality assurance teams live. They do not only need a system to answer one case. They need to know what cases the system has not thought of.

Logitext makes partial logic explicit without pretending language is fully formal

Logitext begins with annotation. A document is marked up so that selected natural-language fragments become named clauses, while formal constraints express how those clauses combine.

In the moderation example, a clause such as “addressed at a group” may be bound to a Boolean variable such as C1. Another clause such as “Message is related to murder, rape, assault, arson, terrorism, vandalism, desecration, or threats” may become C4. Then the document can state a formal relationship such as:

Here, $d$ might mean “disruptive behavior.” The logical structure is explicit. But the meaning of each clause still lives in language. Logitext does not pretend that “threat,” “bias,” or “safety risk” has been perfectly reduced to a formal predicate. It leaves those as what the paper calls natural language text constraints, or NLTCs.

This is the mechanism that makes the paper more interesting than a normal “LLM plus rules” system.

A typical staged neurosymbolic architecture looks like this:

The distinction is subtle but important. In the staged approach, the LLM is responsible for making a correct formal representation up front. After that, the solver can only execute what it was given. If the formalization missed something, the solver will be faithfully wrong. Very efficient. Very tragic.

In Logitext, the solver and the LLM keep talking. The solver proposes Boolean assignments that satisfy the explicit logical structure. The LLM then tries to generate or verify text that satisfies the natural-language constraints under that assignment. If it fails, the assignment is blocked and the solver searches again.

That is why the paper frames LLM-based reasoning as an SMT theory. In classical SMT, a solver coordinates different theories: arithmetic, arrays, strings, bit-vectors, sets, and so on. Logitext adds a theory of natural-language text constraints. The LLM is not outside the solver writing an essay about the answer. It is inside the solving process as the component responsible for semantic feasibility.

The check loop is the article’s center of gravity

The core function in Logitext is check(). Given a Logitext document and a partial assignment, it searches for a full satisfying assignment. Depending on the task, that assignment may include labels, intermediate clause values, or generated text.

This unifies three kinds of work:

The inner mechanism is a propose-verify-refine loop.

First, Z3 proposes a Boolean assignment consistent with the formal constraints and the partial assignment supplied by the user. Second, NLSolver handles unbound string variables. It asks an LLM to propose a text value that should satisfy the relevant natural-language constraints. Third, it verifies each relevant NLTC by asking the LLM whether the proposed text makes the clause true or false. Fourth, if verification fails, the violated clauses are fed back into another proposal attempt. After a fixed number of refinement rounds, failure is returned; the outer solver blocks that Boolean assignment and tries another one.

This matters because it separates two failure modes that are usually entangled in prompting.

A raw LLM answer may be wrong because the model misunderstood a clause, because it combined clauses incorrectly, because it ignored a negation, because it failed to explore alternatives, or because it simply guessed a plausible final answer. Logitext does not magically remove semantic errors. But it gives the system places to catch them. Clause verification, Boolean assignment blocking, and coverage enumeration are all diagnostic surfaces.

For business systems, diagnostic surfaces are not glamorous. They are merely the difference between “the model said no” and “the system failed because clause C7 could not be satisfied under assignment 14.” One of those can be audited. The other is a vibe with a JSON wrapper.

The experiments are really three different evaluations, not one leaderboard

The paper evaluates Logitext on three benchmark families: a new content moderation benchmark with five multi-page policies, five tasks from LegalBench, and five tasks from Super-NaturalInstructions. The tasks span policy, legal, and general instruction-following settings. They are tested across three settings: task execution, text instance generation, and text coverage generation.

These settings should not be collapsed into a single “does Logitext win?” question. They test different claims.

The strongest evidence is not in the normal classification setting. It is in constrained generation and coverage generation.

For text instance generation, the paper reports that Logitext reaches near-saturation success even when using the weaker GPT5-nano base model, while direct prompting with GPT5 degrades, especially on complex content moderation policies. The direct prompt is being asked to solve two jobs at once: select a valid logical configuration and then generate text that realizes it. Logitext delegates the first job to the solver and reserves the LLM for semantic generation and verification. That is the point.

For text coverage generation, the difference is sharper. Under a fixed 3000-second budget, Logitext covers more valid examples, especially with the faster GPT5-nano base model. The paper’s latency breakdown explains why. Candidate generation is much faster when handled by a solver rather than repeated LLM calls. The bottleneck moves to NLSolver calls, especially verification and refinement. In business language: Logitext does not make semantic checking free; it stops wasting expensive semantic calls on search that a solver can do better.

The iteration analysis is also useful. The success rate improves as NLSolver gets more refinement rounds. With caching, the paper reports visible benefits in some settings, especially coverage generation with GPT5, though the effect is limited overall. This is an implementation result, not a second thesis. It says the solve loop can be made more efficient, but the main advantage still comes from separating symbolic search from semantic feasibility.

Task execution is mixed, which makes the paper more credible

The classification results are less tidy. Good. Tidy benchmark stories usually mean someone swept the inconvenient parts into the appendix, where they now live quietly under a table number.

In the original task execution setting using GPT-4o, Logitext performs better on the content moderation and Natural Instructions aggregates, but underperforms on LegalBench. The paper identifies two main reasons.

First, clause-level LLM outputs can be wrong even when a holistic LLM answer happens to be correct. This is an important weakness. Decomposition improves control, but it also creates more local judgment points. If the local judgments are unreliable, the final symbolic composition may faithfully amplify the wrong pieces.

Second, list interpretation can be tricky. A phrase such as “x, y, and z” may be intended as a list of examples, not a required conjunction. If annotation treats examples as conjunctive requirements, Logitext becomes too strict. This is not a solver failure. It is a representation failure, which is less mysterious but still operationally expensive.

The appendix expands the task execution evaluation for LegalBench and Super-NaturalInstructions. The expanded results do not overturn the main story. Logitext wins on seven of ten reported tasks: four of five LegalBench tasks and three of five SNI tasks. But the distribution matters.

The business lesson is not “always decompose.” The lesson is “decompose where the logical structure is worth controlling and the clause meanings are stable enough to verify.”

The paper’s clause-level error analysis is useful here. Some sub-clause judgments are stable across runs: often consistently right, sometimes consistently wrong, rather than randomly unstable. That means errors may be fixable through clause rewriting, better annotation, or targeted validators. It also observes that local errors do not necessarily become global errors. If a wrongly true clause sits inside a larger disjunction where another condition already determines the result, the final decision may survive. This is exactly why the structure of the formula matters. Error propagation is not just about model accuracy; it is about where the error lands in the logic.

The business value is test coverage, auditability, and controllable decomposition

The paper directly shows that Logitext can improve constrained generation and coverage generation, and that it can improve task execution in many but not all evaluated settings. That is the research result.

The business inference is narrower and more useful: Logitext-like systems are most promising where an organization needs to operationalize long-form policy text into repeatable decisions, synthetic test cases, or coverage audits.

Think of four practical use cases.

First, policy QA for moderation and safety. A platform can encode the logical skeleton of a policy while leaving sensitive semantic judgments as NLTCs. The system can then generate examples satisfying particular policy paths, helping policy teams test whether their enforcement logic covers the cases they think it covers.

Second, legal and compliance triage. Many legal rules contain formal-ish structure: thresholds, parties, exceptions, jurisdictional requirements, warranty periods, disclosure conditions. Logitext does not turn legal reasoning into solved arithmetic. But it can help separate “the structure of the rule” from “the semantic judgment needed for this clause,” which is already a serious improvement over dumping the whole document into a prompt and hoping the model feels statutory today.

Third, synthetic data generation for business rules. Coverage generation is valuable when a company needs examples for evaluation, red-teaming, policy simulation, or regression testing. The ability to enumerate satisfying assignments is especially important because humans tend to test obvious cases. Solvers are less imaginative, but more thorough. For test coverage, that is a compliment.

Fourth, audit trails for AI decisions. A Logitext-style system can expose intermediate clause values and failed assignments. This does not guarantee correctness, but it makes failures inspectable. In regulated settings, inspectability is often the first step toward governance. Not the final step. The first step. Let us not get carried away; this is still AI.

The ROI pathway is therefore not “replace compliance analysts.” It is cheaper policy diagnosis, stronger test coverage, and more reliable rule execution in places where current workflows are half spreadsheet, half intuition, and half emergency meeting. Yes, that is three halves. Compliance math has always been special.

Where this approach will break first

The paper is careful enough to show boundaries, and those boundaries matter.

The first boundary is annotation quality. Logitext requires someone to decide which clauses become variables and how the logic connects them. This is not a free lunch. It is structured work. If lists of examples are annotated as required conjunctions, the system will enforce the wrong logic with admirable discipline.

The second boundary is clause-level reliability. A holistic LLM can sometimes answer correctly despite muddy intermediate reasoning. A decomposed system can fail because one clause was misjudged. Logitext gains control by exposing intermediate states, but that also means more intermediate states can be wrong. The practical solution is not to abandon decomposition; it is to identify unstable clauses and rewrite, calibrate, or independently validate them.

The third boundary is latency and cost. The solver can reduce candidate-generation cost, but NLSolver still calls an LLM for proposal and verification. For high-coverage generation, this can be acceptable because coverage is often an offline testing task. For real-time classification at scale, the economics need careful design: caching, smaller base models, clause reuse, and fallback paths become engineering decisions, not footnotes.

The fourth boundary is semantic ambiguity. Some legal or policy terms are deliberately flexible. If the organization itself cannot define a clause consistently, Logitext will not rescue it. It may, however, reveal the inconsistency earlier, which is less glamorous than “AI reasoning” but more useful than another dashboard.

Finally, the paper’s expanded appendix results are incomplete for CMOD at the time reported. LegalBench and SNI expansions are useful robustness evidence for task execution, but they do not fully re-run all experiments across all datasets. The constrained generation story remains the stronger result.

From prompting to solving

The article title says “from prompts to proofs,” but the point is not that Logitext proves natural language truth in some grand philosophical sense. Please do not put that in a vendor deck. The point is more precise: parts of natural-language work can be moved from unstructured generation into constraint satisfaction.

That change matters because many business documents already behave like constraint systems. Policies, contracts, regulations, workflow instructions, and eligibility rules are not just text. They are executable expectations written in prose. LLMs made it easy to throw such prose into a model. They did not make it easy to know whether every valid case was covered, whether a failure came from semantic judgment or logical composition, or whether the system can recover when an assignment is infeasible.

Logitext offers a mechanism for that missing layer. It does not eliminate the LLM’s semantic weakness. It contains it inside a structure where symbolic search, verification, refinement, and audit can do some of the work that prompting alone cannot.

For Cognaptus readers, the deeper lesson is architectural. The next stage of business AI will not be won by making every workflow a longer prompt. It will be won by deciding which parts of a workflow should remain language, which parts should become logic, and where the two must negotiate.

Language will not become fully formal. Business is not that merciful.

But it can become solver-aware. That is already a much better place to start.

Cognaptus: Automate the Present, Incubate the Future.