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

Ce papier présente SpotIt, une nouvelle méthode d'évaluation Text-to-SQL qui remplace les tests basés sur des données statiques par une vérification formelle d'équivalence capable de détecter des différences entre les requêtes générées et les références, révélant ainsi les limites des approches actuelles sur le jeu de données BIRD.

L'essentiel

🕵️‍♂️ SPOTIT : Le Détective qui Vérifie les Traductions de Langage Naturel

Imaginez que vous êtes un chef cuisinier (l'ordinateur) et que vous devez traduire les commandes de vos clients (le langage naturel) en recettes précises (des requêtes SQL) pour préparer un plat.

Le problème, c'est que pour savoir si votre recette est bonne, on vous donne habituellement un seul et unique test : on vous donne un panier de légumes spécifique (une base de données de test) et on vous demande de cuisiner. Si le plat final ressemble à celui du chef étoilé (la "réponse officielle"), on dit que vous avez réussi.

Mais voici le piège :
Il est possible que votre recette soit fausse, mais que, par un pur coup de chance, elle donne le même résultat sur ce panier de légumes précis. C'est comme si vous aviez mis du sel à la place du sucre, mais que le client n'avait goûté qu'un seul fruit qui avait le même goût dans les deux cas. Vous avez "triché" sans le savoir, et le test ne l'a pas vu.

C'est exactement ce que l'équipe derrière SPOTIT a découvert. Ils ont créé un nouveau système pour vérifier les traductions de questions en requêtes de base de données (Text-to-SQL).

🚫 Le Problème de l'Ancienne Méthode (Le Test Statique)

Actuellement, les plateformes d'évaluation fonctionnent comme un examen sur un seul sujet :

1. On pose une question.
2. L'IA donne une réponse (une requête SQL).
3. On l'exécute sur une petite base de données fixe.
4. Si le résultat correspond à celui du "maître", c'est Gagné.

Le problème ? C'est une optimisme trompeur. Deux recettes différentes peuvent donner le même plat sur un seul ingrédient, mais échouer complètement sur un autre.

🕵️‍♀️ La Solution SPOTIT : Le Détective Formel

Au lieu de se contenter d'un seul panier de légumes, SPOTIT agit comme un détective très rigoureux (un vérificateur formel).

Au lieu de dire : "Est-ce que ça marche sur ce panier ?", il demande : "Est-ce qu'il existe n'importe quel panier de légumes, aussi petit soit-il, où votre recette donnerait un résultat différent de celle du maître ?"

• L'analogie du "Contre-exemple" : Imaginez que le détective essaie de construire un scénario minuscule (une base de données de 2 ou 3 lignes) où votre recette échoue. S'il trouve un tel scénario, il vous dit : "Attention ! Votre recette est fausse, même si elle a réussi le test précédent."
• La garantie : Si le détective ne trouve aucun scénario où vous échouez (après avoir cherché très soigneusement), alors on peut être sûr à 100 % que votre recette est correcte, peu importe les ingrédients futurs.

📉 Ce qu'ils ont découvert (Les Révélations)

En utilisant ce nouveau détective sur 10 des meilleurs systèmes d'IA actuels, ils ont fait des découvertes surprenantes :

1. Les notes chutent : Quand on remplace l'ancien test par SPOTIT, la performance des IA baisse de 11 % à 14 %. Cela signifie que beaucoup d'IA étaient "notées trop haut" parce que l'ancien test était trop facile et manquait les erreurs.
2. Le classement change : Les IA qui étaient en tête du classement ne sont plus forcément les meilleures. Certaines qui semblaient géniales se révèlent fragiles.
3. Le vrai coupable ? Parfois, c'est le maître ! C'est la découverte la plus surprenante. Souvent, quand l'IA donne une réponse différente de la "réponse officielle", c'est la réponse officielle qui est fausse !
   • Exemple : Le "maître" a écrit une recette avec une erreur de logique (comme oublier un ingrédient essentiel). L'IA, elle, a compris la question correctement et a donné la bonne réponse. Mais comme l'ancien test comparait juste les résultats sur un panier fixe, il a pénalisé l'IA pour avoir été "trop intelligente".
4. Les questions ambiguës : Parfois, la question du client est floue (comme "Qui sont les membres ?" : est-ce tous les élèves du club, ou seulement ceux inscrits comme "membres" ?). L'IA et le maître peuvent avoir deux interprétations différentes, toutes deux valables.

🛠️ Comment ça marche techniquement (sans les maths)

Les chercheurs ont utilisé un outil appelé SMT (Satisfiability Modulo Theories), qui est un peu comme un super-calculateur de logique.

• Ils ont appris à cet outil à comprendre des choses complexes comme les dates (le 29 février existe-t-il ?) et les chaînes de caractères (les noms, les adresses).
• Au lieu de tester au hasard, le détective explore mathématiquement tous les paniers de légumes possibles de petite taille pour trouver celui qui révèle l'erreur.

🎯 Conclusion : Pourquoi c'est important ?

Cet article nous dit que pour progresser en Intelligence Artificielle, nous ne devons plus nous fier aveuglément aux tests sur des données fixes.

• Pour les développeurs : Il faut arrêter de se fier uniquement aux classements actuels, car ils sont biaisés.
• Pour les benchmarks (les compétitions) : Il faut nettoyer les "réponses officielles" qui contiennent des erreurs.
• Pour l'avenir : SPOTIT offre une loupe plus puissante pour voir les vraies capacités des IA, en trouvant les failles cachées que les tests classiques laissent passer.

En résumé, SPOTIT est passé de "Est-ce que ça marche ici ?" à "Est-ce que ça marche partout ?", et cela a permis de révéler que nos meilleurs "élèves" (les IA) étaient souvent mal notés, ou que leurs "professeurs" (les réponses officielles) faisaient des erreurs !

Résumé technique

Voici un résumé technique détaillé de l'article de conférence SPOTIT : EVALUATING TEXT-TO-SQL EVALUATION WITH FORMAL VERIFICATION, publié à ICLR 2026.

1. Problématique

L'évaluation actuelle des systèmes Text-to-SQL repose principalement sur des méthodes basées sur l'exécution de tests (test-based evaluation). Dans cette approche, les requêtes SQL générées par un modèle sont exécutées sur une base de données de test statique et leurs résultats sont comparés à ceux d'une requête "Gold" (annotée par un humain).

Les auteurs identifient une limitation majeure de cette méthode : elle est optimiste. Deux requêtes SQL différentes peuvent produire le même résultat sur une base de données spécifique par coïncidence, sans être sémantiquement équivalentes. Cela conduit à une surévaluation de la précision des modèles. De plus, cette méthode ne permet pas de distinguer si une erreur provient du modèle généré, d'une erreur dans la requête Gold (annotée manuellement), ou d'une ambiguïté dans la question naturelle.

2. Méthodologie : SPOTIT

Pour pallier ces défauts, les auteurs proposent SPOTIT, un nouveau pipeline d'évaluation basé sur la vérification formelle d'équivalence bornée. Au lieu de tester sur une seule base de données, SPOTIT cherche activement à trouver une base de données (un contre-exemple) qui différencie la requête générée ($P$) de la requête Gold ($Q$).

Le processus se déroule en trois phases :

1. Génération : Un framework Text-to-SQL génère une requête $P$ à partir d'une question naturelle et d'un schéma de base de données.
2. Vérification Bornée : Le système encode le problème d'équivalence entre $P$ et $Q$ sous forme de formule SMT (Satisfiability Modulo Theories). Il utilise un solveur SMT (basé sur l'outil VERIEQL) pour déterminer s'il existe une base de données de taille bornée $K$ où les résultats de $P$ et $Q$ diffèrent.
   • Si la formule est insatisfaisable, les requêtes sont prouvées équivalentes pour cette taille.
   • Si la formule est satisfaisable, le solveur fournit une interprétation qui correspond à une base de données de contre-exemple ($D_{cex}$).
3. Validation : Les contre-exemples trouvés sont exécutés sur un moteur de base de données réel (ex: SQLite) pour éliminer les faux positifs (contre-exemples spurius dus à des approximations dans l'encodage SMT).

Innovations Techniques Clés :

• Extension de VERIEQL : Les auteurs ont étendu le vérificateur existant pour supporter un sous-ensemble SQL plus riche, crucial pour les benchmarks Text-to-SQL. Cela inclut :
  • Un encodage précis des types dates (représentés comme des triplets année/mois/jour avec contraintes de validité, années bissextiles, etc.) et des chaînes de caractères.
  • La gestion des conversions de types implicites (ex: date vers entier, chaîne vers entier).
  • Des opérateurs de manipulation de chaînes (préfixe, suffixe, LIKE, SUBSTR) et de dates (STRFTIME, JulianDay).
• Sémantique d'Ensemble : L'encodage prend en compte la sémantique d'ensemble (Set Semantics) utilisée par les benchmarks comme BIRD, contrairement à la sémantique de sac (Bag Semantics) souvent utilisée en vérification pure.
• Cross-Checking : Une stratégie où les contre-exemples trouvés pour un modèle sont réutilisés pour tester les autres modèles, améliorant l'efficacité globale.

3. Contributions Principales

• SPOTIT : Le premier pipeline d'évaluation Text-to-SQL entièrement basé sur la vérification formelle.
• Nouvel Encodage SMT : Une preuve de correction pour l'encodage d'opérateurs SQL complexes sur les dates et les chaînes, permettant une vérification précise.
• Stratégies de Déploiement : Des méthodes pratiques pour rendre la vérification formelle applicable à grande échelle (gestion des timeouts, validation des contre-exemples).
• Évaluation à Grande Échelle : Une analyse de 10 méthodes state-of-the-art sur le benchmark BIRD (1 533 paires Question-SQL).

4. Résultats Expérimentaux

L'évaluation sur le dataset BIRD révèle des écarts significatifs par rapport aux métriques officielles :

• Baisse de Précision : Lorsque l'on passe de l'évaluation par test ($EX-TEST$) à SPOTIT, la précision des modèles chute de 11,3 % à 14,2 %. Par exemple, la précision du modèle CSC-32B passe de 71,32 % à 58,80 %.
• Changement de Classement : L'ordre des modèles change considérablement. Le modèle classé 1er par la méthode officielle tombe à la 4ème place avec SPOTIT+, montrant que les métriques actuelles masquent des différences de performance réelles.
• Détection d'Erreurs dans les "Gold SQL" : L'analyse des contre-exemples montre une découverte surprenante : dans de nombreux cas où le modèle généré diffère de la Gold SQL, c'est la Gold SQL elle-même qui est incorrecte (erreurs d'annotation, logique erronée). Dans certains cas, la Gold SQL contient des bugs de logique (ex: mauvaise interprétation de conditions booléennes sur les chaînes).
• Ambiguïté : Une partie des divergences provient de questions naturelles ambiguës admettant plusieurs interprétations SQL valides.
• Performance : Le temps moyen pour trouver un contre-exemple est inférieur à 4 secondes, rendant la méthode praticable. Le taux de validation des contre-exemples est élevé (jusqu'à 96 %), confirmant la précision de l'encodage SMT.

5. Signification et Implications

Ce travail remet en question la fiabilité des plateformes d'évaluation Text-to-SQL actuelles (comme BIRD et Spider).

• Fiabilité des Benchmarks : Il démontre que les benchmarks actuels contiennent un nombre significatif de "Gold SQL" erronés ou de questions ambiguës, ce qui fausse l'évaluation de l'état de l'art. Un modèle parfait ne pourrait pas atteindre 100 % de précision sur ces benchmarks en raison de ces erreurs de référence.
• Nouveau Standard d'Évaluation : SPOTIT propose une alternative rigoureuse qui ne se contente pas de vérifier le résultat sur un échantillon de données, mais garantit l'équivalence sémantique (dans les bornes définies).
• Pour la Communauté de Vérification : L'article prouve que les techniques de vérification formelle (SMT) peuvent être appliquées efficacement à des fragments SQL complexes et pratiques, ouvrant la voie à une intégration plus large de ces outils dans le cycle de développement des systèmes de bases de données et d'IA.

En conclusion, SPOTIT offre un outil puissant pour identifier non seulement les faiblesses des modèles de génération SQL, mais aussi les défauts structurels des benchmarks eux-mêmes, incitant à une révision des pratiques d'évaluation dans le domaine.