Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LLM-Guided Quantified SMT Solving over Uninterpreted Functions

Kunhang Lv, Yuhang Dong, Rui Han, Fuqi Jia, Feifei Ma, Jian Zhang

TL;DR

This work tackles the hardness of solving quantified formulas with uninterpreted functions under non-linear real arithmetic, a problem formalized as $QUFNIRA$. It introduces AquaForte, a hybrid framework that leverages Large Language Models to generate semantically grounded uninterpreted function instantiations and integrates these with traditional SMT solvers through an adaptive, soundness-preserving loop. The authors implement a structured preprocessing-instantiation-postprocessing pipeline, develop LLM-driven trigger synthesis, and couple these with existing techniques in an iterative refinement scheme, including exclusion clauses and learned constraints. Empirical evaluations on 1,481 benchmarks show substantial gains over state-of-the-art solvers (e.g., up to +183.6% for CVC5 with GPT-4.1) and strong performance on satisfiable instances, demonstrating that semantic intuition from LLMs can meaningfully augment formal reasoning. The results suggest a promising new paradigm for SMT constraint solving that blends semantic AI with symbolic methods, offering practical performance benefits and motivating further ensemble and iteration-based strategies.

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.

LLM-Guided Quantified SMT Solving over Uninterpreted Functions

TL;DR

This work tackles the hardness of solving quantified formulas with uninterpreted functions under non-linear real arithmetic, a problem formalized as . It introduces AquaForte, a hybrid framework that leverages Large Language Models to generate semantically grounded uninterpreted function instantiations and integrates these with traditional SMT solvers through an adaptive, soundness-preserving loop. The authors implement a structured preprocessing-instantiation-postprocessing pipeline, develop LLM-driven trigger synthesis, and couple these with existing techniques in an iterative refinement scheme, including exclusion clauses and learned constraints. Empirical evaluations on 1,481 benchmarks show substantial gains over state-of-the-art solvers (e.g., up to +183.6% for CVC5 with GPT-4.1) and strong performance on satisfiable instances, demonstrating that semantic intuition from LLMs can meaningfully augment formal reasoning. The results suggest a promising new paradigm for SMT constraint solving that blends semantic AI with symbolic methods, offering practical performance benefits and motivating further ensemble and iteration-based strategies.

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

This paper contains 27 sections, 8 equations, 3 figures, 3 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. SMT Foundations
  4. Solving Techniques for Quantified NIRA
  5. Large Language Models and Prompt
  6. Methodology
  7. Overview
  8. Uninterpreted Function Instantiation
  9. Preprocessing
  10. LLM Instantiation
  11. Post-processing
  12. Quantifier Elimination Strategies
  13. Integration with Traditional Algorithms
  14. Experimental Evaluation
  15. Benchmark Suite
  16. ...and 12 more sections

Figures (3)

  • Figure 1: Overview of AquaForte.
  • Figure 2: Total solved instances across different LLM-solver combinations with 24s timeout. Virtual Best represents the union of all LLM-enhanced configurations.
  • Figure 3: Performance across multiple iterations with 1200s timeout.

Theorems & Definitions (5)

  • Definition 1: SMT Problem
  • Definition 2: NIRA
  • Definition 3: Quantified NIRA
  • Example 1: E-matching Process
  • Example 2: Structured Prompt Design