大型语言模型（LLM）能够在形式化文档中捕捉有用的语义结构，但其直接输出不能被视为可靠的证明或求解器决策。我们探索一种思路：让 LLM 通过一个狭窄且可由求解器验证的接口来引导形式化推理系统。本文将该思路落地到量化数组的 SMT 求解场景。
在现代基于实例化的求解技术中，关键的基元项和等式常被辅助变量、守卫公理以及嵌套数组项隐藏，导致求解器难以发现有效实例。观察发现，许多实例的求解过程主要受一小组“焦点基元项”或约束驱动，这与 SAT 求解中的 backdoor 集合类似。
基于此观察，我们提出 LinguaArray 框架。框架的工作流程如下：
- LLM 生成一个 语义焦点集合（Semantic Focus Set），其中包含少量的基元项或约束；
- 传统 SMT 求解器使用该集合进行实例化，同时负责所有证明工作并对 LLM 的建议进行验证；
- 若在有限时间内未取得进展，系统回退到纯后端求解器，以避免潜在的回归。
通过让 LLM 提供的焦点集合经过求解器的严格验证，LinguaArray 能显著提升求解能力，成功解决了后端单独求解器无法判定的可满足和不可满足实例。实验在 1015 条 SMT‑LIB 基准（覆盖五种逻辑）上进行，整体超时设为 1200 秒（包括 LLM 延迟）。结果显示，LinguaArray 的求解率最高可达 69.1%，相较于对应后端求解器，已解实例数提升 105%–397%。
点评：本工作展示了 LLM 与传统形式化工具的协同潜力，利用 LLM 的语义感知能力在受控范围内提供线索，而不牺牲可验证性，为 SMT 求解尤其是量化数组问题打开了新的提升路径。