SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification

Dit paper introduceert SpotIt, een nieuwe evaluatiepipeline die formele verificatie gebruikt om onbetrouwbare testgebaseerde Text-to-SQL-evaluaties te verbeteren door actief databases te zoeken die gegenereerde en grondwaarheid SQL-query's onderscheiden.

De kern

SPOTIT: De "Waarheidszoeker" voor Database-Vragen

Stel je voor dat je een zeer slimme butler hebt die jouw vragen in gewone taal (Nederlands, Engels, etc.) omzet in een complexe instructie voor een gigantische bibliotheek. Die instructie is een SQL-query (een database-vraag). Je vraagt bijvoorbeeld: "Wie is de jongste patiënt met een abnormale bloedwaarde?" en de butler schrijft een code op die de bibliotheek moet doorzoeken.

Nu komt het probleem: Hoe weet je of de butler het goed heeft gedaan?

Het oude probleem: De "Vaste Test"

Tot nu toe keken we naar de butler door een statische test te doen. We gaven de butler een specifieke, vaste lijst met patiënten (een test-database) en zagen of het antwoord klopte.

• Het gevaar: Stel, de butler schrijft een verkeerde code, maar op die specifieke lijst met patiënten geeft hij per ongeluk het juiste antwoord. Het is alsof je een sleutel hebt die per toeval in een vergrendelde deur past, alleen omdat de deur op dat moment open stond. De test zegt: "Goed gedaan!", maar de butler heeft eigenlijk niet geleerd hoe de deur werkt. Hij heeft alleen geluk gehad met die ene situatie.

De nieuwe oplossing: SPOTIT (De "Tweestrijd")

De auteurs van dit paper hebben SPOTIT bedacht. In plaats van te wachten op een vaste lijst, sturen ze een formele "detective" (een wiskundig bewijsprogramma) de wereld in om actief te zoeken naar een situatie waarin de butler het fout doet.

Hier is hoe het werkt, met een paar creatieve vergelijkingen:

1. De "Waarheidszoeker" (Formele verificatie)

SPOTIT is als een super-intelligente detective die niet kijkt naar één foto, maar naar alle mogelijke werelden.

• De oude manier: Kijkt naar één foto van een feestje. Als iedereen lacht, is het feest geslaagd.
• SPOTIT: Vraagt zich af: "Zou dit feestje ook mislukken als we de muziek harder zetten? Of als we een andere groep mensen uitnodigen?"
• De detective probeert een tegenvoorbeeld te vinden: een specifieke situatie (een database) waarin de butler's antwoord verschilt van het juiste antwoord. Als hij zo'n situatie vindt, is de butler onbetrouwbaar, zelfs als hij op de oude test goed zat.

2. De "Taal-Vertaler" (SQL en Wiskunde)

SQL is een taal die databases begrijpen, maar voor wiskundige computers is het soms als Chinees.

• De auteurs hebben de detective (een programma genaamd VERIEQL) getraind om niet alleen cijfers te begrijpen, maar ook data (zoals geboortedata) en woorden (zoals namen of adressen).
• Ze hebben een nieuwe "woordenboek" gemaakt voor de detective, zodat hij precies weet hoe een computer omgaat met dingen als "Is 2023-01-01 groter dan 2022?" of "Begint deze naam met 'A'?". Zonder dit zou de detective denken dat "10" groter is dan "2" (want 1 is groter dan 2 in de eerste letter), wat in de echte wereld fout is.

3. De Verassende Bevinding: De Meester is ook fout!

Dit is het meest interessante deel van het verhaal.
Toen ze SPOTIT gebruikten om de beste butlers (AI-modellen) te testen, ontdekten ze iets verrassends:

• Vaak dachten we dat de butler het fout had omdat zijn antwoord anders was dan het "gouden antwoord" (het antwoord van de menselijke expert).
• Maar SPOTIT toonde aan dat soms het "gouden antwoord" zelf fout was!
• De metafoor: Stel je voor dat je een quiz doet. De leraar (de expert) heeft een antwoord in zijn antwoordmodel staan. Jij geeft een ander antwoord. De leraar zegt: "Fout!". Maar SPOTIT (de detective) komt binnen en zegt: "Wacht even, als we de regels van de quiz precies bekijken, heeft de leraar het mis. Jij had gelijk, of de vraag was zo vaag dat beide antwoorden kunnen kloppen."

Wat betekent dit voor de wereld?

1. Betrouwbaardere AI: We kunnen nu veel beter zien of een AI echt slim is, of dat hij alleen maar geluk had met de testvragen.
2. Betere Examens: Het blijkt dat veel "examenvragen" (de test-databases) zelf fouten bevatten of dubbelzinnig zijn. SPOTIT helpt ons die fouten op te sporen en de examens te verbeteren.
3. Veiligheid: In de echte wereld (zoals in ziekenhuizen of banken) kunnen fouten in database-vragen leiden tot grote problemen. SPOTIT zorgt ervoor dat we geen "gelukkige fouten" accepteren als waarheid.

Kortom: SPOTIT is niet zomaar een nieuwe test; het is een waarheidszoeker die actief op zoek gaat naar de zwakke plekken in zowel de AI als de examens zelf, zodat we zeker weten dat de antwoorden echt kloppen, niet alleen op papier, maar in elke mogelijke situatie.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "SPOTIT: EVALUATING TEXT-TO-SQL EVALUATION WITH FORMAL VERIFICATION", geschreven in het Nederlands.

Titel: SPOTIT: Het evalueren van Text-to-SQL-evaluatie met formele verificatie

Publicatie: ICLR 2026

---

1. Het Probleem

Text-to-SQL-systemen vertalen natuurlijke taalvragen naar uitvoerbare SQL-query's. De prestaties van deze systemen worden momenteel bijna uitsluitend beoordeeld via test-gebaseerde evaluatie. Hierbij wordt de gegenereerde SQL-query uitgevoerd op een statische testdatabase en worden de resultaten vergeleken met die van een door mensen gemaakte "ground truth" (gouden SQL).

De auteurs identificeren een fundamenteel tekortkoming in deze aanpak:

• Toevallige overeenkomst: Twee verschillende SQL-query's kunnen toevallig hetzelfde resultaat opleveren op een specifieke, statische testdatabase, terwijl ze semantisch verschillend zijn.
• Optimistische evaluatie: Dit leidt tot een overschatting van de nauwkeurigheid van Text-to-SQL-modellen.
• Onbekende fouten in ground truth: De huidige evaluatie gaat er ten onrechte van uit dat de menselijke ground truth altijd correct is. In werkelijkheid bevatten benchmarks vaak fouten in de gouden SQL of zijn de vragen ambigu.

2. Methodologie: SPOTIT

Het paper introduceert SPOTIT (Search-based Text-to-SQL Evaluation), een nieuwe evaluatiepijplijn die gebruikmaakt van formele verificatie in plaats van statische testen.

Kernprincipes:

• Zoekgerichte Evaluatie: In plaats van te kijken of twee query's op één database hetzelfde resultaat geven, probeert SPOTIT actief een tegenvoorbeelddatabase (counterexample database) te vinden waarop de gegenereerde query en de gouden query verschillende resultaten opleveren.
• Gelimiteerde Verificatie (Bounded Verification): Omdat volledige equivalentieverificatie voor SQL over het algemeen onbeslisbaar is, gebruikt SPOTIT SMT-gebaseerde (Satisfiability Modulo Theories) gebonden verificatie. Het zoekt naar databases met een maximale grootte $K$ (bijv. maximaal 5 rijen per tabel).
• Validatie: Als de SMT-oplosser een tegenvoorbeeld vindt, wordt dit gevalideerd door de query's daadwerkelijk uit te voeren op een echte database-engine (zoals SQLite) om "spurious" (vals-positieve) tegenvoorbeelden te elimineren.

Technische Uitbreidingen:
Om SPOTIT bruikbaar te maken voor moderne Text-to-SQL-benchmarks (zoals BIRD en Spider), hebben de auteurs de bestaande verifier VERIEQL aanzienlijk uitgebreid:

• Datums en Strings: Ze introduceerden nieuwe SMT-coderingen voor complexe operaties op datums (zoals STRFTIME, JulianDay, datumverschuivingen) en strings (zoals LIKE, SUBSTR, CONCAT).
• Type-conversies: Er is zorgvuldig omgegaan met impliciete type-conversies (bijv. van datum naar integer), wat cruciaal is voor de correctheid van de semantiek.
• Set-semantiek: De verifier is aangepast om equivalentie onder set-semantiek te controleren (in plaats van alleen bag-semantiek), wat vereist is voor veel benchmarks.

Workflow:

1. Input: Een natuurlijke taalvraag, de gouden SQL en de gegenereerde SQL.
2. Verificatie: De SMT-oplosser zoekt naar een database $D$ binnen de grens $K$ waarvoor $P(D) \neq Q(D)$.
3. Validatie: Het gevonden $D$ wordt uitgevoerd in een echte DBMS. Als de resultaten verschillen, is het een echte fout.
4. Cross-checking: Tegenvoorbeelden gevonden voor één model worden hergebruikt om andere modellen te testen, wat de efficiëntie verhoogt.

3. Belangrijkste Bijdragen

1. SPOTIT Pipeline: De eerste evaluatiepijplijn voor Text-to-SQL die volledig gebaseerd is op formele equivalentieverificatie.
2. Nieuwe SMT-coderingen: Een bewezen correcte uitbreiding van SQL-verificatie met ondersteuning voor datums, strings en hun manipulatie, essentieel voor real-world benchmarks.
3. Praktische Strategieën: Methoden voor efficiënte implementatie, waaronder cross-checking van tegenvoorbeelden en validatie tegen echte databases.
4. Grootschalige Evaluatie: Een uitgebreide studie van 10 state-of-the-art Text-to-SQL-methoden op het BIRD-dataset, die diepgaande inzichten levert in de huidige staat van het veld.

4. Resultaten

De auteurs hebben SPOTIT toegepast op 10 toonaangevende Text-to-SQL-methoden (zoals Alpha-SQL, OmniSQL, GenaSQL) op het BIRD-dev dataset (1.533 vraag-SQL-paren).

• Aanzienlijke Daling in Nauwkeurigheid: Wanneer men overschakelt van de officiële test-gebaseerde evaluatie naar SPOTIT, daalt de gerapporteerde nauwkeurigheid van alle methoden met 11,3% tot 14,2%.
  • Voorbeeld: De nauwkeurigheid van CSC-32B daalde van 71,32% naar 58,80%.
• Verandering in Ranking: De rangschikking van de modellen verandert aanzienlijk. Modellen die hoog scoorden op de officiële leaderboard, zakken vaak door in de ranglijst wanneer ze strikter worden getoetst.
• Oorzaken van Discrepanties: Een handmatige analyse van de gevonden tegenvoorbeelden onthulde drie hoofdoorzaken voor verschillen:
  1. Onjuiste gegenereerde SQL: Het model maakt een fout (ongeveer 26% van de gevallen).
  2. Onjuiste Gouden SQL (Ground Truth): De menselijke annotatie is fout. Dit bleek verrassend vaak het geval te zijn; in veel gevallen waar modellen "fout" werden genoemd, was de gouden SQL juist verkeerd.
  3. Ambigue Vragen: De natuurlijke taalvraag kan op meerdere manieren worden geïnterpreteerd, waardoor meerdere SQL-query's correct kunnen zijn.
• Efficiëntie: De verifier vindt tegenvoorbeelden gemiddeld binnen 4 seconden, wat aantoont dat formele verificatie praktisch toepasbaar is voor grote datasets.

5. Betekenis en Conclusie

Het paper biedt een kritische blik op de huidige stand van zaken in Text-to-SQL-evaluatie:

• Onderschatting van Ground Truth Fouten: De studie toont aan dat bestaande benchmarks (zoals BIRD) aanzienlijke fouten bevatten in hun gouden SQL. Een perfect Text-to-SQL-model kan de huidige "perfecte" score van 100% nooit halen omdat de grondwaarheid zelf imperfect is.
• Noodzaak van Formele Methoden: Test-gebaseerde evaluatie is onvoldoende om de ware prestaties van modellen te meten. SPOTIT biedt een robuustere, meer rigoureuze maatstaf die semantische verschillen blootlegt die door statische testen worden gemist.
• Toekomstperspectief: De resultaten motiveren de verificatiecommunity om meer resources te investeren in het ondersteunen van een groter deel van de SQL-standaard. Daarnaast suggereert het dat toekomstige evaluaties rekening moeten houden met ambiguïteit en mogelijk meerdere acceptabele ground truths moeten toestaan.

Kortom, SPOTIT beweert dat we de "waarde" van Text-to-SQL-modellen moeten herdefiniëren door formele verificatie te gebruiken, wat leidt tot een realistischer beeld van hun capaciteiten en de kwaliteit van de gebruikte benchmarks.