Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays

📄 arXiv: 2610.39435v1 📥 PDF

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

分类: cs.AI

发布日期: 2026-10-29

💡 一句话要点

提出LinguaArray以解决量化数组SMT求解问题

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

关键词: 量化数组 SMT求解 大型语言模型 形式化验证 语义焦点集 自动定理证明 程序验证

📋 核心要点

  1. 现有的SMT求解方法在处理隐藏了关键项和等式的复杂实例时常常失败，限制了其应用。
  2. 本文提出LinguaArray框架，利用LLM建议的语义焦点集来增强传统SMT求解器的能力，确保结果的有效性。
  3. 在1015个SMT-LIB实例的评估中，LinguaArray解决了高达69.1%的实例，解决实例数量提升了105%至397%。

📝 摘要（中文）

大型语言模型（LLM）通常能够识别形式化文档中的有用语义结构，但其输出不能作为证明或求解器决策的依据。本文研究LLM是否可以通过一个狭窄的、可验证的接口引导形式推理系统。我们在量化数组SMT求解中实现了这一想法，提出了LinguaArray框架，其中LLM建议一个小的语义焦点集，而传统的SMT求解器则作为唯一的证明引擎，验证所有结果。实验表明，LinguaArray能够显著提升求解能力，解决更多的可满足和不可满足实例。

🔬 方法详解

问题定义：本文旨在解决量化数组SMT求解中，传统方法在面对复杂实例时的局限性，尤其是当关键项和等式被辅助变量和嵌套数组项隐藏时。

核心思路：通过引入LLM来建议一个小的语义焦点集，帮助求解器聚焦于关键约束，从而提高求解效率和准确性。

技术框架：LinguaArray框架包括两个主要模块：LLM模块负责生成语义焦点集，SMT求解器模块负责验证和证明结果。两者在有限时间内交互，确保求解的有效性。

关键创新：LinguaArray的创新在于将LLM与传统求解器结合，LLM不再直接输出结果，而是引导求解器关注关键约束，从而避免了直接依赖LLM输出的风险。

关键设计：在设计中，LLM建议的焦点集是有限的，并经过求解器验证，确保了结果的可信性。具体参数设置和验证机制在实验中进行了优化，以提高整体性能。

🖼️ 关键图片

fig_0

📊 实验亮点

LinguaArray在1015个SMT-LIB实例的评估中表现出色，解决了高达69.1%的实例，相较于传统求解器，解决实例数量提升了105%至397%。这一结果表明，LLM的引入显著增强了求解器的能力。

🎯 应用场景

该研究的潜在应用领域包括自动定理证明、程序验证和复杂系统建模等。通过提高SMT求解器的能力，LinguaArray能够在更广泛的实际问题中提供有效的解决方案，推动形式化验证技术的发展。

📄 摘要（原文）

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.