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

LLM提出焦点集、SMT求解器验证，提升量化数组求解数量。

资讯摘要

论文提出LinguaArray框架，让LLM在量化数组SMT求解中提出小型语义焦点集（基项或约束），由传统SMT求解器作为唯一证明引擎并验证所有结果。作者报告在五种逻辑的1015个SMT-LIB实例上（1200秒超时含LLM延迟），LinguaArray最多求解69.1%的实例，求解数量较对应后端提升105%–397%。

要点速读

1. LLM仅通过可被求解器验证的窄接口提供语义焦点集，不直接作为证明或求解决策来源。
2. 框架在有限时间内交互，随后回退到后端求解器以缓解潜在性能退化。
3. 作者报告在1015个SMT-LIB实例上最多求解69.1%，求解数较后端提升105%–397%。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/31 08:00:18（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。