LLM 引导的未解释函数上的量词化 SMT 求解
人工智能
2026-01-09 v1
摘要
在非线性实数算术上带有未解释函数的量词化公式对可满足性模理论求解提出了根本性挑战。传统的量词实例化方法由于缺乏对 UF 约束的语义理解而陷入困境，迫使它们在有限的引导下搜索无界的解空间。我们提出了 AquaForte，一个利用大型语言模型为 UF 实例化提供语义引导的框架，通过生成满足约束的函数定义实例化候选，从而显著降低求解器的搜索空间和复杂度。我们的方法通过约束分离对公式进行预处理，使用结构化提示从 LLM 中提取数学推理，并通过自适应实例化将结果与传统 SMT 算法集成。AquaForte 通过系统性验证保持可靠性：产生 SAT 的 LLM 引导实例化求解原始问题，而 UNSAT 结果则生成排除子句用于迭代细化。通过回退到增强了学习约束的传统求解器来保持完备性。在 SMT-COMP 基准上的实验评估表明，AquaForte 解决了 Z3 和 CVC5 等最先进求解器超时的许多实例，在可满足公式上尤为有效。我们的工作表明，LLM 可以为符号推理提供有价值的数学直觉，为 SMT 约束求解建立了一种新范式。
引用
@article{arxiv.2601.04675,
title = {LLM-Guided Quantified SMT Solving over Uninterpreted Functions},
author = {Kunhang Lv and Yuhang Dong and Rui Han and Fuqi Jia and Feifei Ma and Jian Zhang},
journal= {arXiv preprint arXiv:2601.04675},
year = {2026}
}