SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
Authors: Rocky Klopfenstein
YANG HE
Andrew Tremante
Yuepeng Wang
Nina Narodytska
Haoze Wu
Venue: ICLR 2026 Poster (2026)
Keywords: Text-to-SQL
Formal Equivalence Checking
Satisfiability modulo Theories
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: Community-driven Text-to-SQL evaluation platforms play a pivotal role in tracking the state of the art of Text-to-SQL performance. The reliability of the evaluation process is critical for driving progress in the field. Current evaluation methods are largely test-based, which involves comparing the execution results of a generated SQL query and a human-labeled ground-truth on a static test database. Such an evaluation is optimistic, as two queries can coincidentally produce the same output on the test database while actually being different. In this work, we propose a new alternative evaluation pipeline, called SpotIt, where a formal bounded equivalence verification engine actively searches for a database that differentiates the generated and ground-truth SQL queries. We develop techniques to extend existing verifiers to support a richer SQL subset relevant to Text-to-SQL. A performance evaluation of ten Text-to-SQL methods on the high-profile BIRD dataset suggests that test-based methods can often overlook differences between the generated query and the ground-truth. Further analysis of the verification results reveals a more complex picture of the current Text-to-SQL evaluation.

Published as a conference paper at ICLR 2026
Q EVALUATING TEXT-TO-SQL EVALUATION WITH FORMAL VERIFICATION
Rocky Klopfenstein', 1, Yang " Andrew Tremante's Yuepeng Wang",
Nina Narodytska", Haoze Wu
1 Amherst College 2Smon Fraser University 3VWaree Research by Broadcom {rk wikllofensteinng 227, atremante26, www.@ammerst... edu [yha244, yuepeng) sfu. ca, nina. www.naattrtttrrrrroooooo
com
ABSTRACT
Community-driven Text-to-SQL evaluation platforms play a pivotal role tracking the state of the art of Text-to-SQL performance. The reliability of the evaluation process critical for driving progress in the field. Current evaluation methods are largely test-based, which involves comparing the execution results of generated SQL query and a human-labeled ground-truth on a static test database. Such an evaluation is optimistic, two queries can coincidentally produce the output on the test database while actually being different. In this work, we propose a new alternative evaluation pipeline, called SPOTIT, where formal bounded equivalence verification engine actively searches for database that differentiates the generated and ground-truth SQL queries. We develop techniques to extend existing verifiers to support richer SQL subset relevant to Text-to-SQL. A performance evaluation of ten Text-to-SQI. methods on the high-profile BIRD dataset suggests that test- based methods can often overlook differences between the generated query and the ground-trun truth. Further analysis of the verification results reveals a more complex picture of the current Text-to-SQL evaluation.
INTRODUCTION
Text-to-SQL is one of the fundamental building blocks for designing natural language (NL) interfaces that enable users to access and analyze structured data sources. Translating human questions into executable database queries bridges the gap between non-technical users and complex data systems. This functionality underpins modern chatbots and smart assistants across a wide range of industrial applications, such observability platforms for monitoring system health (BitsAl 2025 Splunk 2025). critical business processes (Amazon 2025). and healthcare (Amazon Web Services 2024).
Due to its practical relevance for commercial products, Text-to-SQL has recently attracted significant attention, leading to the development of a wide range of solutions (Shi et al. (2024). New Text-to-SQL frameworks are announced regularly, and thanks to community-drivve
evaluation platforms such as BIRD (Li et al. 2024) and Spider (Lei et al. 2024), their performance can be benchmarked and compared in near real time. Given the pivotal role these platforms play in tracking the state of the art, the reliability of their evaluation processes is crucial for driving progress in the field.
In this paper, we take a close look the evaluation process for the accuracy Text-to-SQL methods. Currently, the process usually involves checking whether the SQL queries generated by a method produce results equivalent to those of the gold SQLs (i.e., numan--ritter ground- SQLs), under pre-defined notion of equivalence. Most ontte-of-thh-art evaluation frameworks (Li al.) 2024 Lei jet al.) 2024) perform this equivalence check through lesting: executing both queries on a static test database and comparing the results. If the results match, the generated SQL is labeled correct. Although widely used in practice, the resting-based approach has clear limitations. Because the check is performed on a single database, two different SQL queries may appear equivalent by chance, purely due to the specific data contained in that database. This raises an important question: when the test-based approach marks generated SQL correct, how often does it truly produce the same
"qqual contribution.

---

Published as a conference paper at ICLR 2026
results the gold SQL in general? The next broader question is: to what extent can the current evaluation process accurately measure the performance of Text-to-SQL methods?
We investigate these questions by exploring alternative correctness evaluation methodology. Instead of relying on test databases to assess equivalence, wc propose to actively search for databases that can differentiate the generated SQL from the gold SQL. The search-based evaluation naturally provides stronger correctness guarantees and enables a more rigorous measurement of accuracy. Since providing complete equivalence guarantee is in general undecidable, we perform SMT-based bounded verification (He et al., 2024), which searches for differentiating databases with specified sizes. We develop new Text-to-S SQL evaluation workflow. SPOTIT, on top of those verification techniques. We significantly extend these techniques to support new set of SQL operators over strings and dates which are commonly used for Text-to-SQI. benchmarks.
Experiments on ten state-of-the-art Text-to-SQL methods on the popular BIRD dataset (Li et al. 2024) suggest that the reported accuracy of these methods drops by 11.3%-14.2%% when switching from the official test-based evaluation to SPOTIT. The varying levels of decrease in absolute precision also lead to substantial changes in the order of ranking the Text-to-SQL methods. Moreover, SPOTIT produces minimal differentiating databases, which enables us to pinpoint the sources of inconsistencies between the generated and gold SQLs. Analysis of these databases uncovers several shortcomings of the current Text-to- toLSQL evaluation process. Most surprisingly, we find that when the predicted SQL disagrees with the ground truth, it is often the gold SQL. that is incorrect.
To summarize, contributions include:
SPOTIT, new evaluation pipeline for Text-to-SQL powered by formal equivalence verification;
novel SMT-encoding for a set of operators over strings and dates, and proof of correctness;
practical strategies for the efficient deployment of SPOTIT;
large-scale evaluation of ten oate-of-the-art Text-to-SQL. methods on the BIRD dataset, which reveals several potential shortcomings of current Text-to-SQL evaluation.
2 PRELIMINARIES
We provide background on Text-to-SQL. and formal equivalence checking. Due to space limitation, an overview of related work is present in App.AA
Text-to-SQL problem statement. Given natural language query N and database with schema S, the goal of Text-to-SQL is to map (N, D) to an SQL query Q, such that executing Q D, denoted Q(D), produces an output relation (table) that answers N.
Text-to-SQI. evaluation. The main evaluation mechanism for a Text-to-SQL. framework relies gold SQL query produced by human annotator. Hence, for each natural language query N over database, there exists a gold SQL query Q that represents the human-labellle ground truth of translating N into SQL. Given a generated SQL P and the corresponding gold query Q, current evaluation performs the following check:
EX-TEST Q, Duss)) = [1, if r E P(Dies) + r Q(Drss)
0. otherwise,
where Dies is test database provided by the benchmark set, and r denotes a row in the result table. In words, EX-TEST compares whether the two tables, P(Dtess) and Q(Dies),, contain the same set of rows. In order to more rigorously analyze the equivalence between P and Q, we use formal verification to search for differentiating database Deex such that EX-TEST(P, Q, Deex) = 0.
Bounded SQL equivalence checking. Given two SQL queries Q1 and Q2 over a schema S and an upper bound K on the relation size, the problem of bounded equivalence checking to decide whether Q1 and Q2 are equivalent, denoted Q1 S. Q2, for all databases 1 conforming to S such that each relation D has most K tuples. Formally,
Q =S,K Q2 def VD E Instances(S). VR E Relations(D). [R] < K + Qi() = Q2)),
where Instances(S) represents all database instances conforming to S, and Relations(D) represents all relations in D. In general, the goal is either to prove the bounded equivalence holds, or to find a counterexample database Dees that disproves the equivalence. Compared with unbounded equivalence
2

---

Published as a conference paper at ICLR 2026
"Which the youngest patient on abnormal ont-ribonuclear protein level?
N2: 'How many male ponienss who underwent testing berween 1995 and 1997 and were subsequently diagnosed with Beheet disease did stay the hospital for treament?"
Please Hist his her date of birth."
I-Gold BQL Q+/:
/+5old SOr. Q-/:
SELECT T1. 11.birthday
SELECT BOUNT (TI, FROX patien: AS T1
FROM patient AS 21
INNER JO1N examiratior. AS T2 ON 11.id -2.id
TNNER 50TN Laboratory AS T2
WHERT T2. agnossis = 'Behcet' AND T1.sex = 'M STRPTIME (' ('32r, r2.examinalion
I2.ID
WHERE 122.mp 1-
OR
BETWEEN " "1995' AND '1997' AND al.admission 1-4
ORDER BY Ti.birthday DESC LIMIT
/+Senerated SOT. P+/:
/+Generated SQI P-/:
SELECT BOUNT (DISTINCT pasient.id] FROM pat INNER JOIN axamination ON patient. examiratlor. NHERE patient. examinatioon exneetttaatio iot_daaattooddateee DE TWEEN "1995 02 01 AND '1997 12 31' AND wxminattion.elagnost patient, admissiinnn '-";
SELECT petient.birttiae
FROM patient
INEER JOIN Laberstory
'M' AND
ON patient..1' Labcratory.
NHERE NOT Laberatory. IN ("-', 1
ORCER BY patient.birthas.
'Behcet'
DESC LIMIT 1
Figure I: Examples of cases where the generated SQL produces the same output as the gold SQL on the BIRD's official test database, but SPOTIT finds database that differentiates the the queries. The parts that explain the mismatch are highlighted. For Ni, the gold SQL is incorrect. And for N2, both SQL queries can be right depending on the interpretation of the NL question.
checking, which is generally undecidable (Mohamed et al. 2024), bounded equivalence checking can handle more expressive SQL subset and guaranteed to uncover small counterexamples (if they exist). These features make bounded verification suitable for large-scale Text-to-SQL. evaluation.
VERIEQL. VERIEQL (He al., 2024) is recently proposed bounded equivalence checker for SQL queries and, to the best of our knowledge, supports the most expressive subset of SQL. among existing tools. It reduces the verification task satisfiability problem by encoding the symbolic execution of the two SQL queries and the non-equivalence of the execution results as a satisfiability modulo theories (SMT) formula (Barrett Tinellil 2018), which can be solved by an off- off-the-shie shelf SMT solver (De Moura & Björner] (008). The bounded equivalence property holds if and only if the formula is unsatisfiable, which means is not possible to find database that result in different execution results. Otherwise, a satisfying interpretation of the formula can be decoded to counterexample database. We significantly extend VERIEQL to support our verification use cases.
3 MOTIVATING EXAMPLES
Before we describe our new verification-based evaluation pipeline, we first discuss main sources of mismatches between the gold SQL and the generated SQL in Text-to-SQL evaluation. -vaauuttttvlllutiooonn..m.m There are three main such sources: (1) NL query N is ambiguous, so both the gold and generated SQL queries are justifiable interpretations; (2) N is unambiguous, but the gold SQI. query is incorrect (gold SQI is are created manually and thus prone to human errors); (3) N is unambiguous, the gold SQL. query is correct, but the generated SQL query is incorrect. Our framework focuses on checking equivalence between the gold SQL and the generated SQL, treating the latter as the best-effort, semantically correct formalization of N. We show that SPOTIT can successfully detect incorrect generated SQLs that are overlooked by existing best- evaluation. Perhaps more surprisingly, SPOTIT also allows us to spot the first and second sources of mismatch. Fig. shows two illustrative examples.
Example 3.1. Consider the query Ni: "Which is the youngest patient with abnormal anti- ribonuclear protein level? Please list his or her date of birth." together with the gold and generated SQL queries. On the development database that BIRD provides, both queries return "1989-08-28", However, SPOTIT found database on which these two queries are not equivalent (Appendix D.I). In fact, we observe that all ten frameworks that we tested generated SQLs that are not equivalent the gold query. Upon closer inspection, we find that the gold query is incorrect: its WHERE clause is equivalent to T2.rnp != f_' OR FALSE, as a string literal like 4+- is interpreted as FALSE in boolean context, which is not the intended behavior.
Example 3.2. Consider another query N2: "How many male patients who underwent testing between 1995 and 1997 and were subsequently diagnosed with Behcet disease did not stay in the hosiptal for treatment?" together with the gold and generated SQL queries. These two queries both return "2" on the BIRD test database. However. the two queries are clearty not equivalent (id is not a primary key of the exami t on table therefore duplicates are allowed): the generated query county all
3

---

Published as a conference paper at ICLR 2026
Query Qr
= Q (Q. E.
Subquery Q
= R (Q) [Q) pn(Q) (Q @ @ Distinct(()) ()) Q @ Q GroupBy(Q, E, o.) With(Q. R. Q)
Attr List
=
id(A) P.)4) L.2
Attr
Cast(d) E |A
Pred 2 b Null A @ [E) E e | E
PrefixOr(s, E) S E) Like(s E) Contain E)
Expr
a lel o B| [EE( E, B) Casef E, E) SubSStr E,, E2. Es) Concat( E1, Eg)
Strftime(x, E) JulianDay (E) DateShift
Toint(B) ToDate(E) ToStr(E)
Join Op
&
=
x b4g 24l DCg pxtp
Collection
U
Arith Op
==
+ X 1111 + 2
Logic Op
Si<l
E
b E Bools i Integers Strings 9 (Count, Min, Max, Sum, Avg) ("%Y", "%M", "%d") 6 ("Year", "Month", "Day""
Relation Names a Attribate Names e E (Null) U Integers Dates U Strings
Figure 2: Extended syntax of SQL Queries. New features are in bold.
examinations per patient, whereas the gold query counts only distinct patients. SPOTIT easily found database that differentiate the two queries Appendix(D.2) Note that depending on the interpretation of the question, both SQL queries can be correct: the gold SQL can be reasonable if the goal is to understand the hosptial workload, while the generated SQL can be reasonable if the goal is to understand the number of unique patients. Hence, we conclude that N₂ is ambiguous.
Note that these examples were overlooked by existing test-based evaluations. On the other hand, using SPOTIT, we found that undetected cases like those are quite common in the BIRD dataset.
METHODOLOGY
In this section, introduce SMT-encodings for number of SQL operators string and date types that were not supported by existing bounded equivalence verification methods but frequently appear in Text-to-SQL benchmarks. Then we present verification-based evaluation pipeline SPOTIT and discuss practical implementation strategies.
4.1 EQUIVALENCE CHECKING FOR SQL QUERIES
To understand our extension, let first walk through Example 4.1
understand how equivalence checking can be encoded as an SMT formula a verifier like VERTEQL (He et al.) (2024).
Example 4.1. Consider schema S {R + fid:int, dob:date)) and the following two queries:
Q1 SELECT id FROM R WHERE MdS
Q2=SELECT id FROM R WHERE i832
We describe how to encode equivalence checking for bound (K) of I as an SMT formula. First, variables are introduced to represent the database and the execution results. This includes symbolic database = ( R >> [[1]], where 4 = [x1, is tuple R, and xı, 82 are integer variables. In addition, tuples 1/ = [2a] and i3 [ra], are introduced to encode query results: (D) = [t2] and (D) = [ta), where 33, Fg are both integer variables. Note that the number of tuples in equal to the bound K. Also note that date (I2) is represented as integer, which is sufficient here but not in general. We later introduce precise encoding of date to support richer operations.
We describe the constraints over the variubles. The first set of constraints ensures thut L2 and by correctly capture the semantics of Qı and Q2. In this case, t2 tuple is constrained by &Q. (x1 > 1 (x3 Iz A -Del(t2))) A (æ1 - Del(tz)), where Del is an uninterpreted function denoting the non-existence of a symbolic tuple. The formula TQ2 ensures that only interpretations satisfying can populate concrete tuple; otherwise, Q1 ''s result is empty. Similarly, to is constrained by 4Q2 = (2) 2 (I4 21 -Del(ta)) A (x1 5 + Del(ta)).
The second of constraints encodes that (D) and Q2(D) returns different results. In this case, it is simply la + lz. The full encoding is a conjunction of all constraints: &22 A AQ2 A (l2 & la), whose satisfiability can be checked by an SMT solver. A satisfying interpretation to this conjunction corresponds to database instance that differentiates Q1 and Q2. For example, the queries are not equivalent under the interpretation I {γ] + 2}.
Extension in SQL encoding. Existing bounded SQL equivalence checker still lacks support for several important features, including precise encoding of dates and strings, which are highly relevant
4

---

Published as a conference paper at ICLR 2026
in Text-to-SQL applications. Furthermore, SQL supports computations across many different data types with implicit type casting (e.g.. 1+ "a" and dat datte((000000-001") "1"), which poses significant challenges to establish precise semantics and encodings. To address these limitations and challenges, we introduce techniques to support dates and strings, along with their manipulations, in the SQL equivalence checker VERIEQI.. We also introduce type conversions across Null, integers, dates, and strings for implicit type casting. For example, in the gold SQL for N2 (Fig. [.. the output of the STRETIME function is implicitly converted from a date an integer.
Fig. 2 presents our supported SQL grammar. Specifically, the query language introduces type conversions among various data types (e.g.. Tolnt(E), E)), To), and (E)),, which allows us to precisely establish the semantics of dates and strings and enhances the expressiveness of our SQL. subset. We also incorporate additional expressions and predicates for data and string manipulations, such as date formatting Strftime(k, (k., F),, Julian day JulianDay((E) (E), string pattern matching PrefixOf(ss, E), SuffixOf(s, E), Like(s, F),, and string truncation SubStr E1, E2g, Fg). The symbolic encoding for these extended expressions and predicates is formally presented in Appendix F
As an example, we describe how to precisely encode a date variable, which is very common in Text-to-SLL. For instance, the date of birth and the time of transaction are naturally modeled with the date type. Previously, date was encoded as a single integer variable (see Example[4.1] Although this coarse representation still enables the encoding of certain date operations (c.g.. comparison), it does not necessarily support all date operations, such as nate-formatting, which is used in the gold As date can be viewed triplet (year, month, day), we introduce
SQL query for N₂ in Fig. [ three integer variables y, m, and d, and constrain their values with the following formula Φ:
①- = 1 A 22 A 43. where 1 = MIN YEAR S y S MAX YEAR, D2 = 1 m S 12, 43 1 < d A (V VV 10, 12) m = d 31)
A(m = 2 + d < 28 + ite(leap((), 1,, 0)) A (V (Vee(46.0111 c +d 30)
The term leap(y) encodes the leap year condition: %4 = 0 A (y % 100 + 0 V % 400 0). Constraints 11, 22, and $3 restrict the possible values the year, the month, and the day, respectively. For example + specifies the valid range of the year, which is specific to the database engine. For example, SQLite only accepts dates between "0000-01-01" and "9999-12-31"" in which case MIN YEAR is 0 and MAX YEAR is 9999. This refined representation allows us to precisely encode a rich set of date operations and analyze more SQL queries compared to the previous encoding.
Equivalence under set semantics. SQL equivalence checkers typically support equivalence under bag semantics and list semantics. However, some Text-to-SQL evaluation platforms, such as BIRD (Li et al. 2024), by default adopt equivalence under set semanties (see equation
[. This can be expressed as an SMT constraint. Given two query results with symbolic tables Ri (I,,... (n] and
Rg [ri...., the condition that R1 and R2 are equivalent under set semantics is as follows:
m
(-Del(L) + vTt (-Del(r,) (44=)))) A A (-Del(r,) + (- Ar, = -4) (2)
j=1
On a high level, equivalence is defined by mutual set containment: R1 = Rg iff R S RS and R₂ S. RR. But since some tuples might be deleted due to WHERE clauses, we restrict set containment to non-deleted tuples, i.e., those satisfying -Del(!).
Correctness of the encodings. We now state the correctness of our symbolic encoding for the extended expressions and predicates, as well as the equivalence under set semantics. Proof of these theorems is in Appendix G As we encode the symbolic execution of queries, to prove the correctness of our approach, we need to show that our symbolic execution coincides with the concrete execution. This involves showing that given an expression E, the satisfying interpretation of E's symbolic execution result is identical to the concrete execution result of E. Thm. T that formally.
Theorem 1 (Correctness of expression encoding). Let D be a database over schema S, as be a tuple list, and E be an expression. Consider symbolic database I over S. a list of symbolic tuples T, and E's symbolic encoding [E]S.TTT. For any satisfying interpretation I with I(T)= = D A I(T = xss evaluating the expression E over the database D and the tuple list xs yields the interpretation of E's symbolic encoding
TT i.e., I(T)= = D A I(T) = 2s + [F] = I([F),,,TT).
Similarly, given a predicate o. the satisfying interpretation of é's symbolic execution result is also identical to the concrete execution result of Φ. This is formally stated in Appendix (c) Lastly, we state the correctness of our encoding for equivalence under set semanties.
5

---

validate that the counterexample database is indeed true counterexample (line Published as a conference paper at ICLR 2026
Algorithm Bounded equivalence checking
Algorithm 2 SPOTIT*
Require: Database schemn S. gold SQL query Q. generated SQL
Require: Databuse S. user query N. gold SQL query Q. Text-to-
query P. time limit hound K
framewrksss M. time limit and hound K
Ensure: A counterexample Dess
Ensure: Counterexamples Das
function EQUIYCHECK(S, for k E [1, K] do
K.
SPOTIT' (S. N.
2:
Das -0
TCS, Dees CHECKBOUND(S T.Q. if res EQUIVALENT then continue
3: for m E MM do
P m(S.N)
Generate SQL query P using Deassmm] +- BQUIYCHECK(S Q,
b. Bounded equivalence under
else if
MONN-QQIVALENT then
6
D. Performing cross-cffccnccnng counterxxamples
7:
P. Find counterexample
Validate countcresample
backend DBMS
for m E M do for E Dana Dealm] do
9:
if -EX- "E, i, Q, Dox) then return {Des}
10:
if -X (ESTTE Q. then
11:
else break Timeout, unsuppoted, undecidable queries
T1:
Dess [m]] e- Deau [m] u (P)
12:
return U
12:
return Dece
Theorem 2 (Equivalence under set semantics). Given relations Rí 11,,...; Lu] and R2 (r....., mm, if formula (2) is valid, then R2 and R2 are equivalent under set semantics.
4.2 SPOTIT: A SEARCH-BASED TEXT-TO- TOXT- EVALUATION PIPELINE
Fig. 3 presents a high-level workflow our approach that consists of three conceptual phases.
2
A+++ k-bounded equivalence verification
GENSQL
Text-D SQL
Dip
P Dees
Q
No
True CeX
Inputs:
QUERY
GOL DSQL. Q
No CEX
Yes
Verified
Spurious
Figure 3: Three main phases of SPOTIT.
① Input phase. Given NL question N and its corresponding gold SQL query Q, Text-to-SQL. framework takes as input N and generates SQL query P. Both Q and are passed to phase (
② Verification phase. The goal is to find counterexample database instance which the queries Q and P produce different outputs. For given bound k < K, we perform bounded equivalence checking between and P. If the queries are proved equivalent, then increase k by one for the next verification check. Furthermore, we cannot find any countcrexample under all bounds and conclude that they are verified up the bound On the other hand, if the queries are proved be non-equivalent under some bound, we proceed to phase 33 for a further validation of D
Validation phase. Given the queries Q and P and counterexample Deex returned by verification algorithm, we must verify that this counterexample is non-spurious. There are two main reasons spurious counterexamples can arise the verification engine. Either because some operators are over-approximated in the SMT encoding or the SQL query admits non-deterministie behaviors that cannot be modeled. Therefore, we execute the queries on the counterexample database (e-g., in SQLite) and check whether the results actually differ. Dex is viewed valid if the results remain different; otherwise, we report this spurious case to the developers.
Alg I implements the second and third phases. For given bound & < K, it first checks bounded equivalence between Q and P (line3). the queries are proven to be non-equivalent (line under some bound, and return it if this is the case. If the queries are proven to be equivalent in line 3 then we increase by one for the next verification step. If the verifier cannot find any counterexample under all bounds,

---

Published as a conference paper at ICLR 2026
A returns empty set. Finally, if the verifier times out on bound k., or the query is unsupported or undecidable, it also returns an empty set.
One observation make is that frameworks, we collect a set of counterexamples that separate the gold query from the generated queries. Hence, we realized that these counterexamples can be reused as checks across all frame- works, as they might generalize across frameworks. Alg implemenss this idea. First, it obtains counterexample databases, if they exist, for all frameworks by calling Alg ( 3 Then, iterates over all frameworks again and tests equivalence between Q and P on these counterexample databases (lines] Empirically, this improves the effectiveness of our approach.
Cross-checking counter-example
progress through the
EXPERIMENTAL EVALUATION
In this section, we investigate the effect of using SPOTIT as the evaluation methodology for Text-to-
SQL tasks. We are interested in the following questions:
How much more SQL queries does extension of VERIEQL support?
Can SPOTIT provide more rigorous accuracy evaluation than test-based approaches?
Can SPOTIT reveal shortcomings in existing Text-to-SQL evaluations?
Experimental Setup. We consider all 1,533 question-SQL pairs from the development set of BIRD (Li et al. 2023b), state-offtthe-ar dataset for evaluating Text-to-SQL methods. The questions span 11 different databases from different professional domains, such education, healthcare, and sports. The official BIRD leaderboard | contains over 80 Text-to-SQL. methods and are updated frequently. Not all methods open-source have predictions publicly available. Therefore, reached out to the developers of top-perti nop-performing Text-to-SQL. frameworks on the BIRD leaderboard and obtained the generated SQL queries for 10 of them, which constitutes a representative subset of state-of-the-an Text-to-SQL methods. The methods are listed in Tab. I
We first evaluate the predictions of each method using BIRD's 's official test- based execution accu- racy metric (EX-TEST), which, as described in
Table I: The Text-to-SQL. methods we evaluated
Entry
Acronym
Eq. [ compares the results of executing the gen- erated and gold queries on given test database. For predictions that are deemed correct by EX- TEST, we apply SPOTIT to perform a more rigor- analysis. We implemented SPOTIT top of VERIEQL (He et al. 2024), which we extended using the methods described in Sec. 4.1 To gen- erate practically relevant counterexamples, we also extend the verification condition exclude degenerate counterexamples that result in empty for one SQL and NULL for the other SQL.
Alphu SQL Qwen2 Coder 32B Li
CSC-SQI. + @0wen2.5.Crdere 7B (Sheng & Xu
20255
CSC-78
CSC-SQL + XiYanSQL (Shong
(Shnig & Xi
20250
CSC-32B
GenaSQL-1 (Donder et A125
GENA-1
GemaSQL-2 (Donder el
GENA-2
RSI. GPT (
2012
RSI.
OmmniSQL332B(L1i)
A0250)
OMNI-MAJ
GSR (anonymous authirs)
GSR
CHESS Talaci et al 2024a
CHESS
SLM-SQL Qwwen..5Cooos--.. Stxce & & Xu
2025c
SLM
We consider three variants of SPOTIT: (i) SPOTIT: Alg. 2 instantiated with the extended verification
instantiated with vanilla VERIEQL and without cross-checking: (iit) SPOTIT* Alg. 2 with cress-nhecking. We verify each generated-gole SQL pair up to bound (K) of 5. Each verifier call is given one physical core, 8GB memory, and a CPU timeout of 600 seconds. In practice, a counterexample can typically be found within seconds, as reported below. Experiments were performed on cluster equipped with Dell PowerEdge R6525 CPU servers featuring 2.6-HHz AMD CPU cores.
engine but without cross-checking (lines 7 ; (ii) SPOTIT Alg. 2
Performance of Verification Engine. We first evaluate the effect of our extensions to the original VERIEQL engine (He et al. 2024) in terms of coverage, defined as the fraction of generated- -oodd- SQL pairs that can be encoded into SMT query. In addition, we measure the average runtime of SPOTIT on questions where a valid differentiating database is found. The results are shown in Tab. 2 Our extensions significantly increase the coverage of the verification engine relevant questions (i.e., ones deemed correct by EX-TEST) for each method, allowing us to formally analyze a larger number of generated SQL queries. For example, for CSC-32B, the coverage increases from 84.83% to 94.88% which corresponds to 110 additional supported questions (94.88% -4.83%) 1094).
https: http://bbidbbbech..ho thub. 10/
7

---

Published as a conference paper at ICLR 2026
Table 2: % of SQL pairs supported by SPOTIT' and SPOTIT. For SPOTIT, also the average time in seconds on pairs where CEXs are found by the verifier and how many them are non-spurious.
Table Performance of Text-to-SSQ methods using EX-TEST, EX-SPOTIT, and EX-SPOTIT on the 1533 BIRD-dev benchmarks.
EX TEST
EX SPorTT
EX SporTr'
Method (# quest.) SPOTIT (%) SPOTIT (5% Avg. Time Valid, (%)
Acc. (%)
Rank
Acc.
Rank
Acc.(S)
Rank
ALPHA (1064)
84,87
93.89
3.10
96.15
CSC-32B
71.32
$8.80
57.82
4
CHESS (976)
87.40
97.13
GENA-2
CSC-32u (1094)
84.83
94.88
3.24
94.46
ALPIIA
69.36
55.87
55.02
CSC-7B (1061)
85.77
96.14
3.93
95.10
GENA-1
69.23
59.45
59.00
GENA-1 (1062)
84.56
94.92
1.11
94.52
CSC-78
69.17
58.54
57.95
GENA-2 (1082)
84.47
94.55
0.93
95.42
RSI.
67.67
56.58
55.80
(1020)
84.51
93.63
54.69
54.04
OMNI-MAU (1026)
86.65
95.61
1.36
95.83
GSR
66.49
54.56
53.72
8
(1038)
86.03
95.18
52.87
SLM (973)
85,92
94.24
1.36
95.05
SLM
63.43
51.37
50.98
10
The average time taken by SPOTIT to find counterexample is under seconds for all methods, which, combined with the fact that the analysis for each question can be done in parallel, confirms that SPOTIT is already a practical method for formally comparing generated SQLs with gold SQLs. Moreover, a high percentage (up 96.15% of the counterexamples found by the verifier are successfully validated, which suggests that our SMT encoding is sufficiently precise in practice.
Comparing test-based evaluation with SPOTIT. We now evaluate the accuracy of each Text-to-SQL method based on EX-TEST, EX- OX-SPOTIT, and EX-SPOTIT" As shown in Tab. 3 the accuracy of each method drops significantly when SPOTIT is used check query equivalence. For example, the accuracy of CSC-32B drops from 71.32% to 58. 80% with SPOTIT, and further to 57.82% when cross- checking enabled. This means that there are 207 generated SQLs (1533 (71.32% - 57.82%) that passed the test the official test databases, but were differentiated from the gold SQL by SPOTIT. Overall, SPOTIT resulted a decrease in accuracy ranging from 9.8% to 13.5%, and cross-checking results in small further decrease, by up to 1%. Interestingly, the ranking of the Text-to-SQU methods also changes substantially when evaluated under the more stringent, perification-bases metrics, particularly in the top half of the table. For example, CSC-32B, which is ranked 1st by the official test-based metric, drops to 4th place when evaluated by SPOTIT* And the 3rd place method ALPIIA drops to the 6th place. These results indicate that test-based methods in many cases overlook differences between the generated SQL and the gold SQL, which might lead to misrepresentation of the actual performance (both absolute and relative) existing Text-to-SQU methods.
The effect of K. To study the effect of the choice of the verification bound K, we vary its value from 1 to 7 and run SPOTIT IT on the predictions of CSC-32B, the best model according to EX-TEST. As shown in Fig. 4 SPOTIT was able to find significantly more differentiating databases when K increases from to 2 and the gain is marginal pass K 3. This justifies our choice of K 5.
70
E30eet (71.39%)
Accuracy (56)
64.4%
59. 45%
60
59.00%
81%.
58 80%
58 58.60%
58 58.60%
Bound
Figure 4: The effect of bound K.
Manual inspection of SPOTIT counterexamples. As SPOTIT performs bounded verification, the differentiating databases it finds guaranteed to be minimal, which makes it easy to an- alyze them and understand the source of difference between the generated and gold SQLs. We manually examined the coun- terexamples for a random sample of 50 queries generated by csc-32B and found that the difference between a generated SQL and a gold SQL can be primarily attributed to the three reasons that we described in Section 3 ambiguous question, incorrect gold SQL, and incorrect generated SQL. Fig. shows a breakdown of the primary attributed reasons for those sampled questions. Surprisingly, while incorrect predictions do constitute a significant portion (26%). more often than not, the gold SQL itself is problematic. There are also a small fraction of cases (10%) where the question itself can be interpreted multiple ways and therefore admits different answers. We discussed two
Incorrect prediction 26.0%
Ambiguous
question 10.0%
Incorrect gold 61.0%
Figure 5: A breakdown of the pri- mary reason for the difference be- tween generated and gold SQLs.
8

---

Published as a conference paper at ICLR 2026
examples of incorrect gold SQLs and ambiguous questions in Fig. Additional examples of each type of issues, along with the databases found by SPOTIT, are provided and discussed in App. D
Additional analysis Spider 2.0 benchmarks.
To assess the generalizability of SPOTIT to more
Table Evaluation of SPOTIT on Spider 2.0.
complex Text-to-SQL. tasks, we evaluate it the
recently introduced Spider 2.0 benchmark (Lei al. 2024). We consider OMNISQL (Li et al.] 2025b), state-of-the-art Text-to-SQL method and GPT-5 on the 135 SQLite questions. These methods pass EX-TEST on 46 and 57 queries, re- spectively, which is competitive with the top entries on the Spider 2.0 leaderboard As shown in Tab. 4 SPOTIT finds differentiating databases for 16 ((34.1% 22.2%) * 135) and 8 query pairs deemed correct by test-based evaluation respectively for OMNISQL. and GPT-5. Spotlt's runtime for finding counterexamples remains low. We believe this is due to the fact that the schemas in Spider 2.0 are only moderately larger than those in BIRD (97.6 vs. 78.6 columns) and counter-examples can usually be detected with small values of K. The main verification challenge when it comes to Spider 2.0 lies in the number of SQL operators required for the queries but currently unsupported by our verification engine, which resulted in a smaller percentage of supported query pairs. Upon closer examination, 52.6% of the unsupported Spider 2.0 queries involve the window function (i.e., OVER clauses). Overall, these results indicate that SPOTIT is also useful for uncovering query discrepancies overlooked by test-based methods on the challenging Spider 2.0 benchmarks.
EX-TEST
EX-SporTr
Aec,(%)
Acc.(S)
Supported (55 Avg. Time
OMNISQL
34.1
22.2
60.9%
3.4
GPT-5
42.2
36.3
50.9%
Summary of findings and implications. We now summarize the findings of our evaluation of state-of-the-art Text-to-SLL evaluation dataset BIRD using SPOTIT and discuss their implications.
Finding 1: Existing test-based correctness metrics that involve executing the generated SQL and the
gold SQL on static test databases can overlook significant variations in output data returned by the generated and gold SQLs. gearch-based evaluation metrie, such as SPOTIT, can serve as a practical alternative that provides additional perspectives on the performance of TeXt-to-SQL. methods.
Finding 2: there is a significant number of problematic gold SQLs in existing Text-to-SQL. benchmark sets. As shown by examples in Tab. Lab.[aan and App. D in many cases, the issue can be hard to detect, yet can cause significantly different behaviors from the intended one. The presence of incorrect gold SQLs makes it hard to determine the true optimal performance on benchmark set, even a perfect Text-to-SQL method cannot achieve 100% accuracy.
Based our result analysis for CSC-32B, speculate that when most Text-to-SQL methods disagree with the gold SQL, the gold SQL is likely problematic. To validate this, we count the number of times that a prediction for a question is deemed correct by EX-TEST but incorrect by SPOTIT* across all 10 Text-to-SQL methods. As shown in Fig. 6 there are 36 questions on which all methods generated queries that differ from the gold SQL. Manual inspection suggests that 31 of those 36 cases have problematic gold SQLs, have ambiguous questions, and only 2 represent genuine errors in the generated SQLs.
150
145
# questions
100
54
50
38
31
27
28
7 # Text-to-SQL methods
Figure 6: A breakdown of ques- tions that passed EX-TEST but failed SPOTIT*
While so far we have focused on incorrect gold SQLs overlooked by EX-TEST, our investigation begs the question: when the gen- erated query differs from the gold SQL, how often in general is the gold SQL problematic? Fig. 7 shows the number of times the prediction for question is deemed incorrect by EX-TEST across the 10 Text-to-SQL methods, for questions where CSC-32B's 's pre- dictions failed EX-TEST. There are 294 questions where at least 8 of the other 9 methods also failed EX-TEST. If shared disagree- ment with gold SQL is also a good indicator for problematic gold SQL in this case, then even perfect Text-to-SQL method might
250
231
questions
200
150
100
63
# 50
36
37
2
11
2 3
7
10
# Text-to-SQL methods
Figure 7: A breakdown of ques- tions for which CSC-32B's pre- dictions failed EX-TEST.
We use the same prompt as used in OMNISQI.. 3 https://spider22sp httpiddr--sggggiuubi..... github.io/. We were not ahle to ohtain predictions of Text-to-SQI. methods on the leaderboard because they are predominantly closed source.

---

Published as a conference paper at ICLR 2026
not be able to achieve an EX-TEST score much higher than 80% on BIRD-dev. As the time of completing this manuscript, the best EX-TEST score for BIRD-dev achieved by any method on the official leaderboard is 76.14%.
Large-scale benchmark sets inevitably contain problematic gold SQLs. Indeed, multiple sources have found examples of problematic gold SQLs in the BIRD dataset (Hui 2024 Wretblad al. 2024). and some of them have already been addressed by the maintainers. SPOTIT is the first approach that can provide minimal, easily analyzable databases to differentiate generated and gold SQLs, and can help to systematically uncover problematic gold SQLs.
Finding 3: A substanfial number of questions in the Text-to-SQI. dataset can be interpreted in different ways, thus admitting different SQL queries. While ambiguity is inherent in natural language, judging the correctness of a generated SQL query based on a single gold SQL query when the natural language question admits multiple interpretations might result in unfair penalization of Text-to-SQL. methods.
Finding (for the verification community)): SMT-based equivalence verification techniques can already support large fraction of practical SQL queries. Our results demonstrate that verification can often be completed within seconds. Due to the practical relevance of Text-to-SQL, we believe there is motivation for the verification community to invest more resources to precisely cover larger fragment of SQL.. In App. [ we discuss further extensions that would be especially useful according to our evaluation. Another significant next step incorporate user preferences (potentially from natural languages) to search for particular types of counterexample databases. One way to achieve this is to encode the preferences additional constraints in the SMT formulation of the verification problem.
6 RELATED WORK
Popular evaluation platforms such as BIRD-SQL eLi al. 2024) and Spider 2.0 (Lei et al. 2024)
evaluate query correctness by testing on predefined database instances. Several additional evaluations
have been proposed to take into account partially correct generated queries (Pinna et al. 2025).
efficiency of query executions (Zhang et al.) 2024). and ambiguity in the questions (Li et al. 2023a
BIRD 2025). However, the final correctness check is still via testing on static database. Formal
SQL equivalence checking broadly falls into two categories, full-fiedged verification (Chu al.
2017c 2018: Zhou et al., 2022, 2024 Wang et al. 2024) and bounded verification (Veanes et al. 2010 Chu et 20. bj He et al. 2024). To the best of our knowledge, VERIEQL (He al. 2024) supports the most expressive SQL fragments, while also offering extensibility for new features. We significantly extend the VERIEQL framework to support date and string types as well as a number of common operators for the Text-to-SQL. evaluation task. Test data generation methods can also be useful for detecting query non-equivalence (Chandra et al. 2015 Somwase et al.. 2024 Zhong et al. 2020).H However, when the countercxamples require very specific structures, random fuzzing/testing can become unreliable in refuting equivalence. In contrast, SPOTIT systematically searches over the space of possible differentiating databases, finds minimal counter-examples, and provides formal guarantee: if SPOTIT deems two SQL queries equivalent, then no counterexample of size less than a fixed number exists. more detailed review of related work can be found in App.
7 CONCLUSION
We presented SPOTIT, the first verification-based evaluation pipeline for Text-to-SQL. We introduced techniques to support a richer SQL grammar, which enabled us to efficiently analyze a large fragment of SQL queries commonly seen in Text-to-SQL tasks. Our initial motivation for developing SPOTIT was to examine the extent to which the accuracy of a Text-to-SQL method is overestimated by test-based evaluation, which is widely adopted as the default metric on high-profile Text-to-SQL. evaluation platforms. However, a closer inspection of the verification results revealed far more complex picture. While SPOTIT can indeed detect incorrect generated SQL queries that were overlooked by test-based methods, significant portion of the inconsistency between the gold and generated SQLs can be explained by the benchmarks themselves either due to problematic gold SQLs or due to ambiguous natural language questions. We discussed the implications of and the next steps from our findings, and hope that our work will motivate further work on evaluating and improving Text-to-SQI. evaluation frameworks.
10

---

Published as a conference paper at ICLR 2026
REFERENCES
Amazon. Build a text-to-sql solution for data consistency in generative ai using amazon nova.
2025. URL hatpap/ww......aa.a...//aa/aaaaa
usiiig amazon novan
Amazon Web Services. How msd uses amazon bedrock to translate natural language into sql for learnin 3/Deaaattttsssssaeaaaaaaaatooooa
http:///ww...aaoooooooooooooooaa nto ottoo-ss---o--.ccoocccceealalla-
2024. Accessed: 2025-09-21.
Clark Barrett and Cesare Tinelli. Satisfiability modulo theories. In Handbook of model checking, pp.
305-343. Springer, 2018.
Team BIRD. Bird-interact: Re-imagine text-to-sql evaluation via lens of dynamic interactions. http://ttthbb.ooomm/iideeeeee/h/
2025. Accessed: 2025-06-01.
Team BitsAI. Bits ai:scale your teams with autonomous ai agents across monitoring, development, and security, September 2025. URL
rm. rm/bitt aii
Zhenbiao Cao, Yuanlei Zheng, Zhihao Fan, Xiaojin Zhang, Wei Chen, and Xiang Bai. Rsl-sql: Robust schema linking in text-to-sql generation. arXiv preprint arXiv:2411.0007. 2024.
Bikash Chandra, Bhupesh Chawda, Biplab Kar, KV Maheshwara Reddy, Shetal Shah, and S Sudar- shan. Data generation for testing and grading sql queries. The VLDB Journal, 24(6):731-755, 2015.
Shuaichen Chang and Eric Fosler-Lussier. How to prompt iims for text-to-sql: A study in zero-shot, single-domain, and cross-domain settings. arXiv preprint arXiv:2305. 1853, 2023.
Shumo Chu, Daniel Li, Chenglong Wang, Alvin Cheung, and Dan Suciu. Demonstration of the cosette automated sql prover. In Proceedings of the 2017 ACM International Conference on Management of Data, pp. 1591-1594, 2017a.
Shumo Chu, Chenglong Wang. Konstantin Weitz, and Alvin Cheung. Cosette: automated prover for sql. In CIDR, pp. 1-7, 2017b.
Shumo Chu, Konstantin Weitz, Alvin Cheung, and Dan Suciu. Hottsql: Proving query rewrites with univalent sql semantics. Acm sigplan notices, 52(6):510 10-524,, 2017c
Shumo Chu, Brendan Murphy, Jared Roesch, Alvin Cheung, and Dan Sueiu. Axiomatic foundations and algorithms for deciding semantic equivalences of sql queries. arXiv preprint arXiv: DXXXvv/882.00299 2018.
Leonardo De Moura and Nikolaj Bjørner. Z3:
An efficient smt solver. In International conference on Tools and Algorithums for the Construction and Analysis Systems, pp. 337-340. Springer, 2008.
Yusuf Denizay Dönder, Derek Hommel, Andrea W Wen- Yi, David Mimno, and Unso Eun Seo Jo. Cheaper, better, faster, stronger: Robust text-to-sql without chain-of-thought or fine-tuning. arXiv preprint Xix: 2025.
Xuemei Dong, Chao Zhang, Yuhang Ge, Yuren Mao, Yunjun Gao, lu Chen, Jinshu Lin, and Dongfang Lou. C3: Zero-shot text-to-sql with chatgpt, 2023.
Yingqi Gao, Yifu Liu, Xiaoxia Li, Xiaorong Shi, Yin Zhu, Yiming Wang, Shiqi Li, Wei Li, Yuntao Hong, Zhiling Luo, Jinyang Gao, Liyu Mou, and Yu Li. A preview of xiyan-sql: A multi-generator ensemble framework for text-to-sql, 2025. URL /ttpps//aaxxiv.or///a...s
08599
Yang He, Pinhan Zhao, Xinyu Wang, and Yuepeng Wang. Verieql: Bounded equivalence verification for complex sqi queries with integrity constraints. Proc. ACM Program. Lang ((OPSLL)) April 2024. doi: 10.1 145/3649849. URI.https: /tt::://doo..oo http://tooo/....//////o 0ttp//10..11///4449999
11

---

Published as a conference paper at ICLR 2026
Binyuan Hui. Panel of BIRD Annotation Issues. MAMMO-CCnnAI/Lsuueese.
2024. Accessed: May 2024.
Fangyu Lei, Jixuan Chen, Yuxiao Ye, Ruisheng Cao, Dongchan Shin, Hongjin Su, Zhaoqing Suo, Hongcheng Gao, Wenjing Hu, Pengcheng Yin, et al. Spider 2.0: Evaluating language models on real-world enterprise text-to-sql workflows. arXiv preprint urXiv:2411.07760 2024.
Boyan Li, Jiayi Zhang, Ju Fan, Yanwei Xu, Chong Chen, Nan Tang, and Yuyu Luo. Alpha-sql: Zero-shot text-to-sql using monte carlo tree search, arXiv preprint arXiv:2502.17248, 2025a.
Haoyang Li. Shang Wu, Xiaokang Zhang, Xinmei Huang. Jing Zhang, Fuxin Jiang. Shuai Wang. Tieying Zhang, Jianjun Chen, Rui Shi, et al. Omnisql: Synthesizing high-quality text-to-sql data at scale. arXiv preprint arXiv:2503.00 022400, 2025b.
Jinyang Li. Binyuan Hui, Ge Qu, Binhua Li, Jiaxi Yang, Bowen Li, Bailin Wang, Bowen Qin, Rongyu Cao, Ruiying Geng, Nan Huo, Xuanhe Zhou, Chenhao Ma, Guoliang Li, Kevin Chen-Chuan Chang, Fei Huang, Reynold Cheng, and Yongbin Li. Can L.M already serve as A database interface? A big bench for lcage-scale database grounded text-to-sqls. CoRR, abs/2305.03111 2023a. doi: 10.48550/ARXIV. 11.10. URL http:::ttt///cct.. /dosi: /tg/10.......oooooooo 48550/ 305. 03111
Jinyang Li, Binyuan Hui, Ge Qu, Jiaxi Yang, Binhua Li, Bowen Li, Bailin Wang, Bowen Qin, Ruiying Geng, Nan Huo, et al. Can Ilm already serve as a database interface? a big bench for large-scale database grounded text-to-sqls. Advances in Neural Information Processing Systems, 36:42330-42357, 2023b.
Jinyang Li, Binyuan Hui, Ge Qu, Binhua Li, Jiaxi Yang, Bowen Li, Bailin Wang, Bowen Qin, Rongyu Cao, Ruiying Geng, Nan Huo, Xuanhe Zhou, Chenhao Ma, Guoliang Li, Kevin Chen-Chuan Chang, Fei Huang, Reynold Cheng, and Yongbin Li. BIRD SQ. hub. 1o/ 2024. Accessed: Sep 2025.
https: /ttp://biiedeeeeeee git
Aiwei Liu, Xuming Hu, Lijie Wen, and Philip S. Yu. A comprehensive evaluation of chatgpt's zero-shot text-to-sql capability, 2023.
Yifu Liu, Yin Zhu, Yingqi Gao, Zhiling Luo, Xiaoxia Li, Xiaorong Shi, Yuntao Hong, Jinyang Gao, Yu Li, Bolin Ding, and Jingren Zhou. Xiyan-sql: novel multi-generator framework for text-to-sql, 2025. URL utLpttss: /ttttp::/arxxv..oo wrg./orgggao....o hbtp://ab//25027 04701
Mudathir Mohamed, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. Verifying sql queries using theories of tables and relations. In Proceedings of 25th Conference on Logic for Pro, volume 100, pp. 445 463, 2024.
Giovanni Pinna, Yuriy Perezhohin, Luca Manzoni, Mauro Castelli, and Andrea De Lorenzo. Redefin- ing text-to-sql metrics by incorporating semantic and structural similarity. Scientific Reports, 15, July 2025. ISSN 2045-2322. doi: 10.1038/s4 0013///41599-25--0000 598-025-04899-9.
Juan Sequeda, Dean Allemang, and Bryon Jacob. A benchmark to understand the role of knowledge graphs on large language model's accuracy for question answering on enterprise sql databases, 2023.
Lei Sheng and Shuai-Shuai Xu. Cse-sql: Corrective self-consistency in text-to-sql via reinforcement learning. arXiv preprint arXiv:2505. 13271, 2025a.
Lei Sheng and Shuai-Shuai Xu. Csc-sql: Corrective seffrooiieyss in text-to-sql via reinforcement learning, 2025b. URL http::ss///aaai..oor///////....0
Lei Sheng and Shuai-Shuai Xu. SIm-sql: An exploration of small language models for text-to-sql. arXiv preprint arXiv 2025c.
Liang Shi, Zhengju Tang, Nan Zhang, Xiaotong Zhang, and Zhi Yang. A survey employing large language models for text-to-sql tasks. ACM Computing Surveys, 2024.
Vladislav Shkapenyuk, Divesh Srivastava, Theodore Johnson, and Parisa Ghane, Automatic metadata extraction for text-to-sql, 2025. Utt.:ttpess//ax....oog/ab//////p 19988999..119188
12

---

Published as a conference paper at ICLR 2026
Sunanda Somwase, Parismita Das, and S Sudarshan. Data generation for testing complex queries. arXiv preprint arXiv:2409.18821 2024.
Splunk. Ai assistant in observability cloud, September 2025. en Ven_use www.uss/ppss.//eeoo.. spttissssplukke spwunk-lukkk.....p ai assistare in- observabiliyyy.ooouu.. html
com com
Shayan Talaei, Mohammadreza Pourreza, Yu-Chen Chang, Azalia Mirhoseini, and Amin Saberi.
Chess: Contextual harnessing for efficient sql synthesis. arXiv preprint arXiv:2405.16755 /6755, 2024a.
Shayan Talaci, Mohammadreza Pourreza, Yu-Chen Chang, Azalia Mirhoseini, and Amin Saberi. Chess: Contextual harnessing for efficient sql synthesis, 2024b. URL URLattps://cxxiv.orr
TiDBCloud. Get Started with Char2Query API. https: httpss:/docs: wwt.::ppnnnnccnciaaaooooooo
/use-chat api 2020. Accessed: May 2024.
Margus Veanes, Nikolai Tillmann, and Jonathan De Halleux. Qex: Symbolic sql query explorer. In
International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp- 425 446. Springer, 2010.
Shuxian Wang, Sicheng Pan, and Alvin Cheung. Qed: A powerful query equivalence decider for sql. Proceedings of the VLDB Endowment,
-3114, 2024.
Niklas Wretblad, Fredrik Gordh Riseby, Rahul Biswas, Amin Ahmadi, and Oskar Holmström. Understanding the effects of noise in text-to-sql: An examination of the bird-bench benchmark, 2024.
Bohan Zhai, Canwen Xu, Yuxiong He, and Zhewei Yao. Excot: Optimizing reasoning for text-to-sql with execution feedback, 2025.
http///aiiii.rrra////////0////00 19988
Bin Zhang. Yuxiao Ye, Guoqing Du, Xiaoru Hu, Zhishuai Li, Sun Yang. Chi Harold Liu, Rui Zhao, Ziyue Li, and Hangyu Mao. Benchmarking the text-to-sql capability of large language models: A comprehensive evaluation, 2024. URL
a24p:/33.a///// 2403. 02951
Ruiqi Zhong, Tao Yu, and Dan Klein. Semantic evaluation for text-to-sql with distilled test suites. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pp. 396-411, 2020.
Aojun Zhou, Ke Wang. Zimu Lu, Weikang Shi, Sichun Luo, Zipeng Qin, Shaoqing Lu, Anya Jia, Linqi Song, Mingjie Zhan, and Hongsheng Li. Solving challenging math word problems using GPT-4 code interpreter with code-based self-verification. In The Twelfth International Conference on Learning Representations, 2024. URL
Ms4Av0
Qi Zhou, Joy Arulraj, Shamkant B Navathe, William Harris, and Jinpeng Wu. Spes: A symbolic approach to proving query equivalence under bag semantics. In 2022 IEEE 38th International Conference on Data Engineering (ICDE), pp. 2735-2748. IEEE, 2022.
13

---

Published as a conference paper at ICLR 2026
A
RELATED WORK
large number of Text-to-SQL frameworks have been proposed over the last few years by research
groups in academia and industry (Liu 2023 Dong et 2023 Chang Losser-Lussier 2023
TiDBCloud] 2020 Talaci et al. 2024b Gao el al. 2025 Sequeda et 2023] Sheng & Xu 2025b
etu 2025 Shkapenyuk et al. 2025 Zhai et al. 2025). However, evaluation frameworks have
received much less attention. There are two main publicly available platforms: BIRD-SQU (Li et al.)
2024) and Spider (Lei et al. 2024) that are commonly used to evaluate the performance Text-to- methods. Their evaluation procedure is performed on predefined database instances, whereas SPOTIT searches for separation datahase instance. A number of evaluation metrics were proposed to take into account partially correct generated queries (Pinna et al. 2025) the efficiency of query executions (Zhang et al., 2024). Recently, (Li ct al. 2023a| BIRD 2025) proposed an iterative evaluation framework in which the system can interact with the user by asking additional questions (e.g., to resolve ambiguity). However, the final evaluation of the correctness of the generated SQL query is still performed on static database.
There are two lines of work in formal equivalence checking for SQL queries: full-fledged and bounded verification. The full-fledged methods (Chu et al., 2017c| 2018 Zhou et al. 2022 2024
Wang et al. 2024) encode queries into specific representations (e.g., algebraic expressions (Chu al. 2018 Wang et al. 2024)) and determine equivalence by proving the equivalence of these representations, thereby guaranteeing equivalence of queries for any possible database. However, such methods typically support only a limited subset of SQL and cannot generate counterexamples for non-equivalent queries. In contrast, the bounded verification approaches (Veanes et al.) [2010] Chu jet al. [01 b. He et al. 2024) check equivalence within finite search space, making them capable of handling larger subsets of SQL and identifying counterexamples. To the best of our knowledge, VERIEQL supports the most expressive SQL fragments and rich integrity constraints, while also offering extensibility for new features (He et al.) 2024). In this work, we significantly extend the VERIEQL framework to support date and string types as well as number of common operators for the Text-to-SQL evaluation task.
Test data generation methods can also be useful for detecting query non-equivalence (Chandra et al. 2015 Somwase et al. 2024 Zhong et al., (1120)Howevee when the counterexamples require very specific structures (which is the case for many query pairs that passed EX-test but failed SpotIt as seen in App. D), random fuzzing/testing can become unreliable in refuting equivalence. In contrast, SPOTIT systematically searches over the space of possible differentiating databases, finds minimal counter-examples, and provides formal guarantee: if two SQL queries are considered equivalent, then no counterexample of size less than a fixed number exists. Computational resources permitted, one could in principle run a portfolio of test-based and verification- based equivalence-checkie methods in parallel to more quickly detect non-equivalence. This is an orthogonal but interesting future direction.
14

---

Published as a conference paper at ICLR 2026
B ANALYSIS OF RUNTIME
Tables 5
g and 9 show the effect of different parameters on runtime, including the number of columns, integrity constraints, tables in the databases, the number of sub-queries in the gold SQL, and the number of nodes in the abstract syntax tree in the gold SQL. We found that all parameters except for the number of tables are positively correlated with median runtime.
#columns
Median runtime (s)
11
0.4310
21
0.1701
31
0. 0.1963
48
0,3887
55
0,5576
64
0.3007
71
0.5365
89
0.2672
94
0.3154
115
0.6537
199
0,8006
Table Median runtime by number of columns
#constraints
Median runtime (s)
5
0.2842
7
0.1701
10
0.4324
16
0.5576
17
0.3887
19
0.1963
21
0.5365
36
0.6877
Table 6: Median runtime by number of constraints
#tables
Median runtime (s)
3
0.2842
4
0.4310
5
0.1701
6
0.6537
7
0.8006
8
0.4249
10
0.1963
13
0.3154
Table 7: Median runtime by number of tables
#subqueries
Median runtime (s)
0
0.3676
1
0.3972
2
1,9128
Table 8: Median runtime by number of subqueries
15

---

Published as a conference paper at ICLR 2026
#AST nodes
Median runtime (s)
0-19
0.1812
20-39
0.3408
40-59
0.3426
60-79
0,4216
80-99
0,9683
100-119
1.1865
139
0.2053
140-159
1.2395
Table 9: Median runtime by number of AST nodes (buckets of 20)
C LIMITATIONS OF EXISTING BOUNDED SQL EQUIVALENCE CHECKER
While SPOTIT builds on top of and extends VERIEQL, a state-of-the-arr bounded verifier that claims to cover the largest SQL fragment, find that there still SQL operators which it either does not support or cannot precisely capture. In this section, we describe the features that appear frequently in failure cases of SPOTIT.
The gold query for question 726 in the BIRD-dev benchmark.
SELECT superhero_ name,, height _cm, RANK() OVER (ORDER BY height.cm DESC) AS HeightRank FROM superhero INNER JOIN publisher
ON WHERE publisher. publisher publisee name = "Marvel Comics"
id publisher.id
SPOTIT does not support the window and analytic functions such as RANK and LAG.
A SQL query generated by OMNISQL.
WITH RECURSIVE TimeSeries (
SELECT 20116-0-01' AS mth UNION ALL SELECT DATE(mth, '+1 month') AS mth FROM TimeSeries WHERE mth "2017-12-01'
SELECT product_name FROM SalesRatio ORDER BY product_name
SPOTIT cannot encode recursive common table expressions above.
Imprecisely encoding for ORDER BY and LIMIT:
Since VERIEQL establishs tables under bag semantics (namely, multi-set), database in- stances are considered equivalent they has the same tuples with the same multiplicities. For instance, Ti and T, in Tables 11 equivalent under bag semanties.
However, when VERIEQL symbolically execute ORDER BY A, VERIEQL automatically converts semantics from bag to list in which the order of tuples matters. In such case, database instances is equivalent iff they are tuple-wise the same. For instance, Ti and T2 in Tables TOL11 are not equivalent under list semantics. Furthermore, if ORDER BY is followed by LIMIT 1, then execution results on Ti and Tp are, respectively, Ri and Rg.
Table 10: Ti
Table 11: T2
Ra
More concretely, consider the gold query Q1 of question 653 in the BIRD-dev benchmark. a query Q2 generated by ALPHA, and a counterexample database found by VERIEQL as follows:
16

---

Published as a conference paper at ICLR 2026
The gold query Q1:
SELECT DisplayName FROM users WHERE id =
SELECT OwnerUserld FROM posts ORDER BY ViewCount DESC LIMIT
The generated query Q2:
SELECT u.displayname AS ownerdisplayname
FROM posts AS p INNER JOIN users AS u ON p.owneruserid = u.id
ORDER BY p.viewcount DESC LIMIT
Table 12: posts
Table 13: users
ViCMCOurE
ommaruserid
id di dipplayamm Y
Null
Mul1
VERIEQL'S execution results of Q1 and Q2 are shown in Tables 14
Table 14: VERTEQL'S result of Q Table 15: VER TEQL's s result of Q2
DiepLayName
ownerdisplayname
'>/
SQLite's execution results of Q1 and Q2 are shown in Tables 16
Table 16: SQLite's s result of Q
Table 17: SQLite's s result of Q2
DisplayName
ovmerdisplayname
'x'
Naturally, VERIEQL identifies spurious counterexample where Q result is 'B' instead of 'A'. This is because the intermediate table from the FROM clause of Q2 is shown as Table 18 where the values column "viewcount" are Null values. While executing the ORDER BY, VERIEQL does not reorder the tuples of this intermediate table but SQLite engine will swap these two tuples. Therefore, VERIEQL failed in this verification task.
Table 18: VERIEQL'S 's intermediate table of Q2
u. Displaytame p. p.viewcount
Null
17

---

Published as a conference paper at ICLR 2026
D ADDITIONAL INCONSISTENCY BETWEEN PREDICTED AND GOLD SQLS OVERLOOKED BY EX-TEST
D.1 EXAMPLE 3.1 (EXTENDED)
Tables 19 show a counterexample database Deex (these are two relevant tables). The generated SQL returns no records, since laboratory rnр is equal '+-" in the single record that violated NOT laboratt laboratory. rmp IN (' (+-"). ). In contrast, the gold SQL Q returns '1000-01-01,, because the condition T2. rnp != r-r OR ++- incorrect.
Table 19: patient
16
sex bf otrtoyy
description
date admisaion diagnesis
1
CD0-01-01
11000001-11 11008-01-814 "1'
Table 20: laboratory (skipped irrelevant columns)
date
got
gpt
1dh
RNP
11000-01-02"
D.2
EXAMPLE 3.2 (EXTENDED)
Tables 21
22 show counterexample database Deex (these are two relevant tables).
The generated SQL P counts two records while the gold SQL Q counts only one record, because the DISTINCT operator is applied before counting.
Table 21: exami na nation in (skipped irrelevant columns)
1d avamination.dat
aol.igg acl.igm
ana.pattern aclliga diagnosis
ket
1ac
11000-01-01'
11
"1'
3
'1'
"
'1'
'1'
<1000 01 01"
14
'1'
0
'
"1'
'1'
'1'
Table 22: patient
sex
birthday
description
first.dete
admission diagnosis
'1'
'1000-01-01'
11000-01-01'
"1000-01-01"
(1'
"1000-01-01'
11000-01-01'
11000-01-014
<1'
18

---

Published as a conference paper at ICLR 2026
D.3 ADDITIONAL EXAMPLES
Example D.I. Consider the question N3, and the corresponding SQL queries (Figure S The differentiating database found by SPOTIT shown in Tables 23 24 25 Note that there is typo in the evidence. According to external medical sources, the normal range of uric acid levels in females should be defined as less than or equal to 6.50, not greater than. The annotator overlooked this rypo. and as result, the gold SQL is clearly incorrect.
Na: "What the anti Cardiolipin antibody concentration of the jemale patient highest
level Evidence: "Anti Cardooliia antibody concentation refers to 'aCL lgG 'oCL. IgM", 'aCI. IgA';
nange?"
female pattent refers Sex F"; highest uric acid level normal ronge refers MAXI UA >> 6,50).
3+Gold SOL Q-/:
SELECT 13.acl_igg, 13.ecl_igm, 13.scl_gga
patient
INNER JOIN lsboratory AS 12 ON T1.id - 12.id
LNNER examination AS 13.id
WHERE T1.sex 'F' AND 72.ua 6.3
URDER BY 12.ua DESC
T.MTT
/+Generazed SQL P+/:
SELECT aciiin exominazion.aci.ine examination.acl acl_iig
FROM pet
LANER JO1N lsboratory UN patient. id lsboratory.id
INNER examination ON patient.id examination.
WHERE patient. sax 's" AND laboratery.ua <= 6.5
ORDER BY laboratory.ue DESC
LIMIT
Figure 8: An example of query with an incorrect gold SQL.
Table 23: patient (skipped irrelevant columns)
1d
sex
Table 24: laboratory (skipped irrelevant columns)
ua
6.5
Table 25: examination (skipped irrelevant columns)
scl.igg acl.igm
acl.iga
19

---

Published as a conference paper at ICLR 2026
Example D.2. Consider the question N₂ and the corresponding SQL queries (Figure 91. The differentiating database found by SPOTIT shown in Tables 26 The natural langue question asks for transactions after Jamuary 1st, 2012, which requires excluding January 1st, 2012. However, the gold SQL. uses a greater-than-or-equual-- condition, which includes 2012/01/01,, thus being incorrect.
N4. "Among transactions made ges stations in the Czech Republic, how many took place after 2012/1/17" Evidence: "Country code for Czech Republic 'C7F.""
/+Gold SQL Q-/:
SELECT COUNT Lraneactiionndd
EROM
transactions_lk AS 11
JUIN gosstations
11.gasstationid 12.gasstationid
KHERE country CZE" AND STRPTINE T1.date) 2 '2022'
/+Generated sQ1, P-/:
SE13CT (x)
FROM transactions_ik AS
INNER JOIN gasstations AS 6 ON T.gasstationid G.gaastationid
WHERE 6.country
reee' T. dadete "2012-01-01"
Figure 9: An example of a query with an incorrect gold SQL..
Table 26: transactions.1k (skipped irrelevant columns)
tramsaction.id
gasstation.id
date
20122011011
Table 27: gasstations (skipped inreeevnn columns)
gaesLation country
C22
20

---

Published as a conference paper at ICLR 2026
Example D.3. Consider the question N₂ and the corresponding SQL queries (Figure 10 The differentiatinng database found by SPOTIT shown in Tables 28|29 This example demonstrates an incorrect gold SQL, which orders by the latest time (DESC) rather than the earlier time (ASC). This directly contradicts the natural language question.
Ns: "Witch country's 's gas station han forst paid castomer in 2012/8/25""
Evidence: "2012/8/25 represented "2012-08-25""
/+Gold SQL Q+/:
s2.souy
FROM transactions_ 1k AS T1
TNKER JOTN gasstations
T2 ON Ti.gasstatforid T2-gaastationid
WHERE 21 2l.dale 22012 08 25r
ORDER BY r1.time DESC
LIMIT -:
/+Generaled SQL P-/:
SELECT cocuntyy
FROM gaestations
JOIN {
SELECT gasstationid
FROM transactions.
WHERE date 22012-08-25'
ORDER time ASE LIMIT
ON G.gaestationid I.gass:ationid;
Figure 10: An example of a query with incorrect gold SQL.
Table 28: transactions.. 1k (skipped irrelevant columns)
gasstation.id date
time
x '2312-08-25' 1
2032 03-25'
2
Table 29: gasstations (skipped irrelevant columns)
gosstation.i
country
21

---

Published as a conference paper at ICLR 2026
Example D.A. Consider the question Nç and the corresponding SQL queries (Figure I7 The differentiating database found by SPOTIT is shown in Tables 30 37 The gold SQL incorrectly encodes the exclusive inequality specified in the natural langue question by using the BETWEEN operator, which leads to inclusive bounds. Thus, the gold SQL is incorrect as it includes values outside of the specified range.
Na: "Peease list patient's plateler level if within normal and if he or she doignosed with MCTD" 100
means platelet within range: PLT <, 100 and PLT 400 meaus platelet level is not within the nomual nange; dingnosed with
Evidence:
refers to Diagnosis
'MCTD"
/aGold SOT. Q+/=
SELECT 12.plt
FROM patieent AS T1
INNER JOIK laboratory AS T2 OR 11.id - T2.1d
WHERE TI.ciagnosis "MOTD" AND
BETWEEN
/+Generated SQL P-/:
SELECT L.plt
LABORATORY
INNER JOLA. PA:TENT ON L.id m P.id
didiagoosis 'MOUD! L.plt 100 L.pl:
Figure 11: An example of query with incorrect gold SQL.
Table 30: patient (skipped irrelevant columns)
id diagnasis
MCTDD
Table 31: laboratory (skipped irrelevant columns)
id plt
0 100
22

---

Published as a conference paper at ICLR 2026
Example D.5. Consider the question N7 and the corresponding SQL queries (Figure 12 The differentiating database found by SPOTIT is shown in Tables 33 SQL is incorrect as it is clearty missing the link to major constraint, filtering only by name.
33 In this example, the generated
N7: "Please indicate the college the person whose first Katy with the Link the major 'mc NN
/+Gold Q+/:
SELECT T2. cé.college
INNER JOIN major AS 12 ON 12.major_id = r1. rd.iark_to_rajee
WHERR
m...io.toommajrr "ophheoo AND 71 rirt.raaee "Katy'
/>Denerated SQL P+/:
SELECT major.college
FROM nember
INNER JOIN MAJOR member. -inkk_o__mjjoor major.major__it
WHERR member rst name
"Katy"
Figure 12: An example of query with an incorrect generated SQL.
Table 32: member (skipped irrelevant columns)
Link.to_major nare
"aa.y'
Table 33: ma j or (skipped irrelevant columns)
major-id college
00
23

---

Published as a conference paper at ICLR 2026
Example D.6. Consider the question Ng and the corresponding SQL queries (Figure 13 The differentiating database found by SPOTIT is shown in Tables 34 In this example, the generated SQL only checks whether the patient
diagnosed with SLE January 1st, 1997. Howeven the natural language question also asks for the patient's s original diagnose at their first hospital visit. Since the generated SQL doesn't 't include this condition, it's incorrect it could return diagnoses from a later visit rather than the patient's 's first one.
Ng: "For the patent who was diagnosed SLF. on 1997/1/27, what was hisher original diagnose when he/she come to the horpital for the fira
Evidence: "SSLE' and original diagnose refers Dingnosis; 1997/1/27 refors 'Examinaation Daze' '1997001227 first came to the hospital refers to patlent. First Date
X-cold SOL. Q-/:
SELECT 71 71.d1agnosis
patient
INNER JDIN exemination AS 12 CN 11.1d 12.1d
WHERE T1.id SRI,CCT 1d
FROM examination
NHERE exami rominrattoo_dae '1997-01-23' AND alannssss 18187
AND
12.examination..ae
T1 firtsdaddd
G*Genecated SQL P-/:
SELECT 12. diagnosis TRCM examination AS T1
patient
Tl.id 12.id
WHERE T1. diagoosss - SSL AND
Tl. r2.exmmination date "3397-01-27'
Figure 13: An example of query with an incorrect generated SQL.
Table 34: pat i ent (skipped imelevant columns)
id diagnosis Cirst_date
'1397-01-26'
Table 35: examination (skipped irrelevant columns)
id examination date
diagnosis
11977011227
24

---

Published as a conference paper at ICLR 2026
Example D.7. Consider the question Ng and the corresponding SQL queries (Figure 14). The differentiating database found by SPOTIT is shown in Tables 36137 This an example of an ambiguous question. The term 'members' can be interpreted in least two ways: any student who is a part of the club, or more specifically, students in the club with the recorded position of "member'. While the gold SQL.taker the second interpretation, filtering 12.position 'Member', i just as reasonable to assume that all students in the club are members, and leave out secondary filter. Coupled with the lack of evidence, the resulting difference queries is most likely due the ambiguity of the natural language question. Hence, it's been marked as an ambiguous question. t
No: "List the last name of members with major in environmental engineering include its department and college name.
Evidence: "Environmental Engineering' is the mujor nome"
/xGold SQ1 Q=/:
SELECT 12.last_name, 11. depastment, rl.college
FROM major AS T1
TYNER JOTN
m1-major_id Ta.
WHERE T2.position 'Membe"! AND T1 m1.major_nn Jname
Fnngt neer! ng²
/-Denerated SOL P+/:
SELECT 11.laat_name, T2, de.depattment, T2.college
FROM nember AS T1
major
to__jjktt__ajor 12.major_id
WHERE
T2rmajor name = "Enviormerte Engineering'
Figure 14: An example of an ambiguous question.
Table 36: ma for (skipped irrelevant columns)
ma jar.id ma jor_name
departmen: colllege
"Envirommental Engineering'
'1'
'1'
Table 37: member (skipped irrelevant columns)
name mejoor
position
25

---

Published as a conference paper at ICLR 2026
Example D.8. Consider the question N10 and the corresponding SQL queries (Figure IS The differentiating database found by SPOTIT is shown Tables 38 39 This example is marked as ambiguous because the natural language question is underspectfied. the intent is to return the legal status of every valid artifact card, which is reasonable interpretation, than the generated SQL. would be correct. However, if the intent is return the of unique legal statuses across valid artifact cards, than the gold SQL is correct.
Nio: For artffct type of cards that do not have mostiple faces on the same card,, state legolities stotus for vintoge play format." Evidence: "Artffact type of cards refers types 'Ariffctt: not have multiple faces the same refors side NULL"; vintage play format refers formaz "Vintage"
/ssold SQL Q-/:
SELECT DISTINCT T2.Stacus
FRUM cards rl
TNNER JCIN legolities AS T2 ON rl.uuid 12.uuid
WHERE Ty.type 'Artifact' AND 72, format 'viintgge' Ti.side IS NULL;
/xGenezated SOL Pe/:
SELECT 12.stotus
JOIN legalities AS 12 ON Ti.cuid = u2.
WHERE Ti.type 'Artifact' AND
NULL f2.mormat
'vintage'>
Figure 15: An example of an ambiguous question.
Table 38: cards (skipped irrelevant columns)
ouid
type
5ide
rg "frti NOT.T.
Table 39: legalities (skipped irrelevant columns)
uuid format status
"vintage" "1'
'vintage' '1'
26

---

Published as a conference paper at ICLR 2026
Example D.9. Consider the question N11 and the corresponding SQL queries (Figure I6). The differentiating database found by SPOTIT is shown in Tables 40 41 This example is considered ambiguous because the natural language question and evidence do not specify tie- tie-breaking rule. In the case that there are two comments on valid posts with a tied high score, a query with LIMIT may return either comment. This is why the generated and gold SQL. return different results. Since the difference arises solely from a lack of specificity, this example is marked as ambiguous.
N11 Among the posts with views ranging from 100 to 150, what is the comment with the highest score" highest refers to
Evidence: "Views ranging from refers ViewCount BETWEEN 150; when MAX(Scomm)
7sBold SQL Q-/:
SELECT
FRCM cormentaa
WHERE postId
SELECT id
FROM poats
NHERR vieeCount BRTNFEN 1.00 AND 150
CRDER BY score DESC
LIMIT
/*Generated SQL P-/:
FCT
TRCM posts A6 T1
TYNER JCTN comments AS T2 T1.id T2-postId WHERE Tl. viewCount BETKEEN 100 AND 150
ORDER BY 12.8core DESC
LIMIT
Figure 16: An example of an ambiguous question.
Table 40: comments s (skipped irrelevant columns)
postid
score
text
Table 41: posts s (skipped irrelevant columns)
1d viewCount
100
100
27

---

Published as a conference paper at ICLR 2026
E
SEMANTICS
[b]
Database D Relation Value
[Tolnt(E]]JD.as
let v =
[ D in
ite(" 0 Null v IsInt(v),
[ToDate(F)] D.a4
lct
E3 p.ara in
ite
Null V IsDate())
ite (Islnt((()) [IntToDate())] p....
ont [StrToate((())))
[ToStr(E]] (iStr(E)]p.ar)
let v
[
p.as in
ite(#
Null V IsStr(v),
ite(Islnt(v), [IntToStr( p..., [oate
ite (us =
Null, Null, as (0) 10 + us(1] 10 + vs
(Sinto))t(s)) p,
let
ite{=(0] "_" (sDigit(ss(I:), (trroo))))))))s
in ite(s 8 Null, Null, v)
[IntToStr(v) p.as [DateToStr(us)Jp...
ite v = Null, Null, IntToStr(v))
let
IntToStr(us(O), m ite(ux(1) S 9, "0" InTToStr(us(()),
(nTooSt((us11]]] (1)).
d ite(us[2] s 9, "0" InfToStr(us(2)).
In(ToStr(us(2))
in ite(us = Null, Null, y "L" --"+
[IntooDatev)]lo.za
lct 01 = [u/10*], 12 (1%11*)) 1, v%10 in
ite(# Null v Vaaliddatte))) Null, (11, 22, va))
[Str (SrTToDate))]Ip.r>
Ict = [Stttoitt(s) p. in
ite Null, Null, [IntToDatevv]]nm p,..)
[E| o E
let
(T]onn((E))]]..... and 11
in ite Nuil V Null, Null, 02)
[SubStr(Ei, Ez, Da
let
D. ei [...: (=ln(e)))) e,
2
[Toint(e)) p.... c/3 [Toit((ss] p.n.: p.
ite( -ee-l5e e/ 0, ez +, e/ < 1, 1, 1)),
ite(u 0V -lv--llvlvv e/ 0,e,
ite -- [,].,,
in ite( = Null v IsStr(e I,ll,,
[Concate(E)) [Ei E2)]
let 01 [ToStr(Es] p. and [ToSt (2 p
p.sa
ite 01 = Null V 02 Null, Null, Concat 01, v2)) 1ct r = [ooDate D.
[Strftime(k, F)
ite k = "%Y"", v0 ite(x = "%M", " o
[JulianDay( E) D.ze
let
E
p,sa in ToJulianDay(!)) if (s)to(
[DateShift i, 1)8)
let
E D,aa in DateAdd(e, 1,8), if (sDtee()))
[o] :: Database D + Relation + Bool U Null
[PrefixOf(s, ]
let ToStr(b)] p... in ite(v Null, Null, PrefixOf(s, v))
OSuffixOf(s, E)] D.ss
let ToStr( b'] D.ss ite y Null, Null, SuffixOf(s, e))
Like E
let ToStr E) ite(y Null, Null, RegexMatch(s,, v))
Contain(s, E) = let Concat(" "%") in [Like(s' E)
E @ Ealp.
= let U1 |Ei]|o. and 12 = [22 D.as in
ite(v) Null = Null, L, 01 v2), if Type(()) Type(oz)
Figure 17: Formal semantics for extended expressions and predicates. The VsValidDate function checks whether a string represent a date within the supported date range of a database engine. The ToJulianDay function converts a date to Julian day and the DateAdd function move a date-value by modifier arguments and 8. The definition these two functions are shown in Appendix G
28

---

Published as a conference paper at ICLR 2026
F ENCODING
[T]olt(E]]ss.TT
= let 8 |.]..
ite = Null v (v). b. D,
let \
[ToDate(E]]s.c.T
|.].. in
ite Null [sDatc(v), v,
ite [ [nntfooaateeollsrrrrs/rrrraaabaa
[ToStr( s.T.
= 1ct 0 = |.] in
ite 0 Null 1s)
[o[[s>St(oo,[IInToS((((]]]]]]s] (ate |e)
[DateToInt us) s...T [Str.
= i = Null,,l Null, us(0) * 10 + os[1] 10 vx(2))
let
=[1:233Lengthh(>)]
23.StToolm((ss))
0 ite(s(0) = --" 23 21.5SS(oooo))
ite(w: < 0, 0.233.nTTSStr(-o))
v1, 21,23.nnTo)))(()) = s),
in ite(= = NNull, Null, (te(
[IntooSt(()) (...T i (us
ite( Null, Null, 23.In(ToStr((t)
let y 23.IniToStrres(00
m ite(v=[1] S 9, "0" 23.In(ToStr(e<(()).
d = ite(us 2] < 9, "0" 23.Im(oSStruss 23.In(ToStr(as((1)))
z3 (3.
ite(us Null, Null, y -+" +++++++***++++ + d)
[IntToDate(]]Iss..7
= let fdiv(e, 10"), ). m fdiv(e%10* 102), d = x%10²,
4 y%41 = 0 (y%100 & 0V y%-100- = 0)
SyS MAX 12, 23 = 1 A ( 31)
41
22 S
2 1.0) A(V=E[460.1)m==<<---
30)
in ite( Null V- (4 62 o3), Null, (y,
= let e [StrTolnt())]ss.r in ite = Null, Null, [IntToDate(
[E, Esls,n
= let [TolntE )..... and 12 = [Tolm ES),,, in i Null v 02 Null, Null, v2)
[SubStr(Ei, Ez, Ea)]ss.r.T
e; E.J.s..7 [ [ =3 1 Lengtthh(())..
2 [Tolnt(e2]]ssn.rr..
[
ite 4, 62 < L,6 1, 1)):
s ite 00v vo@==ovv<tvo>lve
0,s,
ite(e's 2 1-1--, 20:
in ite = Null v (e2) (sStr(ea), Null, s)
[Concate({:: Ex)l (Strttime(x,E))]l..
let 01 [oSStrE) r. and i2 [ToStr E J.r. in
ite( Null v 02 Null, Null, 23. 23.Concat(1s, 02))
let e [ToDate(E]]s.r.T
ite (v = Null, Null,
ite "Y v00) ite(x "%M", (2))) let |F].. ite(u|1]
(JulianDay()]]s.rr
v00 1, (0),,
m ite( e + 12, 12]r d= v(2].
e = 2 fdiv(y, 100) + fdiv(y, 400).
fdiv(36525
4716,, 10=),
42 fdiv * (m + 1), 10*),
in + --d-c- 1524.5, if IsDate())
[DateShit((E,,, 1,.. let |E|s.r.T in ite(8 "Year", DateShiiiBy (e, ite = "Momth", DateShifiBByMoottts....
DateShiftBy Dayssh i)))
Figure 18: Symbolic encoding for extended expressions. The floor division function is defined as fdiv(x, y) = it = 0, x (x x%%y)yy). For clarity, we overload IsInt. IsStr and IsDate to check whether formulas represent integers, strings and dates, respectively. Type conversions and string manipulations are handled using the built-in functions of Z3.
29

---

Published as a conference paper at ICLR 2026
[PrefixOf(s, E,,. [SuffixO((s, E,, [Like(s, F.).S.r.T
let v
[ToStr(E]]ssrr in ite Null, Null, z3. 23.PrefixOf(s. u))
let v
s.r.T in ite( Null, Null, 23.SuffixOf(s, v))
let
[ToStr(F)]]s.r,
i Null, Null, 2ulgll, u))
[Coontiinss, E.STT
let [ToStr[E)]]ss..T and s' = Concat( (" ;,, ".*"" in
ite( Null, Null, z3. Reg.ReexxMatchf u))
[E @ EglsT,
let U1 [i]s.rr and 12 r.. in
ite( = Null V U2 = Null, L, 21 o U2), if Type(v)) = Type(12)
Figure 19: Symbolic encoding for extended predicates.
G PROOF
In this section, we provide the proof of theorems in the main paper.
Theorem 1 (Correctness of expression encoding). Let D be a database over schema S, zs be tuple list, and E be an expression. Consider symbolic database I over S, a list of symbolic tuples T, and E's symbolic encoding [.].. For any satisfying interpretation I with I(T)= D I(T) D8, evaluating the expression over the database D and the tuple list as yields the interpretation of E's symbolic encoding I ([ ). i.e., I(L') D A I(T)
[ I([E]s.T.).
Lemma 1. Suppose [ = v, then I(T) = AI(T)) = zs - [Elza) = [[[ s.T.T)
true iff [E| = v and ((..T.. = v.
Proof. Theorem is proved by proving Lemma [ By structural induction on E.
1. Base cases and some inductive cases are proved He al. (2024).
2. Inductive case: E ToInt(E))
[TTonn((E)]ssrs s.r. = ite(u = Null v IsInt(u), ite(IeStr(u)) (StTToo)))
[Date s.),))
where
[E|sITT ite(a'
by
Fig-
ure 18
[Toln(())]
Null
V
IsInt( ( ), e ite(IsStr(o"), [StrTolnt("]lzzmaann E (ZT) by Figure 17 By inductive hypothesis, we have I(v) I(E])..TT) Z(T),(()) v' Therefore,
where
I [[[Tllt(F)]ss.n
I(ite(v Null v IsInt(u), ite(ISttr()), [StTTont(())s) [oateTollt(e)]]ss...7)
ite(Z(v) Null [[IsInt(v) [(v), ((
ite(Z(v) = Null ( (o..,))
[[[[trTolnn(()]sssrr I[[aate
ite (ter
[StrTolnt(Z(e))]aa)))z)
TDateTolnt([ TD (()))
ite( Null v IsInt(v'), )² "tee ite(IsStr(v')
(StrTolnt(c")Izzam.. [Date Tolnt (v)) (lIzm)
(Foln((F)]
3. Inductive case: E = ToDate E)
(ooDatc(E)ss.r7 ite(v Null IsDate(u), v, ite(Isl)t(v), [ItTo
where [tte v) (StrTTD)te()))ssrrr))) (ooDate(E)lzzuuzpp
F... by
Fig- Null
ure 18
ite
IsDate J, v', ite(IsInt(("))
o (rrTToDatt(u"llzyyzrr [St IStTToTa (1)
where o' [FIz(T),I(T) by Figure 17
By inductive hypothesis, we have
30

---

Published as a conference paper at ICLR 2026
I(v) I(EE],., [[|z()),(())) v'. Therefore,
I [(ToDattE))sssT) = I(ite(t Null (sDate(v), v, (l
vb) = (I) ().T),
Z [
(Z)) = Null v
(
ite(v'= = Null V IsDate(v'), (te(ittt)))
( /ttl [StTToaate
[TolDate(F)]
4. Inductive case: (b)
[ I = it Null v IsStr(v), u ite(IsInt(v), (IntToSttru]lls.... [.... by Fig- ite
[Date ToStr (.),T))
where
ure
18
[ToStr( E))lI
=
Null V
IsStr(
0 (Isint) (f"), IntToStr(u")lzuyyn Z(T) [Date (II))))
where
E Z(T) by Figure 17 By inductive hypothesis, we have I(T),I(T) = v'. Therefore,
I(v) I([E]S,T.T)
I[[ToStr( ()).TT.T) I(ite(v Null [sStrrr)))
I(
[InttoStr(w)]ls..TT]] [DateToStr(] (aatTToTr]] (t
ite(I(u) Null v ((ISStr(v)) ite [te[[(sitt())
[ ToStr (....,))
ite(I(u) = Null Is), ite
(v))...))))
ite(u' Null v IsStr(v'), i'test(s(
[IntToStr(<"]lza)aaa
(
[ToStr(E]Zx,)zz
5. Inductive case: (ote
[DateTolnt((u]] s.rT ite(us Null, +1000==00++==011+0+++++++===+0 by Figure 18
Toant [TT) ite(us Null, Null, ns[0] 10a + us[1] 10 + us (2) by
Figure 17
Therefore, To
ite(us Null, Null, es 10
[s[1]
[1] 10 + v2)) [Date (oateeToon((es)))))).r)
6. Inductive case: StrToint(s)
[Str ite(s Null. Null, ite( v, 0)) where s1 = =[1 23. z3.Length [s)] ite(s(0) "_" U1. z3. Strnnnsss)))) and 1 ite(
V1 23.StrToInt(s:).
0, Int.onto (00trr(v) = 01, Int(ToStr))) (u) = s) by Figure 18 [StrToln((=))zmmzzp
ite(v' = Null, Null, r') where v' ieeiiDDiisss() StrToint(s), ite = ^ IsDigits(s(1:). StrrTonntss), 0)) by Figure
On the one hand, the Z3 builtin function z3. StrTtool))s)) = StrTolnt(s)) if StrTolnt(s)) 2 0: otherwise, 23.Strtol)s(s) -1. To show our encoding precisely capture semantics of SQL's type conversion from strings to integers, let us discuss it in three cases:
(a) If StrToInt(s) 2 0, then v = z3.StrToInt(s) StrToInt(s) (s and & holds. Thus, ite( (, v, 0) = v.
(b) StrToInt( 8) < then v -1 and + T where 81 StrToInt(s[1 :))- ite( v. 0) = 0 UU-
(c) If contains more than digits (c.g.. "abe" and "-abe"), MYSQL evaluates non- numerical strings to 0 by default. By the semantics of z3.StrToInt & never holds which leads ite 1b v. 0) 0.
By 6a and 6c conversion from strings to integers.
known ite( 0) precisely captures the semantics of SQL's type
On the other hand, let discuss the rule in three cases:
31

---

Published as a conference paper at ICLR 2026
(a) If StrTolnt(s) 2 0. then o' StrTolnt(s).
(b) If StrTToInt(s) (8) < then v' StrToon((s[1:])
(c) If 8 contains more than digits (c.g., "abc" and "-abc"), MYSQL evaluates non-
numerical strings to by default. By the semanties of this rule, o' =
By 6a 6c and 6c, we known o' precisely captures the semantics of SQL's 's type conversion
from strings to integers.
Therefore, ( s, 0)) = v' and
I[[StTooln(s]]]s.rrr
[(ite(s Null, Null. ite ④2 0)) = ite(s = Null, Null, I(ite u, 0))) ite Null, Null, o')
= [StrToint(3)]
7. Inductive case: E IntToStr(u)
[IInToStr ( S...TT [IntToStr I(T)) i Null, Null, IntToStr(v)) by Figure 17 Note that
ite( =
Null, Null, 23.nTToStr(t)) by Figure 18
since the Z3 builtin function z3 Int precisely capture the semantics of Intrr ((23 IntToStr(v). Therefore,
I(IntToStr(/)lssrrr)
= I(ite (u = Null, Null, z3. (3.TTooStt(u)))
ite(r Null, Null, I(23.I[( (t))) ite( = Null, Null, IntToStr(u)) [IntToStr(e)llmmxxrr)
=
8. Inductive case: E' = DateToStrress
(oSt S.r.TT ite(us Null, Null, y + "." + -." + d) where y Z3. (.InCToStruuu(0]] m = [vs[vs[1] < 9, "0" + I3.Toto os 1]), z3. InioSStrrr os
and d [2] s 9, "0" + I3. (2). z3 IntTotr (2)) by Figure I8 (oStr
ite(us = Null, Null. V' + a_" + m' + + d') where y = In(ToStr(us(O), m' = ite < 9,"0" + IntToStr(es(I]) [1], (nrToStr(us(L)), and d' ite I 9, "0" IntToStr( us [2]), IntToStr(cs)) (2)) by Figure 17 Note that since the Z3 builtin function z3 IntToSr precisely capture the semantics of IoS I(y) = v'. [(m) m', and I(d)= = d'. Therefore.
[[[uateeoStrruss]s...r] = ite(cs Null, Null, I(y) "_" + I(m) + +"" I(d))
I(ite es = Null, Null, y +"""" ++*"*++**** +m+++++
ite(cs = Null, Null, y + " + +m' + "- +
[Date (otte
9. Inductive case: E = IntToDate(v)
ite(v Nullv Null, [y, m. d)) where (div(z,))) y) ite(=%y- = 0, 0/v/ (x: 2%y)/v), y = fdiv(r. 10a), = fdiv(u%10 100), d v%10?
[IntToDate(v)]s..1]
Po = y%4 = 0 (y%100 + -VV = 0), $ MIN_YE, S S MAX YEAR,
Φ 1 5 < 12, 03 1 5 A (V<e1135..8..0.22
d < 31) (m + d < 30) by Figure 18 = ite(v' = Null V lsValidDate(v), Null, [V vgg dd)) where 1/ |v/10*], J, = =[00%10*/100/] v/g v%102 by Figure 17 By semantics of fdiv, know y= uh. m = vig and = =zg Note that the function Is ValidDaee precisely capture the semanties of - Φ A Φ3). checking whether date is valid in MYSQL. Therefore, I(-(0, A $2 A 4 = IsValidDate and
2 d < 28 + ite (e00,,1,0)) A (Vce(4,6,9,1))
[IntToDate(v)lzzmaaa
[[[[n[ToDate()]]ss::]
I(ite( Null V ( A 42 A Null [y, m, d))
ite(u = Null V ( o A A2 A 2a)), Null, I(y. m, d))
=
ite(v Null V Is VaaaidDatee (v'), Null, [t] 1/2 v/]))
= (ntToDate(w)]
32

---

Published as a conference paper at ICLR 2026
10. Inductive case: E StrToDate
Null, Null, [IntToDate<]]ls.rr]] where (TTTTDaat(ss)lIrnnaa = ite(s [StrTolnt(s)]ss.rr by Figure 17 By inductive hypothesis, we have To v I..,T) = [[(ntToDate [IntooDate(Tu)))layy.. = [IntToDate (v' (I()) Therefore,
[SttToDDaee $) s.l. = (s
[StrTolnt(s)] s...TT S.r.T by Figure 18
Null, Null, [IntToDate( (v I(T)) where
I([StToDate(<]Is.rrr)) = [(ite(s = Null, Null, (
ite(s Null, Null, I[IIntTooate u (...7) = ite(s = Null, Null, [IntToDate (r)) (I()))))) ((rTToDate)))z())..)
11. Inductive case: E = Ej E2.
Since our extended grammar considers Null, integers, dates and strings, shown in Figure 2 the proof for this inductive case is overloaded.
[E E2.ls.r.T = it = Null V 02 Null, Null, 0n 02) where and U2 (20on((E2))ls..))) by Figure 18 [E] EaIz(r),IIT)) ite( Null do
and vi2 [ToInt( [Toln((=a]ax))a have I(mr [([ToInt(E)]]ssn)) [Tolnt( Eg II(T),T = vi and I(v2) = I(Toom(E))ls.rr = [ToInt(E>]] (2))((()))l())))1))))) =
Null, Null, ri v22 where of = [Tolnt E (
by Figure 17 By inductive hypothesis,
1/2. Therefore,
I([EI o E2I(s.T,T)
I(ite(v) = Null V v2 Null, Null, o 0x2))
ite(I((v1) = Null V I((22) = Null, Null, [(()) o I(()))
ite(s) = Null v 0/2 Null, of o
= [E o EZIIZT)
12. Inductive case: E SubStr(Ei, E2, E3).
[SubStr E1, Eg, Eg)]ss.TT = ite(e: = Null V IsStr(e2) V IsStr(es), Null, 8) where 6; [.I. for < < 3. éi [ToSt(e
L3gghgg eg [ToInt(e))] (2).)..)....... eg = [Toln((s))Is..TT e= ite e2 < 0, itee < e/ 1 1,1+ 1)). 8 i 0
-IV IV s ite 2 v. v.elv [. 20 2)))
by Figure 18
[SubStr(E], E2, Ea) E = ite(e4 Null v IsStr(es) IsStr(es), Null, s) where 6+4 [E for 1 < S 3, c [ToStr(=)]Ixm,zI))) 1' (3.Lengthhe().
& [Toint(e))
c [Tolnt(<a)l of ite(- 65 0, ite < 4 0, ite(c)
L,,' 1,7+ ite -
v, c
[. :2 22 +(D) by Figure 17
By inductive hypothesis,
have I(e:) [(E [E.]s.r
eit for = c. I(e)
[ToStr(ew))x 1 < 3. Then, I(e() I[ToSt((eulss..T)> [ I([Toln(e)))ss.r) = [Tointess]22m
el.. and I(e() [[[ToIn((=)]sssrT] =
[Toint(es) es ())) = egg. I(e) = e', and I(s) = s'. Furthermore, since the Z3 builtin function z3.Length precisely captures the semantics of len, we have I(l) = I(z3.Length(e)) len(e() l' Therefore,
I([SubStr(L)) E1, Es, Ba)ls..TT) = Z(ite(e) Null v IsStr(ee) v IsStr(ea), Null, s))
ite(Z(ez)) Null v ([IStr((e)) v ((ISStr(es)),
((s))
ite(e, Null V IsStr(es) v IsStr(ee)).
= [SubStr(Fi, E, E2, Ea Fa)lz()))
13. Inductive case: Φ = Concate (E1, Ez).
[[Concate E2).
ite(v1 Null V 82 Null, -, 233.Conaat(in U1, Up
where U1 = [oSst(EE))lss.r, and U2 = (ToStr(E)]ss.n by Figure [8
[[onncate( F,, F2) F2)] ite(v)
Null v e/ Null, 1, 1,73.Concat(1f, v6)) where
33

---

Published as a conference paper at ICLR 2026
and 1/2 (ToStr(E2)]zzznn by Figure 17 By induc- tive hypothesis, we have I(v1) I[[ F [.,,T.. = [FlIzT), = vi and T(vz) = I([Ke]s.r;)) = [ = 1/. Furthermore, by the semantics of z3.Concat, ((23Cooncat) - Concate. Therefore.
1 =
I([Concate(Fi, F2).ss.r,T)
[( Null V 0/ = Null, 1, 23. Co.cattaa(() v2)))
ite Null v VI((g) ) Null, -,
(o)c. I(2)))
ite(2) = Null v us Null, -, Concat(u,, u4))
[CConcate(E, E1, (())
14. Inductive case: E = Strftime E).
"% . v/0), ite(k "%M"", ,i[], =(2]))) where v = E|s. by Figure 18 [Stritime(ks, E) ZzT))
[[Strftime(x, E,
ite(v Null, Null, ite
ite(w Null, Null, ite(x = "%Y", " (te) = "M"", ,[[], x(2))) where [B]zrr,z by Figure I7 By inductive hypothesis, we have I(v) = I([4),,
[Elz(T)Z((T) = v' Therefore,
[[[Strftim((xx E)]s,,,)
I(ite(c Null, ite "%Y", v00]
ite(k = "%M", v[]],
ite(I(v))
ite "% Y [(u)[O) ite( = =1<'"=">''', [()],
ite = Null,, ite "%Y",, v'
[Strtimee(xxE]]lzxxax
15. Inductive case: E JulianDay(E).
[JulianDay E)
n.T ToJulianDay(u) where v = [E] if u is evaluated to be a
date by Figure 18 Also, ToJulianDay(o)
365.25 * (y + 4716) + |30.6001 * (m
4716)] + d c c 1524.5 where y =[1] < 2?e(0) - -1:v[0]. m = = < 27e[1] +
u[1]. d =2]]. and c 2 [y/100] + Ly/400]. [JulianDay(*]]zzmmarr
01
02 d' + + 1524.5 where v' -B] 1/ ite(v'[1] 20 (,,
m' ite(v'[1] < 2, v'[1] + 12, 12, [L]),, d' = 22 = fdiv(y''
fdiv(365254 (y/ +4716), and and 02 = fdiv 2 100) fdiv(y// 400).
(,,,++))10"" 10 if evaluated
be date by Figure 17 By inductive hypothesis, we have I(v) -[(FF].rr.)
[E]zrr),(r I(T) = v' Furthermore, by the semantics fdiv, I([365.25 25 (y + 4716)]) = ai
and 3[3060001 * (m + 4716)]) = 42. Therefore,
I [[[JulianDay(]]lsn
I (ToJulianDay(())
I[ 335.225 * (y + 4716)] + [30.6001 * (m + 4716)
+d + 1524.5)
+ a2 + d'
(JulianDa(EE]lan)
16. Inductive case: E DateShift(E,,,0) i,
[Dateehiit(E, 8) s.r.T ated to be a date by Figure 18 Also, DateAdd(v, 8) is defined as follows:
DateAdd(v, i, 8) where e [ToDate(E]]ss if v is evalu-
(a) If = "Year", then DateAdd(v, 5) = ite(''(0) < MIN. YEAR V MAX. YEAR <
[0] Null, Null, v') where o' [u[0] + i, v1], e/2]] can be negative and dates falling outside the valid date range are regarded as Null.
(b) If 5 = "Month", then DateAdd(r, i, 5) = ite(v"[0) < MIN YEAR V MAX YEAR <
nf [0), Null, Null, v') where v' = [0[0] + fdiv(e(1) + 12), (v[1) + 1)%12, s/2]].
(c) If = "Day". then (ateAdd(r, 5) = ite( < MIN A v > DATE, v') where o' is new data variable s.t. SinceBegin(e")) SinceBegin(v) = i. In addition, the SinceBegin function counts the ordinal num- ber of date from certain day, e.g., "0000-01-01", which can be defined as
34

---

Published as a conference paper at ICLR 2026
SinceBegin(y, m. year2day(y) + month2day(m) + d where
(ear2day(y)
365 x 1 rdiv(y 1,4) fdiv - 100) fdiv(y 400)
month2day(m) >m it E (1,3.5,7,8, 1, ite = 2, 28 + ite(leap(y)) 1, 3))
Thus, SinceBegin(v') - SinceBegin(w) = i ensure the date v' is i days away from the date
it = "Year", DateShiftiByYearss(..)) i), ite "Month", DateShifiByMonnths( i). DateShiftBDDays((,,, i))) where i1 = [FImm
[DateShift( EMI
is evaluated to be a date by Figure [7] By the semantics of the DateShiftBy Years. DateShiftByMonthss and DateShiftByDays functions, they corresponding the case T6a 16b and [6c Therefore.
E, i, = I(ite ó = "Year", DateShiftBy DateShiftBByYerss(r,, i), ite "Month", DateShiftByMnnthy DateShiitBB(Dasss(,,))) i ())
Theorem 3 (Correctness of predicate encoding). Let D be database over schema S, as be tuple list, and & be a predicate. Consider a symbolic database over a list of symbolic tuples T, and é's symbolic encoding LIlS.I.T. For any satisfying interprelation I with I(T) = D A I(T) Ds, evaluating & over the database and the tuple list as yields the interpretation of o symbolic encoding I( i.e.,
I(T) DAI(T) = as = [olD, I[[o]s,T.T)
Lemma 2. Suppose [ as is valid, then I(T) = AI(T) holds.
[oz I([oss.,7)
Proof. Theorem
3 is proved by proving Lemma 2
By structural induction on ø.
1. Base cases and some inductive cases are proved in He et al. (2024).
2. Inductive case: Φ PrefixOf(s, E).
[[PrefixOf(s, ElS.TT V [ToStr E)ls.I.T by Figure 19
ite
Null, Null, z3 PrefixxxOO((s v)) where [PrrffxOf((s, E)I
ite(e'
Null, Null, PrefixOf(s, v')) where e' ductive hypothesis, we have I(v) = (TTTTTT(E)]] = [ToSStrEE EE) = v.
(oSttr())llxa),xtr))) by Figure 17 By in-
Furthermore, since the Z3 builtin function Prefixii precisely captures the semantics of PrefiXOf, we have Pryf.PrefixOf(s, v)) I(z3.PrefixOf(s, ("ToStr(E)]ss..r))) PrefixOf((s, (eeeixO(ssI(((TSSt((EEE)) [[[ToStr(EE]llssrr)))) Therefore,
PrefixOf(s, [ToStr())] PrefixOf(s, v')
I([PrefixOf(s,E)] E)),,
Z(ite(v = Null, Null, z3. PrefixxxOO(s u)))
iTe(I(v) =
Null, [ PrefixOf(s, v)))
ite(r' = Null, Null, PrefixOf(s, v'))
E)
3. Inductive case: SuffixOf(s, E).
[[SuffixOf(s. s, ESS.TTTT = ite(v
Null, Null, z3 S3.SuffiOOf(s, v)) where [SuffixOf(s, E)
ite(v' Null, Null, SuffiOO(ss, where v' [ToStr(D]] by Figure 17 By in- ductive hypothesis, have I(v) Toortr (TroSt((E))llmrrra)) ()) [ToStt(E)]s.I.T v'. Furthermore, since the Z3 builtin function 23.SuffixOf precisely captures the semantics of OfffixOf, we have T(z3.SuffxOOfs. v)) SuffixOf,O [Toost(F)]]ss.,rr]]
V (E))s..Ts by Figure
19
35

---

Published as a conference paper at ICLR 2026
S
SuffixO((s [TTixOO((s/Toss((E))zxxxxrrr
SuffixOf(s, v')
Therefore,
([,SufiiOOf(s,E))s.rs.
= I(ite(v =
Null, Null, 23.SuffixOf(s: e)))
ite(Z(u)
Null, Null, I x)))
ite = Null, Null, SuffixOf(s;
[SuffixOf(s, E)]
4. Inductive case: Φ Like(s, E).
[[ E) S. ite( Null, 1, 23. RegeXMach(s) where [T)Str(E]]ss s.r.T
by Figure 19
[Like(s, E) I(T)
ite
Null, Null, Regex s, v'))
where v'
By inductive hypothesis, we Furthermore, since Z3 precisely support regular expressions, we have (egex v)) = [ege [[[Totr(E)]]srrr]
[ToStt( (rost(())lzzra () by Figure 17
have I(u) = I([ToStr(E]]ss
= E
I(23. Reg..eeexttt,ss, (ToSt(6)]ss,,77) =
RegexMatch(ss, [ToStr(E)]l
RegexMatch(ss, v²). Therefore,
E)lssr)))
I(ite(v Null, 1, RegexMatch(s,, v)))
ite(I(v) = Null, J, I(z3 RegexMacchsssss v)))
ite( Null, -, RegexMath((s, v'))
[Like(s, F)]
5. Inductive case: o = Contain(s, E).
[[oontain(s, E)lsTT 8'
ite(v
Null, I, 23. Regex ,.) where (ToStr(E)lss..7 by Figure 19 ite(v'
Concate *m 8, " pm
and
[[Contain(s, E)
[Like(s" E)
Null, Null, RegexMatch(s" (s" v')) where 8" Concate "%"" and o' (TToStr(F)llzTT,, by Figure Futhermore, by the semanties of z3. Regex and RegexMatch, we know and s" represent the same regular expression, and I(z3. Rew.eeeatcch(s''"" x²)) = Regex iff T(x') = x". Therefore,
Z(ite(v Null, 1, 23. RegexMatchhs',,
ite(I(v) = Null, 1, I Ratex (atch(sss,)))) ,)))
ite(e' Null, 1. RegexxMtchh(s" v'))
[Like(s",E)]laee EE)
[Contain(s,E]] E))x
6. Inductive case: Φ Eạ ④ E2.
[F1 @ S.S.TTTT = ite( (r) Null 122 Null, 1, ④ 02) where on [F s.r.T and
= [F s.r.T if e; and 02 share the same type, i.e., Type(r)) Type(12) by Figure 19
[E O E2 = ite(vi = Null v v/ = Null, 1, of O v/)) where ts = [
and 2/g Eg IT)) if 0f and to share the same type, i.e., Type(x/) = Type(us) by
Figure 17 Note that this operation only works for E₁ and Eg sharing the same type which is consistent with MYSQL. By inductive hypothesis, we have I(vi) = I[[ ([Ei]Iur), = [E]]s,r,T = of and I(0²) I([EaIz(r)z [E2ls.r.
v.z. Therefore, when E,
and Eg have the same type, we have
I([Fa @ F2ls.r.T)
Z(ite(v: (n Null V 02 Null. 1, ② (22)
ite(I((;) = Null V ((()) = Null, 1, ) @ I(r2))
ite(u' Null V og Null, L,
[E] & EaIzanz
Theorem 2 (Equivalence under set semantics), Given two relations R₁ [t..... ......,t) tal and R₂ (ri..... Tm,, formula (2) is valid, then R₁ and Ra equivalent under set semantics.
36

---

Published as a conference paper at ICLR 2026
Proof. Let Fi be the first conjunct of formula ie., A (-Del(t,) + (-Delr)) At, ry), and let F2 be the second conjunct of formula (2) i... Az= (r)el(r)) - (-De(-) Ary t.). Since formula (2 is valid, both Fi and F22 are valid. Now consider F1. It specifies for any tuple I E R1, if I is not deleted, then there exists a tuple fj that is not deleted and 4 rj. By the definition of C. Ri C R2. Similarly, F2 specifies R2 C R.. Therefore, Ri R2.
37


Reviews:
[{"review_id": "HBDksHJYOL", "reviewer": "Reviewer_E2Yh", "summary": "The paper introduces SpotIt, a verification-based evaluation pipeline for Text-to-SQL that replaces single-database execution tests with SMT-based bounded equivalence checking. Building on VeriEQL, the authors extend the supported SQL fragment with dates/strings, implicit type casts, set-semantics equivalence, and provide correctness proofs for new encodings. On BIRD-dev (1,533 items) across 10 top-performing systems, accuracy reported by standard EX-TEST drops by roughly 9.8–13.5% under SpotIt/SpotIt+, and rankings change substantially. Minimal counterexample databases expose three root causes for mismatches: incorrect gold SQL, ambiguous NL questions, and incorrect generated SQL. Manual audits suggest problematic gold SQLs are common; in some cases, ambiguity makes multiple SQLs “reasonable”. Algorithms for iterative bounds, validation against a real DBMS to filter spurious CEX, and cross-checking of counterexamples across systems are described. Runtime is practical (seconds per pair) with good coverage gains over baseline VeriEQL.", "questions": "1. How sensitive are SpotIt’s findings to the choice of K? Any empirical curve of detected non-equivalences vs K and the diminishing returns?\n2. Did you observe cases where K=5 missed mismatches that appeared at higher K? Any characteristic patterns?\n3. How many spurious CEXs did the validation filter out, and which operators were most responsible?\n4. Can you report results on Spider 2.0 (or BIRD-Interact) to assess generalization beyond BIRD-dev?\n5. How do encodings reconcile engine idiosyncrasies (e.g., string-to-int casting behavior, date boundaries)? Any cross-engine discrepancies observed?\n6. For ambiguity cases, would adding light-weight interaction (à la BIRD-Interact) change pass/fail judgments under SpotIt?", "limitations": "", "rating": 4, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "S1. Strong and timely problem framing; evaluation reliability is critical for Text-to-SQL progress.\nS2. Clean pipeline with validation and cross-checking; minimal CEXs make root causes transparent.\nS3. Substantive empirical findings (accuracy/ranking shifts; gold SQL issues; ambiguity prevalence).\nS4. Formal treatment and proofs for extended string/date operators and set-semantics equivalence.\nS5. Practicality: seconds-scale per-instance runtime; high coverage relative to prior verifier.", "weaknesses": "W1. Bound sensitivity (K): The paper does not quantify how many non-equivalences require bounds beyond K=5, so the false-negative rate is unknown. A detection-vs-K curve and examples missed at K=5 are needed to calibrate trust in results.\nW2. Dataset scope: All results are on BIRD-dev, leaving external validity uncertain. Including Spider 2.0 and one enterprise-style schema would test generality and robustness of conclusions.\nW3. Cause attribution (gold vs ambiguity vs model): The labeling relies on a small, non-adjudicated manual audit, which risks subjectivity. A larger, blinded, multi-annotator study with agreement stats would strengthen these claims.\nW4. DBMS semantics alignment: The SMT encodings may not match engine-specific behaviors (NULLs, casts, date ops), but this isn’t systematically evaluated. Cross-engine validation (SQLite/MySQL/Postgres) and documenting divergences are necessary.\nW5. Presentation quality: Frequent typos/formatting glitches and occasional terminology inconsistencies reduce clarity (e.g., “SQL ITE”, “hosptial”). A thorough proofreading and added navigational aids for dense formal sections would improve readability.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "IWluzK5hhA", "reviewer": "Reviewer_NZfv", "summary": "Traditional Text-to-SQL evaluation typically relies on comparing execution results. However, this can miss subtle semantic differences between the generated and gold SQL, as different queries may produce the same result on a particular database. SPOTIT addresses this limitation by introducing a formal verification-based evaluation method that uses an SMT solver to construct minimal test databases where two SQLs have different execution results. SpotIt supports richer SQL queries than existing methods. Existing text2SQL methods show a significant performance drop after employing SpotIt, highlighting the need for more rigorous SQL verification.", "questions": "1. Did you run any experiments with varying K? How does the latency and accuracy change with increasing K? Would we discover more erroneous SQL queries if we increase K?\n2. In practice, how do users choose the tuple-count bound K for counterexample search? Is there a systematic way to trade off between “smallness” and coverage of semantic differences?\n3. How does SpotIt latency grow with SQL complexity?\n4. On a more complex text2sql benchmark, such as Spider 2.0, could you estimate the percentage of SQL queries that can be covered by SpotIt? It's ok if the percentage is low because not everything can be encoded into SMT solver. But it would be nice to give readers more context because the community is shifting to more complicated benchmarks.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 4, "presentation": 3, "contribution": 3, "strengths": "1. This paper tackles an important problem in Text-to-SQL, assessing SQL correctness beyond execution equivalence. By searching for minimal counterexample databases where two SQL queries diverge, SpotIt offers a more rigorous correctness check and greatly simplifies debugging (e.g., identifying faulty ground truths in BIRD).\n2. The paper extends the SQL syntax that can be encoded into an SMT solver, which is a great contribution. It consistently covers more than 90 percent of the queries generated by various models.\n3. I liked the error analysis the authors did on the BIRD benchmark regarding why the gold SQLs are incorrect. I’ve also personally encountered many erroneous ground truth SQL queries in BIRD, and it used to take me a lot of time to figure out why the reference SQL was wrong. With SpotIt, it would save researchers a significant amount of time identifying these issues.", "weaknesses": "1. SPOTIT only searches for divergences up to a fixed tuple-count bound K. Semantic differences that manifest only on larger databases (e.g., join multiplicity) may go undetected if no small counterexample exists.\n2. As schema size or query complexity grows (many tables, join many tables together, deep nesting, large numbers of predicates), the SMT solver’s search space can explode, leading to longer solve times.\n3. There are still some unsupported SQL features, such as window and analytics functions. I know those might be out of the scope of this paper, but it would be good to discuss them and give examples of SQL queries that can’t be supported.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "bs8EZOs8K8", "reviewer": "Reviewer_eshx", "summary": "In the text to SQL systems, evaluation is an important component and the present evaluation methods are largely based on the execution of the generated SQL and ground truth on a static database. Such kind of evaluation may not lead to the best results as two queries can coincidentally produce the same output on the test database while actually being different. SPOTIT proposes a new alternative evaluation pipeline, where a formal bounded equivalence verification engine actively searches for a database that differentiates the generated and ground-truth SQL queries.", "questions": "How is the experiment impacted on changing bound (K) and does increasingly reveal more counter examples.", "limitations": "", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 4, "contribution": 3, "strengths": "In text to SQL evaluation plays a vital role and this paper acknowledged the issue. Current methods relying on test-based execution on a static database are optimistic. The proposed solution, SPOTIT, replaces the weak test-based check with a much stronger, formal verification method. This also showed that the reported accuracy of these methods drops by 11.3%–14.2% when switching from the official test-based evaluation to SPOTIT", "weaknesses": "The sensitivity of the bound parameter (k) is not analyzed, leaving unclear how verification completeness and runtime scale with k. The paper does not report statistics on timeouts or unsupported queries.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "PRqKbSd4oL", "reviewer": "Reviewer_p5hF", "summary": "This paper introduces SPOTIT, a framework for improving the evaluation of Text-to-SQL systems via formal verification. Instead of relying solely on benchmark-provided test cases, SPOTIT aims to automatically generate counterexample databases that can distinguish between a generated SQL query and the corresponding gold (ground-truth) query.\n\nSPOTIT extends VeriEQL (He et al., 2024) to handle a broader range of SQL constructs frequently used in real-world datasets such as BIRD, including string and date operations (strftime, JulianDay, ToStr, substr, LIKE, etc.). The system is applied to outputs from ten Text-to-SQL models, revealing that many incorrect or semantically mismatched queries pass traditional dataset-based evaluations but are correctly identified as incorrect by SPOTIT.", "questions": "1. How is the value of K (the search bound) determined? Larger K improves completeness but increases runtime—what trade-offs were observed, and what values were used in experiments?\n  \n2. Which query classes cannot be tested using bounded equivalence? Are such queries present in benchmarks such as BIRD?\n  \n3. How does runtime scale with the number of tables, query complexity, and schema size?", "limitations": "", "rating": 4, "confidence": 5, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "* **S1- Clear motivation and formulation**: The paper identifies a well-motivated gap in evaluating Text-to-SQL systems due to incomplete or non-discriminative test databases and formalizes the problem elegantly.\n \n* **S2- Extension of formal verification**: Extending VeriEQL to cover a richer subset of SQL operators is a nontrivial and practically useful engineering contribution.\n \n* **S3- Comprehensive evaluation**: Applying the verifier to ten different Text-to-SQL models on BIRD demonstrates empirical value.\n \n* **S4- Readable and well-structured**: The paper includes illustrative examples that make the approach and findings easy to follow.", "weaknesses": "* **W1- Limited related work coverage**:\n  The paper omits prior research on test data generation and SQL verification, including approaches based on constraint solving and fuzzing [a,b,c].\n  \n  * [a] Chandra et al. Data generation for testing and grading SQL queries. VLDB Journal, 2015.\n  \n  * [b] Somwase et al. Data Generation for Testing Complex Queries. arXiv, 2024.\n  \n  * [c] Zhong et al. Semantic Evaluation for Text-to-SQL with Distilled Test Suites. EMNLP, 2020.\n\n* **W2- Context and positioning**:\n  Related work is moved to the appendix, which weakens the contextual framing. A short related work section in the main text would help readers understand how SPOTIT builds upon and differs from existing formal or data-driven SQL evaluation approaches.\n\n* **W3- Limited scope of expressivity**:\nWhile the supported SQL subset has been expanded, the framework still cannot handle aggregation subtleties (e.g., nested subqueries, HAVING clauses, or complex joins) as far as can be inferred from Fig 2. Clarifying this limitation would improve transparency.\n \n* **W4- Scalability concerns**:\nThe reliance on a SAT solver introduces potential scalability issues as query and schema complexity increase. The paper would benefit from runtime statistics or analysis of computational overhead.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)