Source-linked AI summary
Building SQL Equivalence Proofs from Query Rewrite Rules
Chunyu Chen, Xinyi Huang, Zhengjie Miao
TL;DR
Determining whether SQL queries agree on every database satisfying schema constraints matters for query rewriting and text-to-SQL evaluation, while semantic solvers face practical coverage challenges. EquiTrace builds standalone proofs by composing rewrite rules, aligning representations, and recording derivations; it proves equivalent pairs across three corpus classes, including more query-rewrite cases than QED or SQLSolver.
Problem
Semantic solvers must model bag semantics, NULLs, subqueries, and integrity constraints, and the literature and experiments report unsatisfying empirical coverage of practical queries.
Source: §1 · p. 1Method
EquiTrace separates rule validity from proof discovery, aligns alternative representations, and composes proof-oriented rewrites into replayable derivations to a common expression.
Source: §1 · p. 1, §3.1 · p. 2Results
Across three corpus classes, EquiTrace proves 648/1,106 expected-equivalent text-to-SQL pairs (58.6%), 229/266 curated pairs (86.1%), and 97/240 LLM rewrites (40.4%).
Source: §1 · p. 2Takeaways & Limitations
The recorded derivations expose the transformations and assumptions supporting each proof, and can be replayed as explicit certificates.
Source: §1 · p. 1, §3.3 · p. 3Remaining gaps include search that stops at caps or timeouts in large join regions and cases where saturated search suggests missing transformations or canonical representations.
Source: §5.2 · p. 6
Abstract
from arXiv · showhide
Query rewriting and semantic evaluation of text-to-SQL systems both depend on deciding whether two SQL queries return the same result on every database satisfying the schema constraints. Decades of equivalence-preserving optimizer rules provide a natural basis for constructive proofs: two queries are equivalent when admitted rewrites transform them to a common logical expression. Building on this observation, \sys{} organizes query-rewriting knowledge as a standalone proof-producing system. It separates rule validation from proof discovery, explicitly aligns alternative query representations, and returns the resulting rewrite derivation. Across three corpus classes, EquiTrace proves 648/1,106 expected-equivalent text-to-SQL pairs (58.6%), 229/266 curated pairs (86.1%), and 97/240 LLM-generated rewrites whose results agree under benchmark execution (40.4%). On the query rewrite corpus, EquiTrace proves 97 pairs, compared with 35 for QED and 38 for SQLSolver. An analysis of 1,242 recorded proofs shows that coverage depends on a small number of transformations, while many frequently used rules are individually substitutable. The resulting derivations make each proof replayable and expose the specific transformations on which it depends.
1 INTRODUCTION
The introduction asks whether accumulated query-rewriting knowledge can support standalone SQL equivalence proofs, given practical coverage limits of semantic solvers and mismatches between optimization and proof construction. EquiTrace separates rule validity from proof discovery, aligns representations, and returns replayable derivations.
1 INTRODUCTION
- Symbolic equivalence methods require increasingly rich models of bag semantics, NULLs, subqueries, and integrity constraints, while practical query coverage remains unsatisfying.The introduction asks whether accumulated database rewrite knowledge can serve as a complementary basis for proofs.Source: §1 · p. 1
- Adapting Calcite exposes three optimizer–prover mismatches: one-way guarded rules, transformations requiring global join-region rebuilding, and syntactically distinct equivalent expressions that need normalization.Examples include reverse join-to-semi-join transformations under uniqueness guards and reordered conjunctions.Source: §1 · p. 1
- A standalone prover can combine optimizer transformations, verified rewrite libraries, integrity-constraint reasoning, and semantic canonicalizations while exposing the transformations and assumptions behind each proof.These canonicalizations aim to expose equivalence rather than produce an efficient plan.Source: §1 · p. 1
- EquiTrace separates rule validity from proof discovery, explicitly aligns alternative query representations, and records replayable transformation sequences that reach a common expression.Its implementation uses Apache Calcite, but the principles are not tied to Calcite or one optimizer’s rule inventory.Source: §1 · pp. 1–2
- 648/1,106 expected-equivalent text-to-SQL pairs (58.6%), 229/266 curated pairs (86.1%), and 97/240 LLM-generated rewrites (40.4%) are proved; on the rewrite corpus, EquiTrace proves 97 pairs versus 35 for QED and 38 for SQLSolver.The LLM rewrites counted here agree under benchmark execution.Source: §1 · p. 2
2 BACKGROUND AND RELATED WORK
The background frames equivalence proving as a complementary use of rewrite systems, contrasts it with solver-based semantic verification, and positions EquiTrace as a standalone alternative to optimizer-embedded verification.
2.1 Query rewriting and logical equivalence
- A verifier asks whether two queries can connect through equivalence-preserving transformations, rather than searching their equivalence class for the lowest-cost representative.The resulting derivation is checkable because each step identifies a rule and establishes its side conditions.Source: §2.1 · p. 2
2.2 Existing equivalence provers
- Semantic provers encode query pairs in formal systems and discharge equivalence with solvers, bounded verification, or proof assistants; rewrite-based verification instead reuses validated transformations as lemmas.Examples include UDP [4], SPES, SQLSolver, QED, VeriEQL [8], EQUITAS, HoTTSQL [5], and WeTune.Source: §2.2 · p. 2
2.3 QO-Verify: the optimizer as verifier
- EquiTrace uses query-rewriting knowledge for a standalone proof system, unlike QO-Verify, which searches optimizer-generated spaces for a common expression.The standalone design makes rules and search independently extensible, proofs inspectable and replayable, and failed proofs analyzable in terms of missing transformations.Source: §2.3 · p. 2
3 EQUITRACE
EquiTrace turns admitted query-rewriting knowledge into a standalone proof system that aligns alternative representations and searches for a common logical expression. Its output is a replayable derivation that records transformations and relevant assumptions.
3.1 A proof-oriented rewrite system
- EquiTrace combines executable, semantics-preserving rewrite rules—including optimizer rules, proof-oriented inverses, and schema-dependent equalities—with deterministic strategies and exploratory search.The individual equalities are largely established results; the contribution is making their admission, orientation, composition, provenance, and application explicit.Source: §3.1 · p. 2
3.2 Design principles
- The system separates rule validity from query-pair proof discovery, makes cross-query representation alignment explicit, and treats the derivation as the result.Rule validity may be established separately through formal verification, verified libraries, upstream validation, or rule-specific testing; EquiTrace composes admitted rules rather than reproving them for each pair.Source: §3.2 · pp. 2–3
3.3 Proof model
- Given normalized plans and an environment Γ containing the schema, integrity constraints, and transformations, EquiTrace seeks derivations to compatible representations of a common witness.If no witness is found within the configured search budget, it returns UNKNOWN, which is not evidence of inequivalence.Source: §3.3 · p. 3
- In the EXISTS-versus-join example, the proof depends on uniqueness of S.rid: removing that constraint blocks the conversion and makes EquiTrace return UNKNOWN.The two branches use separate derivations to reach the same expression; the certificate records both branches, the side condition, and the witness.Source: §3.3 · p. 3, Figure 2 · p. 4
3.4 Architecture
- The architecture normalizes plans, applies bounded pair-coordinated alignment and preparation, then explores alternatives in a shared memo; search attempts may expand rules or budgets.Alignment is deterministic and does not itself establish equivalence; only a subsequent witness check or search can close the proof.Source: §3.4 · pp. 3–4
3.5 Proof replay
- For each successful proof, replay re-executes the recorded transformations and accepts the certificate only when both branches reproduce the common witness.Replay checks reproducibility; semantic validity of each rule remains a separate obligation.Source: §3.5 · p. 4
4 HOW FAR CAN REWRITE-BASED PROVING GO?
EquiTrace is evaluated across three query-pair corpora and compared with existing provers on LLM-generated rewrites. Coverage varies across corpus classes, and combining provers yields additional proofs.
4.1 Experiment setup
- The evaluation covers 3,233 pairs: 2,607 text-to-SQL-derived, 295 curated, and 331 LLM-generated rewrites.The LLM rewrites come from GPT-5.4 and SPA-32B-SI and span 167 original queries; originals have a median of six base tables and 18 relational operators.Source: §4.1 · p. 4
4.2 Coverage by corpus class
- EquiTrace proves 648/1,106 text-to-SQL pairs (58.6%), 229/266 curated pairs (86.1%), and 97/240 LLM rewrites (40.4%).The LLM rewrite labels indicate agreement on benchmark-tested instances, not semantic equivalence over all databases satisfying the schema.Source: Table 2 · p. 5, §4.2 · p. 5, §4.1 · p. 5
4.1 Experiment setup
- Execution-based agreement labels the text-to-SQL and LLM-generated corpora, while curated-suite labels are known from prior work.The fixed EquiTrace configuration includes 15 semantic canonicalization components, six bounded HEP rewrite programs, and 83 memo-search rules; parse failures, crashes, timeouts, and UNKNOWN count as misses.Source: §4.1 · pp. 4–5
4.3 Comparison with existing provers
- 97 pairs are proved by EquiTrace, versus 35 for QED and 38 for SQLSolver; their union proves 114.The comparison covers 240 expected-equivalent LLM-generated rewrite pairs.Source: Table 3 · p. 5, §4.3 · p. 5
4.2 Coverage by corpus class
- Coverage reaches 64/127 (50.4%) for SPA-32B-SI and 33/113 (29.2%) for GPT-5.4; the models more often produce different query forms.SPA-32B-SI more often produces CTE-and-join forms, while GPT-5.4 more often introduces EXISTS and IN structures that require additional alignment.Source: §4.2 · p. 5
5 WHAT LIMITS REWRITE-BASED PROOFS?
The analysis distinguishes transformations that appear in proofs from those necessary to preserve them, and finds that unresolved pairs reflect both search limits and gaps in rewrite coverage.
5.2 Remaining gaps
- 101 unresolved pairs hit a rule-application cap or timeout, while 39 saturate their memo without connecting the two plan memos.The former suggest search-capacity or pruning limits; the latter provide stronger evidence of a missing transformation or canonical representation.Source: Table 4 · p. 6, §5.2 · p. 6
5.1 Which transformations are most crucial?
- The study examines transformations in 764 recorded proofs, then disables each of the twenty most-used rules while holding the remaining configuration and search budgets unchanged.A pair is dependent on a transformation if the full configuration proves it but the configuration without that transformation does not.Source: §5.1 · pp. 5–6
- The join-region-ordering canonicalizer appears in 67 proofs and is necessary for 40, while ten of the twenty most-used transformations are individually necessary for no proof.Disabling all ten zero-loss transformations together preserves every proof among the 112 pairs that use at least one of them.Source: §5.1 · p. 6
5.2 Remaining gaps
- Queries joining at least five tables account for 76% of the gaps in both LLM-rewrite suites, versus 62% and 48% of their proved pairs.Wide join regions increase search cost and make structural alignment harder; prominent patterns also include outer joins, window rewrites, and scalar-versus-materialized aggregate CTE differences.Source: §5.2 · p. 6
6 CONCLUSION
EquiTrace turns query-rewriting knowledge into a standalone SQL equivalence prover, proving pairs across three workload classes and exposing replayable derivations. The experiments indicate that coverage depends on representation alignment and applying transformations under schema constraints.
6 CONCLUSION
- EquiTrace proves 974 of 1,612 expected-equivalent pairs across three workload classes, including 97 of 240 expected-equivalent LLM rewrites, compared with 38 for SQLSolver and 35 for QED.Recorded transformations, applicability conditions, and the common witness make the proofs inspectable and replayable.Source: §6 · p. 6