DBDoctor: LLM-Aided SMT Refutation of SQL Query Equivalence

Abstract

DBDoctor uses LLMs to propose counterexamples and rewrite queries into SMT-friendly forms, dramatically reducing the rate of "unsupported" query pairs from 100% to 1% and successfully refuting 47% of previously unverifiable cases.