VeriPIE: Checkable Query Plans and Evidence-Guided Selection for Text-to-SQL
Piyush Jha, Cruise Song, Zhengyu Li, Yatharth Sejpal
cs.LO
Oct 12, 2026 · v1
cs.AI
TL;DR
Implements the QuerySketch plan language's parser, elaborator, and typed relational core in Lean to check and lower LLM-generated query plans to SQL.
Abstract
Financial Artificial Intelligence (AI) governance and model risk management (MRM) emphasize independent validation, transparency, and effective challenge of AI-generated computations. Text-to-SQL translates natural-language questions into Structured Query Language (SQL), but queries that agree on one database can still express different computations. We present VeriPIE, a neurosymbolic framework combining language-model generation with symbolic checks. It ensembles direct SQL generation with QuerySketch, a structured plan language checked by a backend implemented in Lean, a theorem prover and programming language. Plan diagnostics guide repair before SQL generation, while execution agreement and bounded searches for distinguishing databases inform candidate selection. These checks expose malformed plans and hidden disagreement without proving agreement with the user's intent. In single-run experiments on the complete Spider development set, VeriPIE achieves 72.05% test-suite accuracy (745/1,034), compared with DeepEye's 65.67% (679/1,034). Its two-query shortlist covers 78.43% (811 questions), compared with 74.66% for DIN-SQL (772) and 69.05% for DeepEye (714). On BIRD, VeriPIE reaches 68.90% execution accuracy and 73.73% two-query coverage. The central benefit is reviewable evidence about the generated computation: explicit plan checks, repair diagnostics, and concrete disagreements that support safer financial analysis.
Problem
Text-to-SQL queries produced by LLMs can agree on one database yet compute different things, which hinders independent validation in financial model risk management. Execution agreement alone does not establish what a generated query computes.
Approach
VeriPIE extends DeepEye-SQL by ensembling direct SQL generation with QuerySketch, a QPL-derived plan language. QuerySketch's parser, elaborator, and typed relational core are implemented in Lean; they type-check plans against the schema, produce diagnostics for repair, and lower plans to SQL. Candidates are grouped into equivalence-aware buckets using execution agreement and bounded SMT counterexample search (SpotIt+), then ranked.
Results
On the Spider dev set, VeriPIE reaches 72.05% top-1 test-suite accuracy, compared with 65.67% for DeepEye, and 78.43% top-2 coverage. On BIRD it reaches 68.90% execution accuracy. The Lean-backed pipeline alone reaches 71.18%, compared with 68.37% for direct SQL alone.
| Method | Spider Top-1 | Spider Top-2 | BIRD Top-1 | BIRD Top-2 |
|---|
| MAC-SQL | 64.99 | 68.09 | 63.89 | 67.01 |
| DeepEye | 65.67 | 69.05 | 68.45 | 73.66 |
| DIN-SQL | 71.86 | 74.66 | 62.65 | 65.71 |
| VeriPIE | 72.05 | 78.43 | 68.90 | 73.73 |
Spider (test-suite) and BIRD (execution) accuracy
