{"id":"d0ddf6fb-7d24-4bbc-8a27-0e7b4044c0e1","arxiv_id":"2412.05561","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"LLMs, especially GPT-4, can classify SQL query equivalence on complex real-world assignment queries far beyond formal tools' coverage, but they systematically over-predict equivalence.","lead":"The paper builds a new benchmark of complex SQL assignment queries and tests whether LLMs can decide when two SQL queries are equivalent. It reports that GPT-4 reaches about 80% accuracy while formal tools support only about 30% of the queried pairs, but it also finds a strong bias toward calling queries equivalent.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Execution-based ground-truth labels may make the reported 82%/61% accuracy an upper bound; formal validation of 'equivalent' labels is needed.","rationale":"The reader and I converge on the same load-bearing point: the ground truth is execution-based rather than formal all-instance equivalence. I agree with the CONDITIONAL verdict because the paper's central descriptive finding, that LLMs other than GPT-4 are strongly biased toward 'equivalent,' survives the label concern: pairs labeled non-equivalent have a concrete execution witness, so the NEQ accuracy columns and the bias observation are not invalidated. What is threatened is the absolute accuracy claim, since false-equivalent labels inflate the EQ class that dominates both benchmarks and that LLMs already over-predict. A focused label-validation study would settle whether the 82%/61% figures are approximately correct or simply optimistic upper bounds. I did not find a second concern of comparable weight: the few-shot examples may be drawn from the test set, but the headline result is also obtained with basic and CoT prompting, and the code release improves reproducibility even though no formal verification accompanies the benchmark.","tokens_in":24496,"tokens_out":5588,"duration_ms":53785,"concrete_test":"Independently re-label a sample of the 'equivalent' pairs. For SQLEquiQuest: (i) generate multiple fresh database instances, including adversarial cases with NULLs, duplicate rows, empty relations, mixed collations/case, and boundary values near LIMIT/ORDER BY tie-breaks; execute both queries in each instance; (ii) for the subset SQLSolver supports (~30%), run the verifier and compare. If any labeled-equivalent pair differs on a new instance or yields a verifier counterexample, recompute Table 2 after moving that pair to non-equivalent. For Spider+DIN: augment the distilled test suite with additional instances and rerun test-suite-sql-eval; flag all label flips from equivalent to non-equivalent. Quantify the shift in GPT-4 EQ and overall accuracy; if the shift is above about 5 percentage points, the headline 'up to 82%' should be replaced by a label-conditional figure.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 2 defines SQL equivalence as identical outputs on every instance of the schema. The benchmark labels, however, are not produced by that definition. For Spider+DIN (Section C.1) equivalence was decided with test-suite-sql-eval, a finite test suite; for SQLEquiQuest (Section 3.1) teaching assistants executed queries on 'a large database instance designed to account for all potential corner cases,' with no proof that this one instance separates all inequivalent pairs. A finite execution check is sound for non-equivalence (differing outputs certify a witness) but unsound for equivalence: agreeing on the chosen instance(s) only shows equivalence on that data. The 'equivalent' classes in both benchmarks are therefore a superset of true equivalence (Spider+DIN: 385 of 574 pairs; SQLEquiQuest: 307 of 499 pairs). Because most LLMs are biased toward predicting 'equivalent,' false-equivalent labels directly inflate EQ accuracy and the weighted overall accuracy, including the headline 82% and 61% numbers. The NEQ accuracies are less vulnerable, since an execution witness makes non-equivalence certain, which is why the paper's bias finding is more robust than its absolute accuracy claims. This is a missing-support issue the manuscript itself exposes: Section 3.1 asserts but does not demonstrate that the instance covers all corner cases, and Appendix C.1 relies on an execution metric for ground truth.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces SQLEquiQuest, a new benchmark of SQL query equivalence pairs drawn from DBMS assignment submissions, and evaluates five LLMs with four prompting strategies on Calcite, Spider+DIN, and SQLEquiQuest. It reports that LLMs, particularly GPT-4, achieve accuracy up to 82% on Spider+DIN and 61% on SQLEquiQuest, considerably extending coverage over formal tools, but that most LLMs are strongly biased toward predicting equivalence. The paper also studies logical-plan augmentation and fine-tuning of Code Llama-13B.","tokens_in":24794,"tokens_out":7184,"duration_ms":64015,"significance":"The benchmark is a useful resource and the paper is among the first to systematically study LLMs on this task; the NEQ-bias finding is robust and actionable, and the code is publicly available. However, the central accuracy claims are compromised by execution-based ground truth, in-sample prompt tuning, and few-shot examples drawn from the test set. The formal-tool comparison is interesting but inherits these issues.","major_comments":[{"comment":"The ground-truth labels in both benchmarks are not the formal all-instance equivalence defined in Section 2. SQLEquiQuest labels were assigned by executing queries on 'a large database instance designed to account for all potential corner cases,' and Spider+DIN labels were assigned with test-suite-sql-eval. A finite execution check is sound only for non-equivalence; agreement on a single instance or test suite does not prove equivalence. Because the majority of pairs are labeled equivalent (307/499 in SQLEquiQuest, 385/574 in Spider+DIN), any false-equivalent labels inflate the EQ accuracies and the GM numbers in Tables 2 and 3, including the headline 82% and 61%. The manuscript itself exposes this gap: Section 3.1 asserts, but does not demonstrate, that the instance covers all corner cases. Please provide formal validation of the equivalent labels (e.g., by running a formal prover on supported pairs or by giving a separation argument), or restrict all claims to execution-based equivalence and make the EQ/NEQ distinction the primary reporting dimension.","section":"§3.1, §C.1, §2"},{"comment":"The authors state that all prompts were 'carefully designed and refined through iterative testing with each LLM used.' Since the same benchmarks are used both for prompt development and for final scoring, the reported numbers are in-sample. This is particularly problematic for comparing prompting strategies: the differences among P1-P4 may reflect overfitting to the specific test distribution rather than general capability. Please use a held-out development set for prompt tuning and report results on a separate test split, or explicitly describe the reported numbers as upper bounds.","section":"§5.4"},{"comment":"Few-shot examples were 'randomly sampled from the dataset and then fixed for all test samples.' Drawing in-context demonstrations from the same benchmark that is being scored leaks information about the test distribution (and potentially about the exact query pairs), inflating few-shot accuracy. Use few-shot examples from a disjoint development set or from query pairs that are excluded from the evaluation set.","section":"§4.1 (P3), §B.3"},{"comment":"The final labels are produced by a GPT-family classifier with no reported validation; the 'Unknown' class is treated as a negative result. Classification errors propagate directly into Tables 2 and 3. Please report the classifier's accuracy on a human-annotated sample of outputs, and state explicitly how 'Unknown' is counted in the accuracy definition.","section":"§4.2, §B.5"},{"comment":"No repeated runs, confidence intervals, or significance tests are reported. All API LLMs are sampled with temperature 0.2, so the single-run differences (e.g., GPT-4 vs. GPT-3.5 on Question 3 with CoT) may be within run-to-run variation. Please provide multiple runs or bootstrap intervals and avoid drawing conclusions from small numerical gaps.","section":"Tables 2 and 3"}],"minor_comments":[{"comment":"The text says 'for each question in Spider+DIN' but the table is for SQLEquiQuest; correct the reference.","section":"§3.1, Table 1"},{"comment":"The hyperparameter 'do sample' should be 'do_sample' to match standard PyTorch/HuggingFace naming.","section":"§D.1"},{"comment":"The Brown et al. 2020a and 2020b entries are duplicate citations of the same work and should be merged.","section":"References"},{"comment":"The radial axis is described as 'the average number of corresponding feature'; this should be 'the average number of corresponding features per query' for clarity.","section":"Figure 2 caption"},{"comment":"The phrase 'full coverage' should be qualified: LLMs produce an output for every pair, but 'coverage' in Table 4 refers to the tools' ability to verify, not to the correctness of the LLM's predictions; a direct coverage comparison is therefore misleading.","section":"§5.2"}],"recommendation":"major_revision","confidential_remarks":"The paper is likely of interest to the DB/LLM community, and the code release is a plus. The execution-based labeling issue is the main risk; if the authors can re-validate the EQ labels on a subset using formal tools, or clearly reframe the claims, the paper could be resubmitted successfully. The benchmark is small (five questions) and from a single institution; the novelty may be moderate for a journal."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: the SQLEquiQuest benchmark is a genuine contribution, and the observed equivalence-prediction bias is real. The headline accuracy numbers, though, are upper bounds, not point estimates, because both benchmarks define \"equivalent\" by agreement on one database instance (or a finite test suite), while the paper's own definition is all-instance equivalence. Add prompt tuning on the test benchmarks and you have a paper whose qualitative findings I trust but whose absolute numbers I wouldn't quote.\n\nWhat's new and good: SQLEquiQuest is real student submissions on five instructor-designed questions with a schema built to avoid LLM training-data contamination; it fills a gap. The evaluation across five LLMs and four prompting styles is broad. The logical-plan augmentation is a sensible idea and helps, especially for Code Llama-7B. The fine-tuning result (Code Llama-13B gains NEQ accuracy, loses a bit of EQ) is interesting. The consistent bias toward \"equivalent\" across nearly all models is the most durable result, and it holds even if labels shift. Code is released, which helps reproducibility.\n\nSoft spots, in order of severity. First, ground-truth labels. For Spider+DIN, equivalence comes from test-suite-sql-eval; for SQLEquiQuest, from running on one large instance. A difference in outputs certifies non-equivalence, but agreement only certifies equivalence on that data. Since most models over-predict equivalence, false-equivalent labels inflate EQ and geometric-mean accuracy. The 82% and 61% should be treated as ceilings, and the benchmark would be stronger if a sample of equivalent pairs were checked on multiple instances or with a formal tool. Second, the prompting setup leaks test information: Section 5.4 admits prompts were iteratively tuned on each LLM, and few-shot examples were sampled from the same dataset and fixed. That is tuning to the test distribution. Third, outputs go through a GPT-family classifier with \"Unknown\" treated as negative; that's a reasonable engineering choice but it makes the numbers partly about GPT's classification, not solely the queried model. Fourth, no repeated runs or error bars are given. Minor: the paper says it corrects LLM-SQL-Solver's metric but I don't see that comparison table.\n\nWho it's for: people building SQL grading or text-to-SQL validation tools, and anyone benchmarking LLM SQL reasoning. It deserves a serious referee; the benchmark and bias finding are worth publishing after major revision, with the absolute accuracy claims rebased.","headline":"A genuine new benchmark and a robust equivalence-bias finding; the headline accuracy numbers are upper bounds because ground truth is execution-based and prompts were tuned on the test benchmarks.","tokens_in":25288,"tokens_out":2656,"would_cite":true,"duration_ms":25598,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Large language models can classify SQL query equivalence on realistic, complex queries that formal tools cannot handle, with GPT-4 reaching about 82% accuracy on Spider+DIN and about 60% on the new SQLEquiQuest benchmark, while most other…","keywords":["SQL query equivalence","large language models","SQLEquiQuest","prompting strategies","logical plan","equivalence bias","Spider+DIN","text-to-SQL"],"falsifier":"Take any pair SQLEquiQuest labels equivalent and search exhaustively over all small database instances for the schema, or use a solver like SQLSolver on the formal all-instances definition; if any instance yields different outputs, that label is wrong and the reported accuracy is measured against a flawed ground truth.","tokens_in":24322,"feed_emoji":"🗄️","tokens_out":7853,"duration_ms":59904,"temperature":0.7,"pith_summary":"The paper tries to establish that large language models can serve as practical SQL query equivalence checkers for realistic, complex queries that formal verification tools cannot process. It reports that GPT-4 reaches up to 82% accuracy on Spider+DIN and about 60% accuracy on SQLEquiQuest, a new benchmark built from graduate-level database assignment submissions, whereas formal tools support only about 30% of SQLEquiQuest pairs. The paper also claims that prompting strategies, in-context examples, and unoptimized logical plans improve LLM performance. A central caveat is that most tested LLMs are biased toward predicting equivalence, performing well on equivalent pairs but poorly on non-equivalent ones.","feed_headline":"GPT-4 checks SQL equivalence at 82 percent on real query pairs","feed_subtitle":"Formal tools cover 30 percent of these pairs; GPT-4 handles nearly all, though most LLMs are biased to say 'equivalent'.","key_machinery":"The central object is the prompt-to-classifier pipeline: four prompting strategies (basic, chain-of-thought, few-shot, and multi-stage chain-of-thought) feed SQL pairs plus optional unoptimized logical plans from Apache Calcite into an LLM, and a separate GPT classifier maps verbose outputs to 'Equivalent', 'Non-Equivalent', or 'Unknown'. The load-bearing mechanism is the in-context reasoning scaffold: the logical plan makes query semantics explicit, the step-by-step prompts force intermediate explanations, and few-shot examples provide ground-truth demonstrations, together letting the LLM align its equivalence judgment with the execution-based labels. The benchmark SQLEquiQuest is the other central object: a dataset of student assignment submissions against instructor-written ground-truth queries, labeled by execution on a large test database instance.","core_discovery":"The central claim is that LLMs, treated as black-box experts, go beyond the coverage of formal SQL equivalence checkers: whereas SQLSolver supports only about 30% of SQLEquiQuest pairs and VeriEQL supports 2.8%, GPT-4 with the best prompting strategy correctly classifies roughly 82% of Spider+DIN pairs and about 60% of SQLEquiQuest pairs. The paper also finds that this capability is uneven: most tested LLMs classify almost all equivalent pairs correctly but systematically mislabel non-equivalent pairs as equivalent, whereas GPT-4 maintains much stronger performance on non-equivalent pairs. Adding an unoptimized logical plan from Apache Calcite to the prompt generally improves results, and fine-tuning Code Llama-13B substantially improves non-equivalent detection.","pith_inferences":["Because SQLEquiQuest and Spider+DIN labels come from execution on one test database or test suite rather than all possible databases, the reported accuracies likely overstate true logical equivalence; a more rigorous benchmark would certify labels by exhaustive search or formal proofs on small schemas.","The pervasive equivalence bias suggests a testable extension: ask the LLM to generate a counterexample database instance for each predicted non-equivalence, then execute both queries on it; if it cannot produce one, the prediction should be downgraded.","A hybrid pipeline is a natural next step: use a fast biased LLM to filter obviously equivalent pairs and route uncertain or non-equivalent pairs to a formal tool like SQLSolver, potentially recovering formal guarantees where the LLM alone cannot.","The paper's finding that GPT-4 performs poorly on Calcite despite strong performance elsewhere hints that training-data overlap and syntactic style, not just semantic difficulty, drive LLM equivalence judgments; a contamination-controlled benchmark would be needed to separate these factors."],"forward_implications":["GPT-4 can classify SQL equivalence on essentially all query pairs in these benchmarks, where formal tools support at most 30%, so LLM-based checking is a viable first-line tool for realistic query pairs.","On Spider+DIN, adding a logical plan to the prompt improves geometric-mean accuracy for most models and prompting strategies, with the largest gains for the smallest model, Code Llama-7B.","Most LLMs are biased toward predicting equivalence, with near-zero accuracy on non-equivalent pairs, so any practical deployment must guard against this by calibration or fine-tuning.","Fine-tuning Code Llama-13B on labeled equivalence pairs raises non-equivalent accuracy substantially (for example, from 0.5% to 23.8% under basic prompting) while roughly preserving equivalent-pair performance.","GPT-4 correctly classifies more than 80% of the SQLEquiQuest pairs SQLSolver supports and about 52% of the pairs SQLSolver does not support, indicating the LLM approach extends rather than merely replaces formal tools."],"supporting_citations":[{"why":"SQLSolver, the formal checker whose 30% coverage on SQLEquiQuest is the baseline the paper claims to surpass.","marker":"Ding et al., 2023"},{"why":"VeriEQL, the formal verifier that supports only 2.8% of SQLEquiQuest pairs, used as a second baseline.","marker":"He et al., 2024"},{"why":"LLM-SQL-Solver, the prior LLM approach whose Spider+DIN dataset construction and evaluation metric this paper builds on and corrects.","marker":"Zhao et al., 2023"},{"why":"DIN-SQL, the text-to-SQL model used to generate the additional queries in Spider+DIN.","marker":"Pourreza & Rafiei, 2023"},{"why":"test-suit-sql-eval, the execution-based evaluator that produces the equivalence labels for Spider+DIN.","marker":"Zhong et al., 2020"},{"why":"Spider, the base benchmark from which Spider+DIN query pairs are derived.","marker":"Yu et al., 2018"},{"why":"Cosette and its Exams benchmark, the earlier formal prover and small exam dataset that SQLEquiQuest extends.","marker":"Chu et al., 2017"}],"fun_headline_variants":["LLMs outdo formal SQL checkers: 30% to 82% accuracy","GPT-4 solves 82% of SQL equivalence checks, formal tools 30%","SQL equivalence: LLMs leap from 30% to 82% coverage","LLMs beat SQL checkers, but bias toward 'equivalent' pairs"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The ground-truth equivalence labels in both main benchmarks come from running queries on one large test database or test suite, and the paper provides no proof that this instance separates every pair of queries that differ on some database.","fun_headline_variants_meta":{"raw":{"variants":["LLMs outdo formal SQL checkers: 30% to 82% accuracy","GPT-4 solves 82% of SQL equivalence checks, formal tools 30%","SQL equivalence: LLMs leap from 30% to 82% coverage","LLMs beat SQL checkers, but bias toward 'equivalent' pairs"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000208,"raw_usage":{"total_tokens":1408,"prompt_tokens":956,"completion_tokens":452,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":572,"completion_tokens_details":{"reasoning_tokens":366}},"tokens_in":572,"tokens_out":452,"duration_ms":4090,"temperature":1.0,"reasoning_tokens":366,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T20:35:18.189150+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take any pair SQLEquiQuest labels equivalent and search exhaustively over all small database instances for the schema, or use a solver like SQLSolver on the formal all-instances definition; if any instance yields different outputs, that label is wrong and the reported accuracy is measured against a flawed ground truth.","supporting_citations":[{"cited_title":"Semantic evaluation for text-to-sql with distilled test suite","cited_arxiv_id":null,"evidence_quote":"test-suit-sql-eval, the execution-based evaluator that produces the equivalence labels for Spider+DIN."},{"cited_title":"Cosette: An A utomated P rover for SQL","cited_arxiv_id":null,"evidence_quote":"Cosette and its Exams benchmark, the earlier formal prover and small exam dataset that SQLEquiQuest extends."}],"review_version":1}