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的语义理解能力，生成满足约束的函数实例化候选，从而缩小搜索空间并提高求解效率。
  3. 实验表明，AquaForte在SMT-COMP基准测试中，显著优于Z3和CVC5等先进求解器，尤其是在可满足性问题上。

📝 摘要（中文）

量化公式与非线性实数算术上的未解释函数(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约束的语义理解，导致搜索空间巨大，效率低下，容易超时。

核心思路：论文的核心思路是利用大型语言模型（LLMs）的语义理解和推理能力，为UF的实例化提供指导。LLM可以根据公式的约束条件，生成更具针对性的实例化候选，从而显著减少求解器的搜索空间，提高求解效率。这种方法将LLM的语义推理能力与传统SMT求解器的符号推理能力相结合。

技术框架：AquaForte框架包含以下几个主要阶段：1) 公式预处理：通过约束分离等技术，简化原始公式。2) LLM提示生成：构建结构化的提示，引导LLM提取数学推理。3) LLM实例化：LLM根据提示生成UF的实例化候选。4) 自适应实例化：将LLM生成的实例化候选集成到SMT求解器中，并根据求解结果进行迭代优化。5) 验证与回退：通过系统验证保证可靠性，并在必要时回退到传统求解器。

关键创新：最重要的技术创新点在于将LLM的语义理解能力引入到SMT求解过程中，利用LLM生成更有效的实例化候选。与传统方法相比，AquaForte不再盲目搜索，而是有针对性地进行实例化，从而显著提高了求解效率。这种结合语义推理和符号推理的思路是该论文的关键创新。

关键设计：AquaForte的关键设计包括：1) 结构化提示：精心设计的提示能够引导LLM产生高质量的实例化候选。2) 自适应实例化策略：根据求解器的反馈，动态调整实例化策略，避免引入无效的实例化。3) 验证机制：通过验证机制保证求解结果的可靠性，避免LLM引入错误的实例化。

📊 实验亮点

AquaForte在SMT-COMP基准测试中表现出色，解决了许多Z3和CVC5等最先进的求解器超时的实例。尤其是在可满足性问题上，AquaForte展现了显著的优势，证明了LLM在符号推理中的价值。实验结果表明，AquaForte能够有效地利用LLM的语义理解能力，提高SMT求解器的效率。

🎯 应用场景

该研究成果可应用于软件验证、硬件设计、人工智能安全等领域。通过提高SMT求解器的效率，可以更有效地验证软件和硬件系统的正确性，检测人工智能系统中的漏洞，并为形式化方法在实际应用中提供更强大的支持。未来，该方法有望扩展到更复杂的约束求解问题，推动相关领域的发展。

📄 摘要（原文）

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.