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

Este trabajo presenta SpotIt, un nuevo pipeline de evaluación para Text-to-SQL que utiliza verificación de equivalencia formal para identificar diferencias entre consultas generadas y de referencia que los métodos basados en pruebas tradicionales pasan por alto.

Lo esencial

Imagina que el mundo de las bases de datos es como una biblioteca gigante y desordenada. La gente quiere pedir libros (información) usando un lenguaje natural, como si estuviera hablando con un bibliotecario: "¿Me puedes decir quién es el paciente más joven con una enfermedad rara?".

El problema es que los bibliotecarios (los sistemas de Inteligencia Artificial) no siempre hablan el mismo idioma que la biblioteca. Tienen que traducir esa pregunta humana a un código muy estricto llamado SQL (el idioma de las bases de datos).

Hasta ahora, para saber si el bibliotecario (la IA) lo hizo bien, usábamos un método muy simple: la prueba del "mismo resultado".

El problema del método antiguo (La prueba de la foto)

Imagina que le das a dos bibliotecarios diferentes la misma pregunta: "¿Quién es el paciente más joven?".

• Bibliotecario A busca en el registro y encuentra al "Paciente Juan".
• Bibliotecario B busca en el registro y también encuentra al "Paciente Juan".

Como ambos dieron el mismo nombre, el sistema dice: "¡Perfecto! Ambos acertaron".

Pero aquí está el truco: ¿Y si el registro que usaron para la prueba solo tenía a Juan? ¿Y si en la vida real, el Bibliotecario B usó una lógica equivocada que, por pura suerte, funcionó solo porque el registro de prueba era pequeño y específico?

El método antiguo es como evaluar a un conductor de carreras solo porque logró estacionar el coche en un espacio vacío. No sabemos si sabe conducir en una tormenta o en un tráfico denso. Solo sabemos que en esa foto específica, el coche estaba bien.

La solución: SPOTIT (El detective de escenarios)

Los autores de este paper crearon SPOTIT. En lugar de confiar en una sola foto (la base de datos de prueba), SPOTIT actúa como un detective obsesivo o un abogado del diablo.

Su trabajo es:

1. Tomar la pregunta del Bibliotecario A (la IA) y la del Bibliotecario B (la respuesta "correcta" hecha por humanos).
2. Preguntar: "¿Existe algún escenario, algún registro de pacientes, en el que estos dos bibliotecarios den respuestas diferentes?"
3. Si el detective encuentra incluso un solo caso donde las respuestas divergen, ¡Bingo! SPOTIT descubre que la IA estaba equivocada, aunque en la prueba original pareciera correcta.

¿Qué descubrieron? (Las sorpresas)

Cuando aplicaron este nuevo método "detectivesco" a 10 de los mejores sistemas de IA actuales, les pasó algo muy interesante:

1. La IA estaba peor de lo que pensábamos: Muchos sistemas que parecían tener un 70% de éxito, en realidad solo tenían un 55%. El método antiguo les estaba dando "puntos extra" injustos por pura suerte.
2. El "correcto" a veces estaba equivocado: Lo más sorprendente fue que, en muchos casos, la IA tenía razón y la respuesta "oficial" (la hecha por humanos) estaba mal.
   • Analogía: Imagina que el bibliotecario jefe (humano) escribió mal la regla en el libro de instrucciones. La IA, al intentar seguir la lógica, hizo algo diferente. El método antiguo dijo: "La IA falló porque no siguió la regla mal escrita". SPOTIT dijo: "Espera, la regla del jefe es confusa o incorrecta".
3. Las preguntas eran ambiguas: A veces, la pregunta humana era tan vaga que podía tener dos respuestas válidas. El método antiguo castigaba a la IA por elegir una de las dos, mientras que SPOTIT mostraba que ambas eran lógicas.

En resumen

Este paper nos dice que confiar solo en ejemplos fijos para evaluar la Inteligencia Artificial es peligroso. Es como si evaluáramos a un chef solo porque sabe hacer un pastel perfecto cuando usa harina de una marca específica, pero no sabemos si sabe cocinar con otros ingredientes.

SPOTIT es como un simulador de cocina que prueba al chef con miles de combinaciones de ingredientes diferentes para asegurarse de que realmente sabe cocinar, no solo que tiene suerte con un ingrediente específico. Además, nos ayudó a darnos cuenta de que a veces, los libros de recetas (las bases de datos de prueba) tienen errores que nadie había notado.

Es un paso gigante para hacer que la tecnología que habla nuestro idioma sea realmente fiable y precisa.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo "SPOTIT: EVALUATING TEXT-TO-SQL EVALUATION WITH FORMAL VERIFICATION", presentado en ICLR 2026.

1. El Problema: Limitaciones de la Evaluación Basada en Pruebas

El campo de Text-to-SQL (traducción de lenguaje natural a consultas SQL) depende críticamente de plataformas de evaluación comunitaria (como BIRD y Spider) para medir el estado del arte. Sin embargo, el método de evaluación actual tiene una falla fundamental:

• Enfoque Actual (Basado en Pruebas): La corrección de una consulta SQL generada se determina ejecutándola junto con una consulta "gold" (referencia humana) en una base de datos de prueba estática. Si los resultados de ejecución coinciden, la consulta se marca como correcta.
• La Falacia de la Equivalencia: Este enfoque es optimista. Dos consultas SQL semánticamente diferentes pueden producir accidentalmente el mismo resultado en una base de datos específica debido a los datos contenidos en ella. Esto lleva a falsos positivos, donde se asume que un modelo es correcto cuando en realidad no lo es.
• La Pregunta Clave: ¿Con qué frecuencia la evaluación basada en pruebas pasa por alto diferencias reales entre la consulta generada y la consulta de referencia?

2. Metodología: SPOTIT y Verificación Formal

Los autores proponen SPOTIT, un nuevo pipeline de evaluación que reemplaza la verificación estática por una búsqueda activa de bases de datos diferenciadoras utilizando verificación formal.

A. Verificación de Equivalencia Acotada (Bounded Equivalence Checking)

En lugar de probar en una sola base de datos, SPOTIT intenta encontrar una base de datos $D_{cex}$ (contraejemplo) tal que la consulta generada $P$ y la consulta gold $Q$ produzcan resultados diferentes ($P(D_{cex}) \neq Q(D_{cex})$).

• Dado que la equivalencia total de SQL es indecidible, el sistema utiliza verificación acotada basada en SMT (Satisfiability Modulo Theories).
• Se busca un contraejemplo donde el tamaño de las relaciones (tablas) no exceda un límite $K$. Si se encuentra un contraejemplo, las consultas no son equivalentes. Si no se encuentra hasta el límite $K$, se consideran equivalentes bajo ese acotamiento.

B. Extensiones Técnicas Críticas

El motor de verificación subyacente (una extensión de VERIEQL) se amplió significativamente para soportar el subconjunto de SQL utilizado en benchmarks modernos:

1. Codificación Precisa de Tipos de Datos: Se implementó una codificación simbólica rigurosa para fechas (representadas como tripletes año/mes/día con validación de años bisiestos y rangos) y cadenas, superando las limitaciones de las representaciones anteriores (como enteros simples).
2. Operadores de Cadena y Fecha: Soporte para funciones como STRFTIME, JulianDay, SUBSTR, CONCAT, LIKE, y conversiones de tipo implícitas (ej. fecha a entero).
3. Semántica de Conjuntos: Adaptación de la verificación para manejar la equivalencia bajo semántica de conjuntos (donde el orden y las duplicaciones no importan), en lugar de solo semántica de listas o multiconjuntos, alineándose con los estándares de BIRD.
4. Validación de Contraejemplos: Un paso de validación ejecuta las consultas en un motor SQL real (SQLite) sobre la base de datos generada para descartar contraejemplos espurios causados por sobre-estimaciones en la codificación SMT.

C. El Pipeline SPOTIT

1. Generación: Un framework Text-to-SQL genera una consulta $P$ a partir de una pregunta $N$.
2. Verificación: Se ejecuta el verificador SMT para buscar un contraejemplo $D_{cex}$ dentro del límite $K$.
3. Validación: Se ejecuta $P$ y $Q$ en $D_{cex}$ en SQLite. Si los resultados difieren, es un contraejemplo válido.
4. Cruce de Referencias (Cross-checking): Una optimización donde los contraejemplos encontrados para un modelo se reutilizan para probar la equivalencia en otros modelos, mejorando la eficiencia.

3. Contribuciones Clave

1. SPOTIT: El primer pipeline de evaluación para Text-to-SQL impulsado por verificación de equivalencia formal.
2. Nuevas Codificaciones SMT: Desarrollo y demostración de corrección de codificaciones para operadores complejos de fechas y cadenas, esenciales para benchmarks reales.
3. Estrategias de Despliegue: Métodos prácticos para escalar la verificación formal a grandes conjuntos de datos.
4. Evaluación a Gran Escala: Un análisis exhaustivo de 10 métodos de estado del arte en el dataset BIRD, revelando deficiencias sistémicas en la evaluación actual.

4. Resultados Experimentales

La evaluación se realizó sobre el conjunto de desarrollo de BIRD (1,533 pares pregunta-SQL) con 10 modelos avanzados (incluyendo Alpha-SQL, OmniSQL, CSC-SQL, etc.).

• Caída en la Precisión Reportada: Al cambiar de la métrica oficial basada en pruebas (EX-TEST) a SPOTIT, la precisión de los métodos cayó entre un 11.3% y un 14.2%.
  • Ejemplo: El modelo CSC-32B pasó del 71.32% de precisión (Rank 1) al 58.80% (Rank 3) con SPOTIT.
• Reordenamiento de Modelos: El ranking de los modelos cambió significativamente. Los modelos que parecían superiores bajo pruebas estáticas no siempre mantuvieron su posición bajo verificación formal, lo que sugiere que la evaluación actual distorsiona la comparación relativa de los métodos.
• Eficiencia: El verificador encuentra contraejemplos en promedio en menos de 4 segundos por pregunta, demostrando que la verificación formal es viable para evaluaciones a gran escala.
• Análisis de las Discrepancias: El análisis manual de los contraejemplos reveló tres causas principales de fallo:
  1. Consultas Gold Incorrectas: En muchos casos, la consulta de referencia humana era errónea (ej. lógica de WHERE mal interpretada, errores de sintaxis en condiciones de fechas).
  2. Ambigüedad en la Pregunta: La pregunta de lenguaje natural admitía múltiples interpretaciones válidas, haciendo que tanto la consulta generada como la gold fueran correctas bajo diferentes interpretaciones.
  3. Errores del Modelo: El modelo generó una consulta incorrecta.
  • Hallazgo Sorprendente: A menudo, cuando el modelo discrepaba de la gold, la gold era la incorrecta.

5. Significado e Implicaciones

El trabajo de SPOTIT tiene implicaciones profundas para la comunidad de Text-to-SQL y la verificación formal:

1. Cuestionamiento de los Benchmarks Actuales: Demuestra que las métricas basadas en pruebas estáticas sobreestiman significativamente el rendimiento real de los modelos y pueden estar penalizando injustamente a modelos que generan soluciones semánticamente correctas pero diferentes a una gold errónea o ambigua.
2. Calidad de los Datos de Referencia: Revela que los conjuntos de datos de referencia (gold SQLs) en benchmarks populares como BIRD contienen un número significativo de errores y ambigüedades. SPOTIT proporciona una herramienta para depurar y mejorar estos conjuntos de datos.
3. Viabilidad de la Verificación Formal: Prueba que las técnicas de verificación formal (SMT) pueden manejar un subconjunto rico y práctico de SQL (con fechas, cadenas y tipos complejos) de manera eficiente, abriendo la puerta a su uso como métrica de evaluación estándar o complemento.
4. Futuro de la Evaluación: Sugiere que la evaluación ideal debe considerar la ambigüedad del lenguaje natural y permitir múltiples respuestas correctas, en lugar de depender ciegamente de una única consulta gold.

En resumen, SPOTIT no solo ofrece una métrica de evaluación más rigurosa, sino que actúa como una herramienta de diagnóstico que expone las debilidades inherentes en los propios procesos de evaluación y en los datos de entrenamiento de la comunidad Text-to-SQL.