LinguaArray：LLM 引导的可验证量化数组 SMT 求解框架
Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays
AI 导读
研究提出 LinguaArray 框架，由 LLM 提议小型语义焦点集（ground terms/约束），SMT 求解器仍作为唯一证明引擎并认证所有结果，用于量化数组求解。在五类逻辑、1015 个 SMT-LIB 实例、1200s 超时（含 LLM 延迟）评测中，LinguaArray 最多求解 69.1% 实例，比对应后端多解 105%–397%。
正文 · 原文
Abstract:Large language models can often identify useful semantic structure in formal artifacts, but their outputs cannot be trusted as proofs or solver decisions. We study whether LLMs can instead guide formal reasoning systems through a narrow, solver-verifiable interface. We instantiate this idea in quantified array SMT solving, where modern instantiation-based techniques can fail when key ground terms and equalities are hidden by auxiliary variables, axiom guards, and nested array terms. We observe that many instances are largely driven by a small set of focal ground terms or constraints, similar to the backdoor sets in SAT solving. Building on this, we present LinguaArray, a framework where an LLM proposes a small Semantic Focus Set (ground terms/constraints), while a conventional SMT solver remains the sole proof engine and certifies all results. LinguaArray uses these LLM-suggested, solver-validated finite sets to significantly enhance solver capability, solving additional satisfiable and unsatisfiable instances that the backend alone fails to solve. It interacts within a finite time and then falls back to the backend solver to mitigate potential regressions. Evaluation on 1015 SMT-LIB instances across five logics under 1200s timeout (including LLM latency) shows that LinguaArray solves up to 69.1% of instances and increases solved-instance counts by 105%--397% over the corresponding backends.
| Subjects: | Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.39435 [cs.AI] |
| (or arXiv:2610.39435v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.39435 arXiv-issued DOI via DataCite |
Submission history
From: Kunhang Lv [view email]
[v1]
Thu, 29 Oct 2026 06:13:59 UTC (302 KB)
来源：arXiv cs.AI · arxiv.org