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

arXiv: https://arxiv.org/abs/2610.17493 · HTML: https://mlsanity.com/paper/2610.17493/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 10 of its 18 references that are in the map.
- First posted on arXiv 12 Oct 2026.

## Builds on (most cited first, 10 of 10)

- [Can LLM Already Serve as A Database Interface? A BIg Bench for Large-Scale Database Grounded Text-to-SQLs](https://mlsanity.com/paper/2305.03111/) (2023)
- [DIN-SQL: Decomposed In-Context Learning of Text-to-SQL with Self-Correction](https://mlsanity.com/paper/2304.11015/) (2023)
- [MAC-SQL: A Multi-Agent Collaborative Framework for Text-to-SQL](https://mlsanity.com/paper/2312.11242/) (2023)
- [Semantic Evaluation for Text-to-SQL with Distilled Test Suites](https://mlsanity.com/paper/2010.02840/) (2020)
- [Natural SQL: Making SQL Easier to Infer from Natural Language Specifications](https://mlsanity.com/paper/2109.05153/) (2021)
- [TalkToModel: Explaining Machine Learning Models with Interactive Natural Language Conversations](https://mlsanity.com/paper/2207.04154/) (2022)
- [DeepEye-SQL: A Software-Engineering-Inspired Text-to-SQL Framework](https://mlsanity.com/paper/2510.17586/) (2025)
- [Semantic Decomposition of Question and SQL for Text-to-SQL Parsing](https://mlsanity.com/paper/2310.13575/) (2023)
- [SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification](https://mlsanity.com/paper/2510.26840/) (2025)
- [LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers](https://mlsanity.com/paper/2609.21492/) (2026)

## Abstract (arXiv)

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.