LLM-Guided Quantified SMT Solving over Uninterpreted Functions

TL;DR

AquaForte introduces a novel framework that uses Large Language Models to guide SMT solving over formulas with Uninterpreted Functions, significantly improving efficiency and success rate on complex benchmarks.

Contribution

This work is the first to integrate LLMs into SMT solving for UFs, enhancing instantiation guidance and reducing search space while maintaining soundness and completeness.

Findings

AquaForte solves instances that timeout traditional solvers.

It is particularly effective on satisfiable formulas.

Demonstrates the potential of LLMs in symbolic reasoning tasks.

Abstract

Quantified formulas with Uninterpreted Functions (UFs) over non-linear real arithmetic pose fundamental challenges for Satisfiability Modulo Theories (SMT) solving. Traditional quantifier instantiation methods struggle because they lack semantic understanding of UF constraints, forcing them to search through unbounded solution spaces with limited guidance. We present AquaForte, a framework that leverages Large Language Models to provide semantic guidance for UF instantiation by generating instantiated candidates for function definitions that satisfy the constraints, thereby significantly reducing the search space and complexity for solvers. Our approach preprocesses formulas through constraint separation, uses structured prompts to extract mathematical reasoning from LLMs, and integrates the results with traditional SMT algorithms through adaptive instantiation. AquaForte maintains soundness through systematic validation: LLM-guided instantiations yielding SAT solve the original problem, while UNSAT results generate exclusion clauses for iterative refinement. Completeness is preserved by fallback to traditional solvers augmented with learned constraints. Experimental evaluation on SMT-COMP benchmarks demonstrates that AquaForte solves numerous instances where state-of-the-art solvers like Z3 and CVC5 timeout, with particular effectiveness on satisfiable formulas. Our work shows that LLMs can provide valuable mathematical intuition for symbolic reasoning, establishing a new paradigm for SMT constraint solving.