Evergreen: Efficient Claim Verification for Semantic Aggregates

Aquí se presenta un resumen técnico detallado del artículo "Evergreen: Verificación Eficiente de Afirmaciones para Agregados Semánticos".

1. Declaración del Problema

Con el auge de los motores de procesamiento de consultas semánticas (por ejemplo, Snowflake Cortex AISQL), la agregación semántica se ha convertido en un operador primitivo. Esto permite que los Modelos de Lenguaje Grandes (LLM) reduzcan una relación de tuplas en un resumen o agregado en lenguaje natural. Sin embargo, estos agregados generados por LLM a menudo contienen afirmaciones alucinatorias (por ejemplo, "la mayoría de las reseñas son positivas" cuando no lo son) que no se basan en los datos subyacentes.

Verificar estas afirmaciones es un desafío debido a cuatro factores principales:

1. Escala: Las relaciones a menudo exceden las ventanas de contexto de los LLM (miles de reseñas = cientos de miles de tokens).
2. Complejidad: Las afirmaciones involucran cuantificadores (todos, algunos, mayoría), agrupaciones y comparaciones entre grupos, lo que requiere una mezcla de razonamiento semántico (comprensión de texto) y razonamiento simbólico (conteo/comparación).
3. Costo: La verificación por fuerza bruta requiere invocar un LLM para cada tupla, lo cual es prohibitivamente costoso y lento.
4. Explicabilidad: Los usuarios requieren citas (evidencia) para confiar en el veredicto, no solo un binario "verdadero/falso".

Los enfoques existentes no abordan esto de manera holística: los métodos de LLM como juez fallan en contextos grandes; la Generación Aumentada por Recuperación (RAG) lucha con afirmaciones cuantificadas sobre tuplas independientes; y los LLM basados en programas delegan la optimización al LLM, lo que lleva a un rendimiento subóptimo.

2. Metodología: El Sistema Evergreen

Evergreen replantea la verificación de afirmaciones como una tarea de procesamiento de consultas semánticas. En lugar de pedirle a un LLM que "verifique" una afirmación, Evergreen compila la afirmación en una consulta declarativa de verificación semántica ejecutada por un motor de consultas.

A. Descomposición y Compilación de Afirmaciones

1. Descomposición: Un LLM divide el agregado en lenguaje natural en afirmaciones atómicas y resuelve referencias vagas (por ejemplo, pronombres) utilizando el contexto original.
2. Mapeo Lógico: Las afirmaciones se mapean a estructuras lógicas:
   • Existencial/Universal: $\exists t, \forall t$
   • Cardinal/Proporcional: $\exists \ge k, \exists \ge \rho$
   • Ordinal/Anidado: Clasificación de grupos o cuantificadores anidados (por ejemplo, "Todas las ubicaciones tienen >2 quejas").
3. Generación de Consultas: Las afirmaciones se compilan en una API estilo DataFrame utilizando operadores relacionales estándar (filter, map, aggregate) y operadores semánticos (llamadas a LLM basadas en prompts).
   • filter(prompt): Filtrado semántico.
   • map(prompt): Extracción de atributos semánticos.
   • aggregate: Se mapea a cuantificadores (por ejemplo, bool_or $\to$ $\exists$, count_if $\to$ cardinalidad).

B. Optimizaciones Conscientes de la Verificación

Evergreen introduce optimizaciones específicas para minimizar las llamadas a LLM manteniendo la corrección:

1. Parada Temprana: El motor de consultas utiliza un modelo de iterador.
   • Para $\exists$ (por ejemplo, "algunos"), se detiene tan pronto como se encuentra un testigo.
   • Para $\forall$ (por ejemplo, "todos"), se detiene tan pronto como se encuentra un contraejemplo.
   • Para afirmaciones cardinales o proporcionales, empuja la lógica de comparación hacia abajo para detenerse una vez que el umbral se determina matemáticamente, independientemente de las tuplas restantes.
2. Ordenamiento por Relevancia: Para hacer efectiva la parada temprana, las tuplas se ordenan previamente por relevancia. Un LLM genera una consulta de búsqueda basada en la lógica de la afirmación; las tuplas se clasifican por similitud de incrustación (embedding) y coincidencia de palabras clave para que los "testigos" aparezcan al principio del flujo.
3. Estimación con Secuencias de Confianza (CS): Para casos donde la parada temprana es imposible (por ejemplo, verificar que una afirmación universal es verdadera), Evergreen utiliza Secuencias de Confianza Válidas en Cualquier Momento. A diferencia de los intervalos de confianza clásicos, las CS permiten el monitoreo continuo sin inflar las tasas de error. El sistema detiene el muestreo una vez que el intervalo de confianza demuestra que la afirmación es verdadera o falsa con alta probabilidad.
4. Optimizaciones de Propósito General:
   • Fusión de Operadores: Combina múltiples operadores semánticos (por ejemplo, filter + map) en una sola llamada a LLM por tupla.
   • Filtrado por Similitud: Un pre-filtro ligero que utiliza incrustaciones para descartar tuplas obviamente irrelevantes antes de invocar al LLM.
   • Caché de Prompts: Reutiliza las respuestas del LLM para prompts idénticos a través de diferentes afirmaciones.

C. Citas mediante Proveniencia de Semianillo

Para proporcionar explicaciones, Evergreen trata las citas como proveniencia de datos. Utiliza proveniencia de semianillo para lógica de primer orden:

• Cada tupla se anota con tokens que indican si satisface la fórmula de la afirmación.
• El sistema deriva un conjunto mínimo de tokens (monomios) que justifican el resultado.
• Si una afirmación es verdadera, devuelve el conjunto mínimo de testigos. Si es falsa, devuelve el conjunto mínimo de contraejemplos. Esto asegura que las explicaciones sean concisas y estén matemáticamente fundamentadas.

3. Contribuciones Clave

1. Formalización Lógica: Identificó tipos comunes de afirmaciones en agregados semánticos y los mapeó a estructuras lógicas bien definidas (existencial, universal, cardinal, proporcional, ordinal, anidado).
2. Compilación Declarativa: Demostró cómo compilar afirmaciones en lenguaje natural en consultas declarativas de verificación semántica, desplazando la carga de optimización del LLM al motor de consultas.
3. Optimizaciones Novedosas: Introdujo técnicas específicas para la verificación (Parada Temprana, Ordenamiento por Relevancia, Estimación con Secuencia de Confianza) que reducen drásticamente el costo y la latencia.
4. Proveniencia Formal: Aplicó la proveniencia de semianillo para formalizar las citas como explicaciones mínimas de los resultados de verificación.
5. Evaluación Exhaustiva: Construyó un conjunto de pruebas de 16 afirmaciones diversas sobre conjuntos de datos reales de reseñas de restaurantes para evaluar el sistema.

4. Resultados Experimentales

El sistema se evaluó en tres conjuntos de datos de Yelp (1.6k–1.8k tuplas cada uno) frente a líneas base: LLM como juez (base_rm), Agente Aumentado por Recuperación (rag_agent) y un Evergreen sin optimizar (evg_unopt).

• Calidad vs. Costo:
  • LLM Fuertes: Evergreen con un LLM fuerte (Opus) logró F1 = 1.00 (verificación perfecta) mientras reducía el costo en 3.2$\times$ y la latencia en 4.0$\times$ en comparación con la versión sin optimizar.
  • LLM Débiles: Evergreen usando un LLM débil (Llama 8B) superó a una línea base fuerte de LLM como juez (Opus) en puntuación F1 (0.89 vs. 0.82) con un costo 48$\times$ menor y una latencia 2.3$\times$ menor.
  • vs. Agente RAG: Evergreen igualó o superó la calidad del agente RAG con un LLM débil a un costo 63$\times$ menor y una latencia 4.2$\times$ menor.
• Estudio de Ablación:
  • La Parada Temprana fue la optimización más crítica, reduciendo el costo/latencia en 6.7$\times$.
  • La Estimación (CS) y el Caché de Prompts proporcionaron ahorros de 2$\times$–2.7$\times$.
  • Desactivar las optimizaciones generalmente degradó el rendimiento significativamente, demostrando la necesidad del enfoque neuro-simbólico.
• Robustez: Incluso con modelos más débiles, Evergreen mantuvo una alta precisión de proveniencia (0.84–0.99), asegurando que las citas proporcionadas fueran confiables.

5. Significado

Evergreen representa un cambio significativo en cómo los sistemas de datos semánticos manejan la fiabilidad.

• Sinergia Neuro-Simbólica: Combina efectivamente la comprensión semántica de los LLM con la optimización rigurosa y el razonamiento lógico de los motores de consultas de bases de datos.
• Escalabilidad: Resuelve los cuellos de botella de la "ventana de contexto" y el "costo" que actualmente impiden el uso confiable de LLM en el análisis de datos de producción.
• Confianza: Al proporcionar citas mínimas y matemáticamente fundamentadas, va más allá de las salidas de "caja negra" de los LLM, haciendo que los agregados semánticos sean auditables y confiables para uso empresarial.
• Dirección Futura: Abre el camino para "Restricciones de Integridad Semántica", donde los sistemas de bases de datos pueden hacer cumplir automáticamente la corrección en los conocimientos generados por LLM.

En resumen, Evergreen demuestra que al tratar la verificación de afirmaciones como un problema de optimización de consultas, los sistemas pueden lograr calidad de verificación perfecta o casi perfecta a una fracción del costo y la latencia de los enfoques actuales basados en LLM más avanzados.