Source-linked AI summary
VeriPIE: Checkable Query Plans and Evidence-Guided Selection for Text-to-SQL
Piyush Jha, Cruise Song, Zhengyu Li, Yatharth Sejpal
TL;DR
Text-to-SQL queries can return plausible results while computing incorrectly, and agreement on one database does not establish agreement with user intent. VeriPIE combines SQL generation with Lean-checked plans, diagnostics, and bounded checks; on Spider, it outperforms DeepEye in top-1 results and covers more questions with its two-query shortlist. Its evidence supports review, but does not establish semantic correctness or regulatory compliance.
Problem
Text-to-SQL queries can silently produce plausible but incorrect results, and traditional execution checks or agreement among generated queries do not establish computational correctness.
Source: §1 · p. 1Method
VeriPIE combines direct SQL generation with Lean-checked QuerySketch plans, using diagnostics for repair and execution agreement and bounded searches to inform selection.
Source: §1 · p. 1, §3.2 · p. 3Results
On Spider, VeriPIE answers 745 questions correctly at top-1 versus DeepEye’s 679, and its top-2 shortlist covers 811 questions versus DeepEye’s 714 and DIN-SQL’s 772.
Source: §5.1 · p. 4Takeaways & Limitations
VeriPIE provides inspectable computation evidence for independent validation and effective challenge, without establishing semantic correctness or regulatory compliance.
Source: §6 · p. 5Future work will evaluate financial reporting and regulatory workloads and extend counterexample-guided judging, repair, and efficient verification.
Source: §6 · p. 5
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
Financial model risk management calls for validation and effective challenge of AI-generated computations. VeriPIE addresses the text-to-SQL challenge by making query computations and selection evidence available for review.
1 INTRODUCTION
- Financial governance developments highlight the need for checkable components in financial AI applications.The passage cites model-risk, data-quality, and governance concerns and risk-based requirements for covered AI systems.Source: §1 · p. 1
- Incorrect text-to-SQL queries can silently omit exposures, double-count transactions, or miscalculate aggregates while returning plausible results.Execution checks and agreement among generated queries do not establish computational correctness or agreement with the user’s intent.Source: §1 · p. 1
- VeriPIE checks query plans with Lean, returns diagnostics to guide repair, and combines execution agreement with structural checks and bounded searches to inform selection.The checks narrow uncertainty about the generated computation but do not prove that it matches user intent.Source: §1 · p. 1
- The framework connects candidate generation, plan checking, repair, and selection through explicit evidence about each candidate, supporting review of operations and selection evidence.The paper evaluates the framework on the complete Spider and BIRD development sets.Source: §1 · pp. 1–2
2 RELATED WORK
VeriPIE builds on text-to-SQL generation, intermediate plan languages, and execution-based selection by adding checkable plans and evidence-aware candidate grouping. Its focus is computational evidence for independent validation in financial applications.
2 RELATED WORK
- VeriPIE extends text-to-SQL generation with a structured intermediate representation and augments selection with execution grouping, bounded verification, and ranking subject to additional checks.DeepEye-SQL combines multiple generators with deterministic checks and candidate selection [8].Source: §2 · p. 2
- QuerySketch extends QPL [3] and is elaborated in Lean into a common representation for validation, repair, SQL lowering, and equivalence checking.SemQL and NatSQL abstract selected SQL details [5], while QPL preserves query structure through explicit operator plans [3].Source: §2 · p. 2
- Execution voting ranks candidates by observed-result frequency, while bounded verification searches for counterexample databases within a fixed bound [7].A completed check finding none supports equivalence only within its encoded model and bound; VeriPIE can use checks and counterexamples to revise execution-based ranking.Source: §2 · p. 2
- VeriPIE emphasizes checkable computational evidence for independent model validation in financial applications, unlike approaches focused primarily on execution accuracy.Figure 1 depicts diagnostics guiding repair and execution agreement and bounded-equivalence evidence informing grouping and final selection.Source: §2 · p. 2, Figure 1 · p. 2
3 THE VERIPIE APPROACH
VeriPIE combines direct SQL generation and Lean-checked QuerySketch plans in a workflow that checks, repairs, groups, and selects candidates. Its stages provide evidence about executability and candidate agreement without establishing that a computation answers the user’s question.
3 THE VERIPIE APPROACH
- VeriPIE generates candidates from Direct-SQL and Lean-Backed pipelines, checks and executes them, repairs detected problems, then groups and ranks executable candidates.Reference SQL is not used during inference, and both pipelines feed a common grouping and selection stage.Source: §3 · p. 2
3.1 Direct-SQL VeriPIE
- Direct-SQL VeriPIE combines standard generation strategies with structural and execution checks, then buckets passing candidates by their observed results.Its checks cover parsing, executability, schema references, output shape, and question-relevant features such as aggregation and ordering.Source: §3.1 · p. 2
3.2 Lean-Backed VeriPIE
- QuerySketch is a QPL-derived plan language whose Lean parser and elaborator build syntax trees, resolve schema references, and check types before SQL lowering.Its typed relational core represents database operations, and the language supports expressions used by BIRD and Spider.Source: §3.2 · p. 3
- Accepted QuerySketch plans pass explicit checks for supported operations, schema references, and types; rejected plans receive diagnostics for repair.These checks do not establish that SQL lowering preserves every aspect of plan meaning or that the plan answers the question.Source: §3.2 · p. 3
3.3 Diagnostic Repair
- Repair uses failed-check feedback to revise candidates, and revised QuerySketch plans are parsed and elaborated before their generated SQL is checked again.A model revision is not itself evidence of success; repaired candidates rejoin selection through checked plans and execution results.Source: §3.3 · p. 3
3.4 Equivalence-Aware Grouping and Selection
- Execution buckets rank candidates by agreement on the observed database, while bounded checks can connect or separate structurally different candidates with counterexamples.A counterexample does not identify which candidate matches user intent, and bounded results are limited to the encoded model and search bound.Source: §3.4 · p. 3
- VeriPIE provides reviewable computational evidence for financial workflows, while human interpretation remains necessary to assess intended business meaning.The table caption identifies complete development-set results and defines Top-1, Top-2, and time, but the supplied passage gives no result values.Source: §3.4 · p. 3, Table 1 · p. 4
4 EXPERIMENTAL SETUP
The evaluation covers the complete Spider and BIRD development sets, whose scoring differs: Spider checks reference agreement across test databases, while BIRD scores on one benchmark instance. Results are based on one local run per system, with Top-1 as the primary metric and Top-2 measuring whether either returned query passes.
4.1 Benchmarks and Baselines
- Spider scores all 1,034 development questions across 20 databases with the official test-suite evaluator; BIRD scores 1,534 questions across 11 databases on the benchmark instance alone.Because BIRD can count coincidental agreement as correct, scores are not directly comparable across benchmarks.Source: §4.1 · p. 4
- One evaluation run per system used openai/gpt-5.6-luna through OpenRouter, with a 16-slot candidate budget for combined VeriPIE.The Lean arm allowed one plan-repair round; the full-development Direct-SQL replay used SpotIt+ with bound 2 and an 8-second timeout per checked pair.Source: §4.1 · p. 4
- DeepEye [8] supplies 16 direct-SQL candidates; its Direct-SQL-only ablation changes selection alone, while LLM-only listwise selection ranks the saved DeepEye pool without Lean candidates.MAC-SQL and DIN-SQL [11] represent modular generation and repair approaches; CHASE-SQL [10] offers diverse generation with learned pairwise selection.Source: §4.1 · p. 4
4.2 Evaluation Metrics
- Top-1 scores the first returned query, while Top-2 measures whether either returned query passes rather than automatic identification of the correct answer.For DIN-SQL and MAC-SQL, the second query comes from an independent complete generation attempt.Source: §4.2 · p. 4
5 RESULTS AND ANALYSIS
VeriPIE’s clearest reported gains are in Spider, especially shortlist coverage, while its BIRD differences are smaller. The analysis also notes higher Spider latency, proposes a scoring-based hypothesis for differing gains, and highlights reviewable disagreements as potentially valuable for MRM.
5.1 Main Results
- 745 Spider questions are correct at top-1 for VeriPIE versus DeepEye’s 679, while its top-2 shortlist covers 811 versus 714 for DeepEye and 772 for DIN-SQL.The top-1 difference from DIN-SQL is two questions (0.19 points), distinct from the 3.77-point top-2 difference.Source: §5.1 · p. 4
- VeriPIE exceeds DeepEye on BIRD by 0.45 points in top-1 accuracy and 0.07 points in top-2 coverage.The top-1-to-top-2 gap corresponds to 66 Spider and 74 BIRD questions where the second candidate succeeds after the first fails; interactive inspection is a potential use, not an evaluated interface.Source: §5.1 · p. 4
- 39.89 seconds is VeriPIE’s estimated mean Spider latency, versus 35.44 for DeepEye and 12.04 for DIN-SQL, while BIRD latency is 60.59 and 60.58 seconds for VeriPIE and DeepEye.The aggregate timings do not isolate the cost of individual checking stages.Source: §5.1 · p. 4
5.2 Interpreting the Benchmark Difference
- The scoring rules suggest that Spider’s test suite can distinguish candidates that agree on the original instance, whereas BIRD’s single-instance execution score cannot; this remains a hypothesis for the different gains.On the fixed combined pool, adding bounded evidence to structural selection improves Spider top-1 by 1.16 points, but does not establish the proposed explanation.Source: §5.2 · p. 5
- Identifying computational disagreements and producing reviewable counterexamples may be valuable from an MRM perspective even when benchmark accuracy improvements are modest.Source: §5.2 · p. 5
6 CONCLUSION
The conclusion presents VeriPIE as a text-to-SQL pipeline connecting generated answers to checkable evidence, with an inspectable basis for independent validation and effective challenge. It also identifies financial reporting and regulatory workloads as future evaluation targets.
6 CONCLUSION
- VeriPIE combines direct SQL generation with execution agreement, structural checks, and bounded counterexamples, while its Lean-backed arm checks, repairs, and lowers QuerySketch plans through a typed relational core.Reviewers can examine which operations passed checks, why a revision was needed, and where candidate answers disagree.Source: §6 · p. 5
- The evidence can strengthen AI governance without establishing semantic correctness or regulatory compliance.Source: §6 · p. 5
- Future work will evaluate financial reporting and regulatory workloads and extend counterexample-guided judging, repair, and efficient verification.Source: §6 · p. 5
A.1 QuerySketch and Repair Example
The example makes QuerySketch’s intermediate operations inspectable: a scan exposes columns needed for ordering, and TopSort selects a requested number of rows while returning specified output. A recorded repair example links failed type checks to a compatible plan that passes the Spider test suite.
A.1 QuerySketch and Repair Example
- TopSort sorts rows and keeps a requested number, as in selecting one youngest singer.Source: §A.1 · p. 5
- The scan exposes both name and age, then TopSort orders by age but returns only name, so age must remain available between steps despite not appearing in the final output.QuerySketch lets the checker examine intermediate dependencies before SQL generation.Source: §A.1 · pp. 5–6
- For “Show the stadium names without any concert,” initial plans failed type checking; diagnostic repair produced a compatible NOT EXISTS plan that passed the official Spider test suite.Source: §A.1 · p. 6
A.2 Agreement Beyond the Observed Database
On the observed payment table, NOT IN and NOT EXISTS can return the same unmatched accounts when identifiers contain no nulls. Adding a null can separate their results, leaving the question and schema to guide which treatment is intended.
A.2 Agreement Beyond the Observed Database
- With no null payment account identifiers, NOT IN and NOT EXISTS can return the same unmatched accounts.The example assumes non-null account identifiers.Source: §A.2 · p. 6
- Adding a null payment account identifier to a valid database can distinguish the two candidate queries.Their initial agreement depended on the current data.Source: §A.2 · p. 6
- The question and schema provide context for choosing the intended treatment of unmatched accounts.The separating database supplies a concrete reason to reconsider the candidates' apparent agreement.Source: §A.2 · p. 6
A.3 Two-Answer Baseline Protocol
DIN-SQL and MAC-SQL produce two answers through independent complete runs of their own pipelines. Rank 1 retains the original final output, while rank 2 comes from another complete generation attempt.
A.3 Two-Answer Baseline Protocol
- DIN-SQL and MAC-SQL obtain two answers through independent, complete runs of their own pipelines.Each baseline's second answer comes from another complete generation attempt, including normal refinement steps.Source: §A.3 · p. 6
- Rank 1 retains the original final output, while rank 2 is the final output of another full attempt.The second attempt includes the method's normal refinement steps.Source: §A.3 · p. 6
- Top-2 counts success when either final output is correct, so each reported baseline evaluation uses two generation attempts per question.Source: §A.3 · p. 6
A.4 Further Evaluation and Verification
The ablations find that combining generation paths gives the best Spider top-1 accuracy under a 16-slot budget, while bounded selection adds gains on the combined pool. Further work targets financial schemas, BIRD verification, and unevaluated extensions.
A.4 Further Evaluation and Verification
- Future evaluation will cover financial schemas and recurring reporting queries, and compare BIRD predictions with reference SQL using bounded equivalence checking.Planned reports distinguish counterexamples, completed bounded checks, and unknown outcomes to study coincidental correctness.Source: §A.4 · p. 6
- Judging and repair using a separating database are proposed extensions, not evaluated features; selective verification when leading buckets are close is another proposed latency direction.Source: §A.4 · p. 6
A.5 Generation and Selection Ablations
- Combined VeriPIE uses four standard direct-SQL candidates, four candidates from two refinement paths, and eight Lean-backed candidates.The refinement paths are decomposition with self-correction and schema-focused refinement; the Lean-backed candidates are checked, repairable plans lowered to SQL.Source: §A.5 · p. 6
- Selection ablations reuse the combined 8+8 pool: execution-only groups observed results, structural selection groups normalized SQL or Lean plans, and bounded selection adds verifier evidence.The shared question-based safeguards remain; bounded evidence can connect structurally different candidates or separate them when a counterexample is found.Source: §A.5 · p. 6, Table 2 · p. 6
- The repair ablation changes candidate validity within the combined slot allocation, rather than only replacing the selector on an unchanged executable pool.It uses original Lean plans before repair, retains invalid slots, and recomputes relevant SQL checks.Source: §A.5 · p. 6
- Structural plus bounded selection gains 1.16 percentage points over structural selection and 0.77 over execution-only selection on the fixed combined pool.Structural selection alone does not improve on execution-only selection; removing Lean plan repair costs 0.29 points.Source: §A.5 · p. 6, Table 2 · p. 6
- Combining generation paths achieves the best Spider top-1 accuracy under the same 16-slot budget, exceeding both paths alone.Table 2 reports Spider top-1 accuracy; generation variants start with 16 slots, and selection variants reuse the combined 8+8 pool.Source: §A.5 · p. 6, Table 2 · p. 6