SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints

SpotIt+ is een open-source tool die Text-to-SQL-systemen evalueert door middel van gebonden equivalentieverificatie en een door LLM's ondersteunde constraint-mining pipeline om realistische database-instanties te genereren die verschillen tussen gegenereerde en grondware SQL-query's blootleggen.

De kern

Stel je voor dat je een zeer slimme, maar soms wat ongeduldige assistent hebt die vloeiend twee talen spreekt: Nederlands (wat jij vraagt) en SQL (de taal van databases). Je vraagt hem: "Laat me zien wie de klanten zijn met een inkomen tussen de 8.000 en 9.000 euro."

De assistent schrijft een opdracht op (een SQL-query) en geeft die aan de database. De database doet zijn werk en geeft een lijstje terug. Tot nu toe lijkt alles goed.

Maar hier is het probleem: Hoe weet je zeker dat de assistent de opdracht écht goed heeft begrepen?

In de wereld van computers wordt dit vaak getest door de uitkomst van de assistent te vergelijken met die van een menselijke expert op een vast, klein voorbeeld-database. Als de lijsten op dat ene voorbeeld hetzelfde zijn, zeggen we: "Goed gedaan!"

SpotIt+ is een nieuw, slim gereedschap dat zegt: "Wacht even, dat is niet genoeg. Die lijsten kunnen toevallig hetzelfde zijn op dat ene voorbeeld, terwijl de assistent de opdracht fundamenteel verkeerd heeft begrepen."

Hier is hoe SpotIt+ werkt, vertaald naar alledaagse taal:

1. De "Tijdmachine" voor Databases (Bounded Verification)

Stel je voor dat je wilt weten of twee recepten voor een taart echt hetzelfde zijn. Je kunt ze niet alleen vergelijken op één specifieke dag met één specifieke bakkerij. Je moet ze testen in alle mogelijke keukens met alle mogelijke ingrediënten.

SpotIt+ doet precies dit, maar dan met databases. Het is een soort tijdmachine die duizenden verschillende, denkbeeldige databases creëert om te kijken of de assistent's antwoord en het juiste antwoord altijd hetzelfde blijven.

• Als ze op elke denkbeeldige situatie hetzelfde zijn: Gefeliciteerd, het is correct.
• Als ze op één situatie verschillend zijn: SpotIt+ stopt en roept: "Hé, hier is een fout!"

2. Het Probleem met de "Gekke" Fouten

In het verleden was er een probleem met deze tijdmachine. Soms vond hij een fout, maar was die fout zo gek dat hij in de echte wereld nooit zou gebeuren.

Het voorbeeld uit het papier:
De assistent zegt: "Inkomens moeten groter zijn dan 8.000."
De expert zegt: "Inkomens moeten tussen 8.000 en 9.000 liggen."

Op de standaard testdatabase staan alleen mensen met een inkomen van 8.100, 8.500 en 9.000. Beide antwoorden lijken hier perfect.
Maar de oude tijdmachine (zonder extra regels) vond een "tegenbewijs" met een persoon die een inkomen van 8.000,00 had.

• Oude methode: "Zie je wel! De assistent is fout, want hij sloot 8.000 uit!"
• Realiteit: In deze specifieke database bestaan mensen met precies 8.000 euro inkomen gewoon niet. Het is een "kinderachtige" fout die in de praktijk nooit voorkomt. Het is alsof je een auto test op een racecircuit en zegt: "Deze auto is slecht, want hij kan niet over een muur van 5 meter springen." Nee, auto's zijn niet gemaakt om muren te springen.

3. De Oplossing: De "Werkelijke Regels" (Constraint Mining)

SpotIt+ is slimmer. Het kijkt eerst naar de database en vraagt zich af: "Wat zijn de echte, logische regels hier?"

Het pakt de database en zoekt naar patronen, zoals een detective die een dossier bestudeert:

• "Ah, in deze database hebben alle mensen een landcode die bestaat uit 2 letters."
• "Alle leeftijden liggen tussen 18 en 90."
• "Iedereen die een auto heeft, heeft ook een rijbewijs."

SpotIt+ pakt deze regels en zegt tegen de tijdmachine: "Zoek niet naar gekke situaties met muren van 5 meter of mensen van 200 jaar oud. Zoek alleen naar fouten die echt kunnen gebeuren binnen de regels van deze wereld."

4. De "Slimme Assistent" (LLM)

Soms is de detective (SpotIt+) te streng. Hij ziet dat in de testdatabase alle leeftijden tussen 30 en 60 liggen, en zegt dan: "Nee, mensen kunnen hier nooit ouder dan 60 worden." Dat is natuurlijk onzin.

Daarom heeft SpotIt+ een LLM (een zeer slimme taal-assistent) ingeschakeld als "rechter".

• SpotIt+: "Ik heb gezien dat de leeftijd 30-60 is."
• LLM: "Wacht, dit is een database van werknemers in een kantoor. Het is logisch dat ze tussen 30 en 60 zijn, maar dat betekent niet dat mensen ouder dan 60 onmogelijk zijn. Laat de grens iets ruimer zijn, bijvoorbeeld 0 tot 120."

De LLM corrigeert de regels zodat ze realistisch blijven, maar niet onmogelijk.

Waarom is dit belangrijk?

Voor bedrijven die chatbots of slimme assistenten bouwen, is het cruciaal om te weten of die systemen echt slim zijn.

• De oude manier (Testen op één database): Is alsof je een piloot test door hem één keer op een rechte landingsbaan te laten vliegen. Hij slaagt, maar kan misschien niet in een storm vliegen.
• De nieuwe manier (SpotIt+): Test de piloot in duizenden denkbeeldige stormen, maar alleen in stormen die echt kunnen voorkomen (geen stormen met blauwe regen of vliegende koeien).

Conclusie:
SpotIt+ is een gereedschap dat zorgt dat we niet worden misleid door "toevallige" successen. Het zoekt naar de echte fouten in slimme databasesystemen, door te kijken naar wat er in de echte wereld mogelijk is, en niet alleen naar wat er op een stukje papier staat. Het maakt de test van deze systemen eerlijker, slimmer en veiliger.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "SpotIt+: Verification-based Text-to-SQL Evaluation with Database Constraints" in het Nederlands.

Probleemstelling

Het evalueren van Text-to-SQL-systemen (het vertalen van natuurlijke taal naar SQL-query's) is een kritieke uitdaging. Bestaande evaluatieplatforms, zoals die gebruikt worden voor de BIRD-dataset, vertrouwen voornamelijk op test-gebaseerde evaluatie. Hierbij wordt de gegenereerde SQL-query uitgevoerd op een vaste testdatabase en worden de resultaten vergeleken met die van de "gold" (juiste) query.

Deze aanpak heeft een fundamenteel nadeel: twee niet-equivalente queries kunnen op een specifieke testdatabase exact dezelfde resultaten opleveren. Dit leidt tot een te optimistische inschatting van de nauwkeurigheid van een model.

Eerdere werken hebben voorgesteld om verificatie-gebaseerde evaluatie te gebruiken, waarbij een SMT-oplosser (Satisfiability Modulo Theories) systematisch zoekt naar database-instanties die de gegenereerde query en de gold-query van elkaar onderscheiden (counterexamples). Echter, een groot probleem met deze methode is de praktische relevantie van de gevonden counterexamples. Zonder extra beperkingen genereert de verifier vaak onrealistische databases met pathologische randgevallen (bijvoorbeeld waarden die in de echte wereld onmogelijk zijn, zoals een leeftijd van -5 of een landcode die niet bestaat). Deze "nep"-fouten zijn technisch correct, maar bieden weinig inzicht voor ontwikkelaars.

Methodologie: SpotIt+

SpotIt+ is een open-source tool die de verificatie-gebaseerde aanpak verbetert door database-beperkingen (constraints) te integreren die zijn afgeleid van de voorbeelddatabases. De workflow bestaat uit de volgende stappen:

1. Constraint Mining (Specifatie Mining):
   Het systeem analyseert de voorbeelddatabase om vijf soorten beperkingen automatisch af te leiden:

   • Bereikbeperkingen (Range Constraints): Minima en maxima voor numerieke kolommen.
   • Categorische beperkingen (Categorical Constraints): Een eindige set van toegestane waarden voor kolommen met weinig unieke waarden.
   • NotNull-beperkingen: Kolommen die geen null-waarden mogen bevatten.
   • Functionele afhankelijkheden (Functional Dependencies): Relaties waarbij één kolomset een andere uniek bepaalt.
   • Volgorde-afhankelijkheden (Ordering Dependencies): Inequaliteitsrelaties tussen numerieke kolommen.

2. LLM-validatie en Reparatie:
   Pure regelgebaseerde mining kan leiden tot overfitting op de specifieke testdata (bijv. als de testdata alleen leeftijden van 30-60 bevat, zou een strakke beperking [30, 60] gelden, wat onrealistisch is voor een algemene database).

   • SpotIt+ gebruikt een Large Language Model (LLM) om de gemineerde beperkingen te valideren.
   • Het LLM beoordeelt of een beperking een echte domeineigenschap is (bijv. "landcodes zijn uniek") of een artefact van de testdata.
   • Het LLM kan ook "repareren": het kan een te restrictieve bereikbeperking verbreden (bijv. van [30, 60] naar [0, 120] voor leeftijden) om realistische counterexamples mogelijk te maken.

3. Beperkte Equivalentieverificatie:
   De gevalideerde beperkingen worden gecodeerd als SMT-beperkingen in de verificatie-engine (VeriEQL). De engine zoekt vervolgens binnen een begrende zoekruimte (bijv. databases met maximaal 5 rijen per tabel) naar een database-instantie die voldoet aan deze beperkingen, maar waar de gegenereerde query en de gold-query verschillende resultaten opleveren.

Belangrijkste Bijdragen

1. SpotIt+ Tool: Een open-source implementatie voor Text-to-SQL-evaluatie die verificatie combineert met constraint mining.
2. Constraint Extraction Pipeline: Een innovatieve pipeline die regelgebaseerde mining combineert met LLM-validatie en -reparatie om realistische domeinbeperkingen te extraheren.
3. Empirische Validatie: Een uitgebreide evaluatie op de BIRD-dataset die aantoont dat deze aanpak de realisme van counterexamples verbetert zonder de detectiecapaciteit van fouten te verliezen.

Resultaten

De auteurs hebben SpotIt+ gebruikt om 10 state-of-the-art Text-to-SQL-methoden te evalueren op de BIRD-dev dataset (1.533 vragen).

• Detectie van Discrepanties: Alle verificatie-gebaseerde methoden (SpotIt, SpotIt+-noV, SpotIt+) vonden aanzienlijk meer discrepanties tussen gegenereerde en gold queries dan de traditionele test-gebaseerde evaluatie (EX-test).
• Realisme:
  • SpotIt (zonder constraints) vond veel counterexamples, maar deze waren vaak onrealistisch (bijv. met NULL-waarden waar de data aangeeft dat deze niet voorkomen, of extreme numerieke waarden).
  • SpotIt+-noV (met constraints, maar zonder LLM) elimineerde onrealistische gevallen, maar was soms te restrictief en miste soms echte fouten omdat de constraints te strak waren.
  • SpotIt+ (met LLM-validatie) leverde de beste balans. Het produceerde kwalitatief realistischere counterexamples (bijv. met geldige categorieën zoals 'Secretary' in plaats van willekeurige nummers) en herstelde soms fouten die door te strake constraints waren onderdrukt.
• Efficiëntie: De tool is zeer efficiënt. De gemiddelde tijd om een counterexample te vinden is minder dan 2 seconden (0.9s voor de volledige SpotIt+ configuratie), wat aangeeft dat de extra constraints de zoekruimte effectief verkleinen zonder de prestaties te schaden.
• Ranking: De rangschikking van de modellen veranderde enigszins ten opzichte van de EX-test, wat suggereert dat test-gebaseerde evaluatie sommige modellen ten onrechte hoog scoort.

Betekenis en Impact

SpotIt+ biedt een significante stap voorwaarts in de betrouwbaarheid van Text-to-SQL-evaluatie. Door te zorgen dat gevonden fouten praktisch relevant zijn, helpt het ontwikkelaars om echte zwakke plekken in hun modellen te identificeren in plaats van zich te richten op pathologische randgevallen.

De tool is direct toepasbaar op bestaande benchmarks zoals BIRD en Spider. De integratie van LLM's voor het valideren van database-beperkingen opent een nieuwe richting voor hybride systemen die formele verificatie combineren met semantisch begrip van domeinkennis. Dit is cruciaal voor het bouwen van robuuste AI-assistenten in kritieke domeinen zoals gezondheidszorg en financiën, waar SQL-fouten ernstige gevolgen kunnen hebben.