LLM 引导的未解释函数量化 SMT 求解

带未解释函数（UF）的非线性实数算术上的量化公式，给可满足性模理论（SMT）求解带来了根本性挑战。传统量词实例化方法之所以举步维艰，是因为它们缺乏对 UF 约束的语义理解，只能在有限引导下搜索无界的解空间。我们提出 AquaForte，一个利用大语言模型为 UF 实例化提供语义引导的框架：通过生成满足约束的函数定义实例候选，显著降低求解器的搜索空间与复杂度。我们的方法通过约束分离对公式进行预处理，使用结构化提示从 LLM 中提取数学推理，并通过自适应实例化将结果与传统 SMT 算法集成。AquaForte 通过系统化验证保持可靠性（soundness）：经 LLM 引导的实例化若判定为 SAT，即可解决原问题；而 UNSAT 结果会生成排除子句用于迭代精化。完备性则通过回退到以学到的约束增强的传统求解器来保留。在 SMT-COMP 基准上的实验评估表明，AquaForte 求解出了 Z3、CVC5 等最先进求解器超时的众多实例，对可满足公式尤为有效。我们的工作表明，LLM 能够为符号推理提供有价值的数学直觉，为 SMT 约束求解确立了一种新范式。