When Solvers Guess Smarter: Teaching SMT to Think in Functions

Timeouts are where formal verification quietly loses its glamour.

A team writes a specification. A solver receives the formula. Everyone expects the machine to answer a clean question: is this system safe, satisfiable, contradictory, or not? Then the solver thinks. And thinks. And returns nothing useful before the clock runs out.

This is not because SMT solvers are weak. They are among the most important pieces of invisible infrastructure in modern software verification, program analysis, model checking, and automated test generation. The problem is that some formulas force them into a miserable kind of search: quantified constraints over arithmetic and uninterpreted functions. In those formulas, the solver sees a function symbol such as $f(x)$ or $g(x)$, but it does not know whether the function behaves like a distance metric, a cost curve, a physical transformation, a polynomial, a recurrence, or an unhelpful little gremlin. It only knows the formal constraints attached to the symbol.

The paper behind AquaForte, LLM-Guided Quantified SMT Solving over Uninterpreted Functions, asks a useful question: what if a language model could provide the mathematical guess, while the SMT solver remained responsible for checking it?¹

That is the important distinction. AquaForte is not “ChatGPT replaces Z3.” Nobody sensible should want that headline, and fortunately the paper does not require it. The better headline is more interesting: an LLM can act as a semantic hypothesis generator inside a formal validation loop. It proposes concrete interpretations for uninterpreted functions. The solver then validates, rejects, excludes, or falls back.

In business language: the model gets to suggest; the solver gets to decide. Adults remain in the room.

The hard part is not arithmetic; it is not knowing what the function means

SMT solving extends satisfiability checking by reasoning over background theories such as arithmetic, arrays, bit-vectors, and uninterpreted functions. Uninterpreted functions are useful because they let engineers model components abstractly. Instead of defining every internal behavior of a function, a specification can say: this function exists, it takes these arguments, and it satisfies these constraints.

That abstraction is powerful. It is also expensive.

A solver can reason about arithmetic because arithmetic has semantics. It knows what addition, multiplication, equality, and ordering mean. But an uninterpreted function is deliberately opaque. It obeys congruence: if $x=y$, then $f(x)=f(y)$. Beyond that, the solver does not know its shape.

This becomes especially painful when quantifiers enter the formula. A formula may say something like “for all $x$, these function relationships hold,” or “there exists some value satisfying this condition.” Practical solvers then need to instantiate quantified formulas with useful ground terms. Choosing those terms is the art, and sometimes the trap.

Traditional approaches such as E-matching and model-based quantifier instantiation are sophisticated, but they remain largely syntactic. They look for patterns, terms, and candidate models. What they often lack is the mathematical hunch that a human might have: “This function is probably linear,” “these two functions may be equivalent under scaling,” or “this constraint resembles a sum-of-squares structure.”

AquaForte tries to inject that hunch without handing over correctness.

AquaForte’s mechanism: turn opaque symbols into checkable guesses

The paper’s central mechanism is simple enough to explain, though not simple to engineer.

AquaForte takes an SMT formula containing uninterpreted functions. It separates and simplifies the formula, asks an LLM to propose concrete mathematical definitions for the functions, validates those definitions, and then gives the resulting formula back to a traditional SMT solver.

The LLM might look at constraints involving a function $f$ and propose that $f(x)=x^2$, or that a pair of functions are equivalent under a transformation, or that a function is piecewise linear. Those are not accepted as truth. They are treated as candidates.

The workflow looks roughly like this:

This is why the paper is best read mechanism-first. The benchmark numbers are large, but the architecture is the lesson. AquaForte does not ask an LLM to prove the formula. It asks the LLM to compress a search space by suggesting plausible function interpretations.

That is a different kind of AI contribution. It is not replacing the formal method. It is changing the candidate-generation layer around it.

The soundness loop is the product, not a footnote

The likely misconception is obvious: “The LLM solves formal verification problems.”

No. The LLM proposes interpretations. The solver validates them.

This distinction is not academic politeness. It determines whether the idea can be used in real verification workflows.

If the LLM-guided instantiation leads the solver to a satisfiable result, the solution can be checked against the original problem. If an attempted instantiation fails, AquaForte records the failure and generates exclusion clauses so the system does not keep retrying the same bad interpretation. If the LLM path does not produce a useful result within the iteration or time budget, the framework falls back to the traditional solver, enriched by accumulated constraints.

So the LLM is not trusted as an oracle. It is used as a search heuristic with a validation harness.

That design pattern matters beyond SMT. A lot of enterprise AI discussion still treats “AI reasoning” as if the business choice were between full automation and human supervision. AquaForte suggests a more useful middle layer: let the model generate high-value hypotheses in a domain where blind enumeration is expensive, then validate those hypotheses through a deterministic or formal system.

The solver is still the accountant. The LLM is the intern who notices that the receipt looks suspiciously like a hotel bill. Useful, but not authorized to close the books.

The main evidence: AquaForte solves many cases that baseline solvers miss

The evaluation uses 1,481 benchmark instances across three groups: 281 SMT-COMP 2025 instances from UFNIRA and UFLRA, plus two custom 600-instance benchmark sets. One custom set focuses on sum-of-squares verification; the other, the Mathematical Functions Dataset, covers rational function inequalities, piecewise functions, recursive function problems, and function-limit-style algebraic properties.

The paper compares AquaForte combined with Z3 and CVC5 against baseline Z3 and CVC5, using GPT-4.1, Claude-4-Sonnet, and DeepSeek-V3 as LLM backends. The primary timeout is 24 seconds, following a rapid-evaluation setting, with additional 1200-second experiments.

The headline result is strong:

This is main evidence, not an ablation. It supports the claim that LLM-guided instantiation can substantially expand the number of solved instances under the tested conditions.

But the shape of the gains is more important than the total.

The largest improvements appear on satisfiable cases. In the detailed GPT-4.1 breakdown, AF+Z3 increases solved SAT instances on the SMT-COMP subset from 16 to 58, on the Mathematical Functions Dataset from 275 to 429, and on the sum-of-squares set from 12 to 162. AF+CVC5 shows a similar pattern: on the sum-of-squares set, CVC5 alone solves no SAT instances, while AF+CVC5 solves 159.

UNSAT gains are much smaller. On some datasets they barely move. On the Mathematical Functions Dataset, CVC5’s UNSAT count even moves from 27 to 26 under AF+CVC5 with GPT-4.1. That is not a scandal; it is diagnostic.

A satisfying assignment can often be found by guessing the right structure. An unsatisfiability proof requires ruling out all possibilities. LLMs are much better at proposing plausible mathematical forms than at performing exhaustive exclusion. Apparently, even neural networks prefer finding the door to proving the building has no doors.

The ablation-like comparison says the LLM is not just a slower MBQI

The paper also compares AquaForte against several CVC5 strategies: MBQI, counterexample-guided quantifier instantiation, and enumeration over SyGuS grammars. This is best read as a comparison with prior solver strategies, not as a full component ablation of AquaForte itself.

The result is useful because it positions the method against existing ways of improving quantified solving:

The interpretation should be precise. AquaForte outperforms these strategies in this experimental setup, but it does not make them obsolete. The paper itself treats them as complementary. LLM proposals could seed, steer, rank, or prune traditional synthesis and instantiation methods.

That matters for practical adoption. Enterprises do not usually throw away solver infrastructure because a paper shows a better curve. They add a layer if it improves throughput without breaking guarantees. AquaForte looks more like a steering layer than a replacement engine.

The timeout test shows that “just wait longer” is not the answer

The 1200-second timeout experiment is a robustness and efficiency test. It asks whether the baseline solvers merely need more time.

Apparently, not much.

This test supports a specific claim: for these benchmarks, simply giving traditional solvers a much longer timeout does not recover the missed instances. The bottleneck is not only CPU patience. It is search direction.

For AquaForte, the result also says something subtle. A single LLM call tends to either produce a useful instantiation early or fail to do so. Longer solver runtime after that does not add much. More iterations may help, but passive waiting does not.

That is operationally relevant. If a verification pipeline has a timeout problem, the business question is not only “Can we buy more compute?” Sometimes the better question is “Can we change the search proposal mechanism?”

This is where the paper becomes more than an academic performance story.

Iteration helps, but not infinitely

The multi-iteration experiment is best interpreted as a sensitivity test around LLM-guided refinement. It evaluates whether repeated LLM attempts improve solve rates when earlier instantiations fail.

They do.

With a 1200-second timeout, moving from one to ten iterations improves Claude’s AF+Z3 result from 833 to 953 solved instances, and AF+CVC5 from 704 to 804. Averaged across LLMs, Z3-based configurations improve by 15.5% from iteration 1 to 10, while CVC5-based configurations improve by 17.6%.

The paper reports diminishing returns after roughly 5 to 7 iterations. That is exactly what one would expect if the LLM is exploring a finite set of useful semantic interpretations. Early attempts capture obvious structures. Later attempts start paying rent in smaller coins.

For business use, this creates a tunable cost-quality tradeoff:

The paper’s virtual-best result shows complementarity among models, but virtual best is not a deployed product. It is an upper-bound signal: different LLMs solve different cases. A production system would need routing, fallback, caching, or model selection logic to capture part of that benefit without multiplying cost blindly.

The table that matters for managers: what the evidence supports and what it does not

The paper’s results are impressive, but they do not support every conclusion a vendor deck would love to draw from them. The distinction is where the value is.

The most business-relevant result is not “AquaForte is faster.” The paper reports solver execution times in the detailed table excluding LLM inference latency, with GPT-4.1 averaging 7.60 seconds, Claude-4-Sonnet 16.56 seconds, and DeepSeek-V3 20.66 seconds. That means the right metric for a company is not just solver time. It is end-to-end throughput, timeout reduction, cloud/API cost, reproducibility, and integration complexity.

For teams blocked by solver timeouts, this may still be attractive. A few seconds of LLM inference can be cheap if it avoids hours of failed debugging. But for low-latency inner loops, the economics need measurement, not vibes. Vibes have already done enough damage to software engineering.

The business value is fewer blind alleys in verification workflows

AquaForte matters because many expensive technical workflows depend on answering formal questions under time constraints.

In software verification, a timeout can prevent a safety property from being checked. In program analysis, it can stop a tool from classifying a code path. In model checking, it can leave a system state unresolved. In automated test generation, it can prevent useful test cases from being synthesized.

The paper’s mechanism maps to business value through a practical chain:

1. Specifications with quantified uninterpreted functions create hard solver instances.
2. Traditional solvers may timeout because syntactic instantiation explores too much irrelevant space.
3. AquaForte uses an LLM to propose semantically plausible function definitions.
4. The solver validates those proposals formally.
5. More instances are solved within bounded time.
6. Engineering teams get fewer unresolved verification cases, faster diagnosis, and potentially better automated testing coverage.

That last word, “potentially,” is doing real work. The paper demonstrates benchmark performance, not enterprise ROI. The ROI depends on whether a company’s formulas resemble these benchmark families, whether SAT/model-finding cases dominate the bottleneck, whether LLM latency is acceptable, and whether the verification stack can integrate a hypothesis-generation layer cleanly.

Still, the direction is valuable. It suggests that LLMs may be most useful in formal engineering not as replacement reasoners but as semantic search compressors.

Where AquaForte should be used carefully

The boundaries are not decorative; they affect adoption.

First, the strongest gains are on satisfiable instances. If the business workflow mostly needs UNSAT proofs, AquaForte may provide less value. It may still help by excluding failed interpretations or guiding search, but the paper’s evidence is much less dramatic there.

Second, end-to-end speed is not identical to reported solver execution time. The detailed performance table excludes LLM inference latency, and the average LLM call times are material. Any deployment should measure full pipeline latency.

Third, custom benchmarks matter. The paper includes SMT-COMP instances, but it also includes two constructed benchmark sets designed to stress mathematical-function reasoning. That is legitimate and useful, but companies should test on their own formula distributions before assuming similar gains.

Fourth, reproducibility and determinism require attention. The paper uses low-temperature LLM settings, structured prompts, parsing, type-checking, and validation. A casual “ask the model for a function” implementation would not be AquaForte. It would be a bug generator wearing a lab coat.

Finally, fallback is not optional. The system’s credibility comes from keeping the traditional solver in control. Remove that and the whole idea becomes another example of neural confidence wandering into a formal system and touching things it should not touch.

The larger lesson: LLMs are useful when they guess into a checker

The interesting pattern here is bigger than quantified SMT.

AquaForte belongs to a class of systems where LLMs generate candidates and formal tools verify them. Code agents can propose patches and tests can validate them. Planning agents can propose workflows and rule engines can check constraints. Data agents can propose transformations and schema validators can reject invalid outputs. In all these cases, the LLM is useful not because it is always correct, but because it can propose candidates that would be expensive to enumerate blindly.

For Cognaptus readers, the lesson is not “use LLMs for formal verification.” That is too narrow. The better lesson is architectural:

Put the LLM where semantic guessing is valuable, and put the checker where correctness matters.

AquaForte is a clean example because formal verification makes the boundary visible. The LLM does not get to declare victory. It gets to make a mathematically informed guess. The solver then does the unpleasant, necessary work of checking.

That is not as glamorous as replacing a solver. It is also much more useful.

The future of AI in serious engineering may not be machines that reason perfectly from first principles. It may be systems that guess smarter, fail safely, and hand every claim to something stricter than themselves.

AquaForte shows one version of that future: not SMT without solvers, but solvers with better instincts.

Cognaptus: Automate the Present, Incubate the Future.