面向量化数组的可验证 LLM 引导焦点 SMT 求解

大型语言模型通常能够识别形式化产物中有用的语义结构，但其输出不能被视为证明或求解器决策。我们研究 LLM 是否能够通过狭窄且可由求解器验证的接口，引导形式化推理系统。我们在量化数组 SMT 求解中实例化了这一思想：现代基于实例化的技术在关键基础项和等式被辅助变量、公理守卫以及嵌套数组项隐藏时可能失效。我们观察到，许多实例主要由一小组焦点基础项或约束驱动，这与 SAT 求解中的后门集合相似。基于此，我们提出 LinguaArray：一种由 LLM 提出小型语义焦点集（基础项/约束）的框架，同时由传统 SMT 求解器作为唯一的证明引擎，并对所有结果进行认证。LinguaArray 使用这些由 LLM 提出、经求解器验证的有限集合，显著增强求解器能力，解决后端单独运行时无法解决的其他可满足和不可满足实例。该框架在有限时间内进行交互，随后回退到后端求解器，以减轻潜在的性能回退。在 1200 秒超时限制下（包括 LLM 延迟），对五种逻辑中的 1015 个 SMT-LIB 实例进行评估的结果表明，LinguaArray 最多可解决 69.1% 的实例，并使已解决实例数量较相应后端提高 105%--397%。