arXiv cs.AI· Piyush Jha, Cruise Song, Zhengyu Li, Yatharth Sejpal·· 3 天前AI 评分29
VeriPIE：面向 Text-to-SQL 的可检查查询计划与证据引导选择
VeriPIE: Checkable Query Plans and Evidence-Guided Selection for Text-to-SQL
AI 导读
VeriPIE 是一个神经符号框架，将语言模型生成与符号检查结合，通过 Lean 实现的后端校验 QuerySketch 结构化计划语言，并用计划诊断指导修复、以执行一致性和区分性数据库搜索筛选候选。
正文 · AI 翻译
摘要：金融人工智能（AI）治理与模型风险管理（MRM）强调对 AI 生成计算的独立验证、透明度与有效质疑。Text-to-SQL 将自然语言问题转换为结构化查询语言（SQL），但在同一数据库上结果一致的查询仍可能表达不同的计算。我们提出 VeriPIE，一个将语言模型生成与符号检查相结合的神经符号框架。它将直接 SQL 生成与 QuerySketch 集成，后者是一种结构化计划语言，由用 Lean（一种定理证明器和编程语言）实现的后端进行检查。计划诊断在 SQL 生成之前指导修复，而执行一致性和用于区分数据库的有界搜索则为候选选择提供依据。这些检查能揭示畸形计划和隐藏分歧，但无法证明与用户意图一致。在完整 Spider 开发集上的单次运行实验中，VeriPIE 达到 72.05% 的测试套件准确率（745/1,034），而 DeepEye 为 65.67%（679/1,034）。其双查询候选列表覆盖 78.43%（811 个问题），而 DIN-SQL 为 74.66%（772），DeepEye 为 69.05%（714）。在 BIRD 上，VeriPIE 达到 68.90% 的执行准确率和 73.73% 的双查询覆盖率。核心优势在于提供关于所生成计算的可审查证据：明确的计划检查、修复诊断以及具体分歧，从而支持更安全的金融分析。
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.17493 [cs.LO] |
| （或 arXiv:2610.17493v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.17493 由 DataCite 颁发 arXiv DOI（待注册） |
提交历史
来自：Zhengyu Li [查看电子邮件]
[v1]
2026年10月12日星期一 23:31:04 UTC（58 KB）
来源：arXiv cs.AI · arxiv.org