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

O artigo apresenta o SpotIt, um novo pipeline de avaliação para Text-to-SQL que utiliza verificação formal de equivalência para identificar diferenças entre consultas geradas e de referência que os métodos tradicionais baseados em testes poderiam ignorar.

O essencial

Imagine que você está pedindo a um assistente de IA que ele escreva uma receita de bolo baseada apenas na sua descrição: "Quero um bolo de chocolate com frutas vermelhas".

O assistente entrega uma receita. Você olha para a receita dele e compara com a "receita oficial" (a que um chef humano escreveu). Se você seguir as duas receitas e, por sorte, o bolo sair exatamente igual no seu teste (digamos, usando apenas 2 ovos e 1 xícara de açúcar), você diz: "Ótimo! O assistente acertou".

O problema é que essa "sorte" pode esconder erros graves.

A receita do assistente pode ter dito "adicionar sal" em vez de "adicionar açúcar", mas como você só testou com uma quantidade específica de ingredientes, o bolo ficou doce de qualquer jeito. Se você tentasse fazer o bolo com outra quantidade de ingredientes, o resultado seria um desastre.

O artigo SPOTIT (que será apresentado na conferência ICLR 2026) diz que a forma como avaliamos essas IAs hoje está muito "otimista" e falha em pegar esses erros.

Aqui está a explicação do que eles fizeram, usando analogias do dia a dia:

1. O Problema: O "Teste de Prova" (A Avaliação Atual)

Hoje, para ver se uma IA sabe transformar perguntas em comandos de banco de dados (o que chamamos de Text-to-SQL), os pesquisadores usam um "teste de prova" estático.

• A Analogia: É como se o professor de matemática desse um único problema para a turma resolver: "Quanto é 2 + 2?". Se o aluno responder "4", ele passa.
• O Erro: E se o aluno tivesse escrito a fórmula errada, mas que, por coincidência, deu "4" naquele caso específico? O professor não percebeu. Na área de bancos de dados, isso significa que a IA pode estar gerando comandos errados que, por sorte, funcionam apenas nos dados de teste que os humanos criaram.

2. A Solução: O "Detetive de Contradições" (O SPOTIT)

Os autores criaram o SPOTIT. Em vez de apenas testar a receita em uma cozinha específica, o SPOTIT é como um detetive super-rápido que tenta criar milhões de cozinhas diferentes para ver se ele consegue encontrar uma única situação onde a receita do assistente e a do chef dão resultados diferentes.

• Como funciona: O SPOTIT usa uma tecnologia chamada "Verificação Formal" (que é como um matemático muito rigoroso). Ele não chuta; ele prova logicamente se existe alguma combinação de dados (uma "cozinha") onde as duas receitas falham em ser iguais.
• O Resultado: Se o SPOTIT encontra uma "cozinha" onde o bolo do assistente fica salgado e o do chef fica doce, ele diz: "Ei! Eles não são iguais! A IA errou (ou a receita oficial errou)".

3. As Descobertas Surpreendentes

Quando eles aplicaram esse "detetive" em 10 das melhores IAs do mundo, usando um banco de dados famoso chamado BIRD, descobriram coisas chocantes:

• A IA não é tão boa quanto parecia: A precisão das IAs caiu drasticamente (entre 11% e 14%). Muitas vezes, a IA passava no teste antigo só porque os dados de teste eram "sortudos", não porque ela sabia a resposta certa.
• O "Chef" (o Humano) também errou: A descoberta mais curiosa foi que, muitas vezes, quando a IA dava uma resposta diferente da "oficial", a resposta oficial estava errada!
  • Analogia: Imagine que o professor escreveu a resposta errada no gabarito. O aluno, ao tentar pensar de forma lógica, deu a resposta certa, mas foi marcado como errado porque não bateu com o gabarito. O SPOTIT mostrou que os "gabaritos" (as respostas humanas) estão cheios de erros e ambiguidades.
• Perguntas Confusas: Muitas perguntas dos testes são ambíguas. É como perguntar "Quantos membros tem o clube?". Isso significa "todos os alunos inscritos" ou "apenas os que têm o cargo de 'membro' registrado"? A IA e o humano podem ter entendido coisas diferentes, e ambos estariam "certos" dependendo da interpretação.

4. Por que isso importa?

O SPOTIT nos ensina duas lições importantes:

1. Não confie cegamente nos testes atuais: Se uma IA passa no teste de hoje, pode ser apenas porque os dados de teste eram fáceis ou "sortudos". Precisamos de testes mais rigorosos que tentem "quebrar" a lógica da IA.
2. Os dados de treino precisam de uma faxina: Os próprios bancos de dados e perguntas que usamos para treinar e testar as IAs estão cheios de erros humanos. Precisamos limpar esses "gabaritos" antes de culparmos as máquinas.

Resumo final:
O SPOTIT é como um inspetor de qualidade que não se contenta em ver se o produto funciona na primeira tentativa. Ele tenta criar cenários extremos para ver se o produto quebra. E, ao fazer isso, ele descobriu que tanto os fabricantes (as IAs) quanto os designers (os humanos que criam os testes) precisam melhorar suas ferramentas.

Resumo técnico

1. O Problema

A avaliação atual de sistemas Text-to-SQL (conversão de linguagem natural para SQL) baseia-se quase exclusivamente em métodos de teste estático. Nesse processo, as consultas SQL geradas por um modelo são executadas em um banco de dados de teste fixo (fornecido pelo benchmark, como BIRD ou Spider) e os resultados são comparados com os resultados de uma consulta "Gold" (padrão-ouro, escrita por humanos).

O artigo identifica uma falha fundamental nessa abordagem:

• Otimismo Excessivo: Duas consultas SQL semanticamente diferentes podem produzir o mesmo conjunto de resultados em um banco de dados específico devido à distribuição particular dos dados. Isso leva a falsos positivos, onde consultas incorretas são classificadas como corretas.
• Limitação da Equivalência: A verificação baseada em teste não garante que as consultas sejam equivalentes em todos os bancos de dados possíveis, apenas naquele específico.
• Problemas nos Dados de Referência: O processo de teste não consegue distinguir se um erro vem da geração do modelo ou de erros na própria consulta "Gold" (que é criada manualmente e propensa a falhas humanas).

2. Metodologia: SPOTIT

Os autores propõem o SPOTIT (Search-based Proof of Text-to-SQL Integrity via Verification), um pipeline de avaliação alternativo que utiliza verificação formal de equivalência limitada em vez de execução de testes.

Abordagem Central

Em vez de executar consultas em um banco de dados fixo, o SPOTIT utiliza um motor de verificação baseado em SMT (Satisfiability Modulo Theories) para ativamente procurar um banco de dados diferenciador (counterexample).

• Objetivo: Encontrar um banco de dados $D_{cex}$ tal que a execução da consulta gerada ($P$) e da consulta Gold ($Q$) produza resultados diferentes.
• Verificação Limitada: Como a equivalência completa de SQL é indecidível, o sistema verifica a equivalência dentro de um limite de tamanho de relação ($K$). Se o verificador não encontrar um contraexemplo até o limite $K$, as consultas são consideradas equivalentes para aquele tamanho.

Inovações Técnicas

Para tornar a verificação viável para benchmarks modernos de Text-to-SQL, os autores estenderam significativamente o verificador existente VERIEQL:

1. Codificação SMT para Strings e Datas: Desenvolveram novas codificações para operadores de SQL que manipulam strings e datas (comuns em benchmarks como BIRD), incluindo:
   • Formatação de datas (STRFTIME), cálculo de dias julianos e deslocamento de datas.
   • Manipulação de strings: prefixo, sufixo, LIKE, CONTAIN e truncamento (SUBSTR).
   • Conversão implícita de tipos (ex: data para inteiro, string para inteiro), crucial para a semântica correta do SQL.
2. Semântica de Conjuntos vs. Multiconjuntos: Adaptaram a verificação para suportar a semântica de conjuntos (onde duplicatas são ignoradas), que é o padrão em plataformas como BIRD, diferentemente da semântica de multiconjuntos (bags) usada em muitos verificadores anteriores.
3. Validação de Contraexemplos: O pipeline inclui uma fase de validação onde o banco de dados candidato gerado pelo SMT é executado em um SGBD real (SQLite) para garantir que o contraexemplo não seja espúrio (falso positivo do verificador).

Fluxo de Trabalho (Algoritmo)

1. Geração: Um framework Text-to-SQL gera a consulta $P$ a partir da pergunta $N$.
2. Verificação: O motor SMT verifica a equivalência entre $P$ e a Gold $Q$ para tamanhos de banco de dados crescentes ($k=1$ até $K$).
3. Validação: Se um contraexemplo for encontrado, ele é validado no SQLite.
4. Cross-Checking: O sistema reutiliza contraexemplos encontrados para um modelo para testar outros modelos, aumentando a eficiência.

3. Contribuições Principais

1. SPOTIT: O primeiro pipeline de avaliação de Text-to-SQL baseado em verificação formal de equivalência.
2. Extensão de Verificadores: Novas codificações SMT para operadores de strings e datas, provando a correção dessas extensões teoricamente.
3. Estratégias Práticas: Métodos para implantação eficiente, incluindo a reutilização de contraexemplos entre diferentes modelos.
4. Análise em Grande Escala: Uma avaliação abrangente de 10 métodos de ponta no dataset BIRD, revelando falhas sistêmicas nos métodos de avaliação atuais.

4. Resultados Experimentais

Os experimentos foram realizados no conjunto de desenvolvimento do dataset BIRD (1.533 pares de pergunta-SQL) com 10 frameworks de ponta.

• Queda na Precisão Reportada: Ao substituir a métrica de teste oficial (EX-TEST) pelo SPOTIT, a precisão dos métodos caiu significativamente:
  • A redução variou entre 11,3% e 14,2% na precisão absoluta.
  • Exemplo: O método CSC-32B, que era o 1º colocado com 71,32% de precisão no teste oficial, caiu para a 4ª posição com 57,82% sob o SPOTIT+.
• Reordenamento dos Rankings: A ordem de classificação dos modelos mudou substancialmente, indicando que o teste estático favorece indevidamente certos modelos que coincidem com os dados de teste, mas falham em generalização semântica.
• Descoberta de Erros na "Gold SQL": Uma descoberta surpreendente foi que, em muitos casos onde a consulta gerada diferia da Gold, a própria consulta Gold estava incorreta.
  • Em uma amostra manual, quando todos os 10 modelos discordaram da Gold SQL, 31 de 36 casos tinham Gold SQLs problemáticas.
  • Isso sugere que o limite superior de desempenho em benchmarks atuais é artificialmente limitado por erros humanos nas anotações.
• Ambiguidade: O SPOTIT identificou casos onde a pergunta em linguagem natural era ambígua, admitindo múltiplas interpretações SQL válidas, o que penaliza injustamente os modelos em avaliações binárias.
• Eficiência: O tempo médio para encontrar um contraexemplo foi inferior a 4 segundos por consulta, demonstrando que a verificação formal é viável para avaliação em larga escala.

5. Significado e Implicações

O trabalho do SPOTIT tem implicações profundas para o campo de Text-to-SQL e para a comunidade de verificação formal:

1. Crise de Confiança nos Benchmarks: Os resultados indicam que as métricas atuais (baseadas em teste estático) superestimam drasticamente a capacidade real dos modelos e mascaram erros nas próprias bases de dados de avaliação.
2. Necessidade de Revisão de Dados: A comunidade deve investir na correção sistemática das consultas "Gold" em benchmarks como BIRD e Spider, utilizando ferramentas como o SPOTIT para detectar inconsistências.
3. Novo Paradigma de Avaliação: O SPOTIT propõe uma mudança de paradigma: em vez de perguntar "a resposta está correta neste banco de dados?", devemos perguntar "a consulta é semanticamente equivalente para qualquer banco de dados possível?".
4. Ponte entre IA e Verificação Formal: O trabalho demonstra que técnicas de verificação formal (SMT) podem ser aplicadas com sucesso e eficiência a problemas práticos de IA, cobrindo uma fração significativa de consultas SQL do mundo real, incentivando a comunidade de verificação a expandir o suporte para mais recursos de SQL.

Em resumo, o SPOTIT expõe que a avaliação atual de Text-to-SQL é frágil e otimista, oferecendo uma ferramenta rigorosa para medir a verdadeira equivalência semântica e revelar falhas tanto nos modelos quanto nos dados de referência.