Can the Rookies Cut the Tough Cookie? Exploring the Use of LLMs for SQL Equivalence Checking

TL;DR

This paper investigates the use of large language models (LLMs) for SQL query equivalence checking, introducing a new benchmark and demonstrating that LLMs significantly outperform formal models, though they struggle with non-equivalent pairs.

Contribution

The paper presents a novel benchmark for complex SQL equivalence checking and evaluates LLMs' reasoning capabilities, revealing their strengths and limitations in this domain.

Findings

LLMs achieve up to 82% accuracy on SQL equivalence tasks.

LLMs support full coverage of complex SQL queries beyond formal models.

LLMs show bias towards predicting equivalence, with poor performance on non-equivalent pairs.

Abstract

Equivalence checking of SQL queries is an intractable problem often encountered in settings ranging from grading SQL submissions to debugging query optimizers. Despite recent work toward developing practical solutions, only simple queries written using a small subset of SQL are supported, leaving the equivalence checking of sophisticated SQL queries at the mercy of intensive, potentially error-prone, manual analysis. In this paper, we explore how LLMs can be used to reason with SQL queries to address this challenging problem. Towards this, we introduce a novel, realistic, and sufficiently complex benchmark called SQLEquiQuest for SQL query equivalence checking that reflects real-world settings. We establish strong baselines for SQL equivalence checking by leveraging the ability of LLMs to reason with SQL queries. We conduct a detailed evaluation of several state-of-the-art LLMs using various prompting strategies and carefully constructed in-context learning examples, including logical plans generated by SQL query processors. Our empirical evaluation shows that LLMs go well beyond the current capabilities of formal models for SQL equivalence, going from a mere 30% supported query pairs to full coverage, achieving up to 82% accuracy on Spider+DIN. However, a critical limitation of LLMs revealed by our analysis is that they exhibit a strong bias for equivalence predictions, with consistently poor performance over non-equivalent pairs, opening a new direction for potential future research.