LLM引导的可验证焦点SMT求解用于量化数组
原文：Verifiable LLM-Guided Focal SMT Solving for Quantified Arrays
大型语言模型通常能在形式化产物中识别有用的语义结构，但其输出不能被信任为证明或求解器决策。我们研究LLM能否转而通过一个狭窄的、求解器可验证的接口来引导形式推理系统。我们在量化数组SMT求解中实例化这一想法，现代基于实例化的技术在关键基项和等式被辅助变量、公理守卫和嵌套数组项隐藏时可能失败。我们观察到许多实例在很大程度上由一小部分焦点基项或约束驱动，类似于SAT求解中的后门集。在此基础上，我们提出LinguaArray，一个由LLM提出小型语义焦点集（基项/约束）、而传统SMT求解器仍是唯一证明引擎并认证所有结果的框架。LinguaArray利用这些LLM建议、求解器验证的有限集合显著增强求解器能力，额外求解后端单独无法求解的可满足和不可满足实例。它在有限时间内交互，然后回退到后端求解器以缓解潜在的性能退化。在1200秒超时（含LLM延迟）下对五种逻辑的1015个SMT-LIB实例进行评估，结果显示LinguaArray最多求解69.1%的实例，并将求解实例数较相应后端提升105%至397%。作者：Kunhang Lv、Rui Han、Fuqi Jia、Yuhang Dong、Feifei Ma。类别：cs.AI