VeriPIE: Checkable Query Plans and Evidence-Guided Selection for Text-to-SQL

Piyush Jha; Cruise Song; Zhengyu Li; Yatharth Sejpal

cs.LOOct 12, 2026

VeriPIE: Checkable Query Plans and Evidence-Guided Selection for Text-to-SQL

Authors: Piyush Jha, Cruise Song, Zhengyu Li, Yatharth Sejpal

Organizations: Georgia Tech

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.

Figures & tables

Panel of Figure 1 — Figure 1. The VeriPIE workflow. Diagnostics guide repair, and revised candidates return to checking. Lean checks apply to QuerySketch plans. Execution agreement and bounded-equivalence evidence guide grouping and final selection. Generate candidates, apply Lean checks and execution, repair failures with a loop back to checking, group into equivalence-aware buckets, and select the final query.

		Spider: test-suite evaluation			BIRD: execution evaluation
Method	Main mechanism	Top-1	Top-2	Time (s)	Top-1	Top-2	Time (s)
LLM listwise selection	Joint ranking of the candidate list	59.48	66.34	38.00	60.95	67.86	63.82
MAC-SQL	Schema selection, decomposition, refinement	64.99	68.09	5.26	63.89	67.01	19.06
DeepEye	Execution agreement, confidence-aware judging	65.67	69.05	35.44	68.45	73.66	60.58
DIN-SQL	Decomposition and self-correction	71.86	74.66	12.04	62.65	65.71	13.23
VeriPIE	Plan checks, repair, equivalence-aware selection	72.05	78.43	39.89	68.90	73.73	60.59

Table 1. Complete development-set results. Top-1 is first-query accuracy. Top-2 is coverage by either returned query (both percentages). Time is estimated mean seconds per question. Bold marks the highest accuracy or coverage.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Configuration	Top-1 (%)
VeriPIE	72.05
Candidate generation
Direct-SQL only (16 direct)	68.37
Lean-Backed only (16 Lean)	71.18
Selection on the same combined pool
Execution-only selection	71.28

Appendix

Table 2. Spider top-1 accuracy. Higher values are better. All generation variants start with 16 slots. Selection variants reuse the combined 8+8 pool.

Execution-Guided Text-to-SQL

See all 17 papers

What Predicts Correctness in Text-to-SQL? A Selective-Prediction Study
Jul 7, 2026Robert RichardsonLLM Answer Verification Selective Prediction
Affiliation
Spider 2.0-AIFunc: Extending Real-World Text-to-SQL to AI-Native SQL Workflows
Jul 7, 2026Tianyang Liu, Canwen Xu, Fangyu Lei +6Text-to-SQL Relational Databases
1UC San Diego · *Work done during Tianyang Liu’s internship at Snowflake. · 2Snowflake AI Research +1
SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints
Mar 4, 2026Andrew Tremante, Yang He, Rocky Klopfenstein +3Text-to-SQL Evaluation Text-to-SQL
∗Amherst College · †Simon Fraser University · ‡VMware Research by Broadcom

Jul 7, 2026J/K move · Enter open · S save

What Predicts Correctness in Text-to-SQL? A Selective-Prediction Study

Robert Richardson

Affiliation

LLM Answer Verification Selective Prediction Text-to-SQL LLM Uncertainty Estimation Text-to-SQL Evaluation

Open paper AskPDF arXiv

Evaluating uncertainty in AI-generated SQL queries requires estimating whether a query is correct, where correct means it executes to the same result as a human-written reference. We study which signals predict correctness on hard multi-table text-to-SQL, using AUROC to measure how well each ranks correct queries above incorrect ones. On BIRD and Spider, black-box signals such as string, structural, and execution self-consistency, a schema-relevance score, and query executability all fall between about 0.61 and 0.68 AUROC, with string self-consistency strongest at 0.675; white-box log-probability is similar (0.67). The signals that move past this ceiling are verification-based: an LLM judge scores from 0.72 (GPT-4o-mini) to 0.78 (Claude). Judges from different providers make different errors, so a two-provider ensemble reaches 0.82 AUROC with a well-calibrated probability (expected calibration error 0.03) and supports useful abstention frontiers (for example, answering 27% of questions at 24% selective risk) where self-consistency offers no valid low-risk subset. The pattern holds across two benchmarks, two generators, and two judge providers. We also ask whether a verifier can be trained. Fine-tuned verifiers, both encoder and generative, reach about 0.77 to 0.79 AUROC in-distribution but fall to about 0.66 on unseen schemas; scaling to 7B, adding schema diversity, distilling a strong judge's rationales, and cross-benchmark training all fail to close that gap. Cross-schema transfer appears to track model scale and reasoning rather than fine-tuning. In practice, correctness uncertainty for text-to-SQL lives in reasoning-based signals: a fine-tuned verifier is a good in-domain tool, but a verifier that generalizes across schemas currently means a large frozen reasoning model.

Abstract

Execution-Guided Text-to-SQL

Explore similar work

What Predicts Correctness in Text-to-SQL? A Selective-Prediction Study

Spider 2.0-AIFunc: Extending Real-World Text-to-SQL to AI-Native SQL Workflows

SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints