LLM-Guided Quantified SMT Solving over Uninterpreted Functions

• URL: http://arxiv.org/abs/2601.04675v1
• Date: Thu, 08 Jan 2026 07:40:37 GMT
• Title: LLM-Guided Quantified SMT Solving over Uninterpreted Functions
• Authors: Kunhang Lv, Yuhang Dong, Rui Han, Fuqi Jia, Feifei Ma, Jian Zhang,
• Abstract summary: Quantified formulas with Uninterpreted Functions (UFs) over non-linear real arithmetic pose fundamental challenges for Satisfiability Modulo Theories (SMT) solving.<n>We present AquaForte, a framework that leverages Large Language Models to provide semantic guidance for UF instantiation.<n>Our approach preprocesses formulas through constraint separation, uses structured prompts to extract mathematical reasoning from LLMs, and integrates the results with traditional SMT algorithms.
• Score: 10.767268261124515
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version) [49.462399222747024]
  We propose a novel framework for the logical specification of non-Markovian rewards in Decision Processes (MDPs) with large state spaces.<n>Our approach leverages Linear Temporal Logic Modulo Theories over finite traces (LTLfMT)<n>We introduce a method based on reward machines and Hindsight Experience Replay (HER) to translate first-order logic specifications and address reward sparsity.
  arXiv  Detail & Related papers  (2026-02-05T22:11:28Z)
• Satisfiability Modulo Theory Meets Inductive Logic Programming [2.3791444696448085]
  ILP provides interpretable rule learning in relational domains, but remains limited in its ability to induce and reason with numerical constraints.<n>Recent work has begun to address these limitations through tighter integrations of ILP with Satisfiability Modulo Theories (SMT) or specialised numerical inference mechanisms.<n>In this paper we investigate a modular alternative that couples the ILP system PyGol with the SMT solver Z3. Candidate clauses proposed by PyGol are interpreted as quantifier-free formulas over background theories.<n>This supports the induction of hybrid rules that combine symbolic predicates with learned numerical constraints, including thresholds, intervals
  arXiv  Detail & Related papers  (2025-12-15T02:08:32Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• Do LLMs Dream of Discrete Algorithms? [0.7646713951724011]
  Large Language Models (LLMs) have rapidly transformed the landscape of artificial intelligence.<n>Their reliance on probabilistic inference limits their effectiveness in domains requiring strict logical reasoning.<n>This paper proposes a neurosymbolic approach that augments LLMs with logic-based reasoning modules.
  arXiv  Detail & Related papers  (2025-06-29T22:03:01Z)
• Worst-Case Symbolic Constraints Analysis and Generalisation with Large Language Models [7.658134651527103]
  Worst-case symbolic constraints analysis requires inferring the symbolic constraints that characterise worst-case program executions.<n>We show that even state-of-the-art large language models (LLMs) struggle when applied directly on this task.<n>We propose WARP, an innovative neurosymbolic approach that computes worst-case constraints on smaller concrete input sizes.
  arXiv  Detail & Related papers  (2025-06-09T19:33:30Z)
• LLM-Symbolic Integration for Robust Temporal Tabular Reasoning [69.27153114778748]
  We introduce TempTabQA-C, a synthetic dataset designed for systematic and controlled evaluations.<n>This structured approach allows Large Language Models (LLMs) to generate and executesql queries, enhancing generalization and mitigating biases.
  arXiv  Detail & Related papers  (2025-06-06T05:14:04Z)
• Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
  Chain-of-Thought (CoT) prompting enhances the reasoning of large language models (LLMs) by decomposing problems into sequential steps.<n>We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths.<n>SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
  arXiv  Detail & Related papers  (2025-04-13T13:35:41Z)
• Gap-Filling Prompting Enhances Code-Assisted Mathematical Reasoning [0.0]
  Chain-of-thought (CoT) and program-of-thought (PoT) fine-tuning are common methods to transfer LLM knowledge to small language models (SLMs) This paper introduces Gap-Filling Prompting (GFP), a novel two-step prompting strategy designed to enhance the problem-solving process for SLMs.
  arXiv  Detail & Related papers  (2024-11-08T08:52:59Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  We propose a new satisfiability-aided language modeling (SatLM) approach for improving the reasoning capabilities of large language models (LLMs) We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. We evaluate SATLM on 8 different datasets and show that it consistently outperforms program-aided LMs in the imperative paradigm.
  arXiv  Detail & Related papers  (2023-05-16T17:55:51Z)
• Exploring Viable Algorithmic Options for Learning from Demonstration (LfD): A Parameterized Complexity Approach [0.0]
  In this paper, we show how such a systematic exploration of algorithmic options can be done using parameterized complexity analysis. We show that none of our problems can be solved efficiently either in general or relative to a number of (often simultaneous) restrictions on environments, demonstrations, and policies.
  arXiv  Detail & Related papers  (2022-05-10T15:54:06Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  This paper studies Linear Temporal Logic over Finite Traces (LTLf) proposition letters are replaced with first-order formulas interpreted over arbitrary theories. The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
  arXiv  Detail & Related papers  (2022-04-28T17:57:33Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.