LLM-Guided Quantified SMT Solving over Uninterpreted Functions

📄 arXiv: 2601.04675v1 📥 PDF

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

分类: cs.AI

发布日期: 2026-01-08

💡 一句话要点

AquaForte：利用LLM指导的量化SMT求解器，解决未解释函数问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: SMT求解 量化公式 未解释函数 大型语言模型 约束求解

📋 核心要点

  1. 现有SMT求解器在处理包含未解释函数的量化公式时，面临搜索空间巨大和缺乏语义指导的挑战。
  2. AquaForte利用LLM生成函数实例化的候选，通过语义理解缩小搜索空间，并结合传统SMT算法进行求解。
  3. 实验表明，AquaForte能够解决传统求解器超时的实例，尤其在可满足公式上表现出显著优势。

📝 摘要（中文）

量化公式与非线性实数算术上的未解释函数（UF）为可满足性模理论（SMT）求解带来了根本性的挑战。传统的量词实例化方法由于缺乏对UF约束的语义理解而难以奏效，迫使它们在有限的指导下搜索无界的解空间。我们提出了AquaForte，一个利用大型语言模型（LLM）为UF实例化提供语义指导的框架，通过生成满足约束的函数定义的实例化候选，从而显著减少求解器的搜索空间和复杂度。我们的方法通过约束分离预处理公式，使用结构化提示从LLM中提取数学推理，并通过自适应实例化将结果与传统SMT算法集成。AquaForte通过系统验证保持可靠性：LLM指导的实例化产生SAT结果即可解决原始问题，而UNSAT结果则生成排除子句以进行迭代细化。通过回退到使用学习约束增强的传统求解器来保持完整性。在SMT-COMP基准上的实验评估表明，AquaForte解决了许多最先进的求解器（如Z3和CVC5）超时的实例，尤其是在可满足公式上。我们的工作表明，LLM可以为符号推理提供有价值的数学直觉，从而为SMT约束求解建立一种新的范例。

🔬 方法详解

问题定义：论文旨在解决含有未解释函数（Uninterpreted Functions, UFs）的量化公式的SMT（Satisfiability Modulo Theories）求解问题。现有方法，特别是传统的量词实例化方法，在处理此类问题时，由于缺乏对UF约束的语义理解，导致搜索空间巨大，效率低下，容易超时。

核心思路：论文的核心思路是利用大型语言模型（LLM）的语义理解能力，为UF实例化提供指导。LLM可以根据公式的约束条件，生成更有可能满足约束的函数实例，从而缩小搜索空间，提高求解效率。这种方法将LLM的数学推理能力与传统的SMT求解器相结合。

技术框架：AquaForte框架包含以下几个主要阶段：1) 约束分离：对输入的公式进行预处理，将约束条件分离出来。2) LLM提示：使用结构化的提示，引导LLM生成满足约束的函数实例化候选。3) 自适应实例化：将LLM生成的候选实例与传统SMT算法集成，进行求解。4) 验证与迭代：对求解结果进行验证，如果得到SAT结果，则问题解决；如果得到UNSAT结果，则生成排除子句，进行迭代细化。如果LLM指导的实例化失败，则回退到使用学习约束增强的传统求解器。

关键创新：该论文的关键创新在于将大型语言模型（LLM）引入到SMT求解过程中，利用LLM的语义理解能力来指导UF实例化。与传统的盲目搜索方法相比，LLM能够提供更有效的实例化候选，从而显著减少搜索空间。这种方法为SMT求解开辟了一条新的途径，即利用AI模型来增强符号推理能力。

关键设计：论文中关键的设计包括：1) 结构化提示：设计有效的提示语，引导LLM生成高质量的实例化候选。2) 自适应实例化策略：根据LLM生成的候选实例的质量，自适应地调整实例化策略。3) 验证与迭代机制：通过验证和迭代，保证求解的可靠性和完整性。4) 回退机制：在LLM指导的实例化失败时，回退到传统求解器，保证求解的完整性。

📊 实验亮点

AquaForte在SMT-COMP基准测试中表现出色，解决了许多Z3和CVC5等最先进的求解器超时的实例。尤其是在可满足公式上，AquaForte的性能提升显著，证明了LLM在符号推理方面的潜力。具体性能数据未在摘要中给出，但强调了其在解决困难实例上的有效性。

🎯 应用场景

该研究成果可应用于软件验证、程序分析、硬件设计等领域。通过提高SMT求解器的效率，可以更有效地验证软件和硬件系统的正确性，减少错误和漏洞。未来，该方法有望扩展到更复杂的约束求解问题，并与其他AI技术相结合，实现更智能化的系统验证。

📄 摘要（原文）

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.