Evergreen: Efficient Claim Verification for Semantic Aggregates

1. Declaração do Problema

Com o surgimento de motores de processamento de consultas semânticas (por exemplo, Snowflake Cortex AISQL), a agregação semântica tornou-se um operador primitivo. Isso permite que Modelos de Linguagem Grandes (LLMs) reduzam uma relação de tuplas em um resumo ou agregado em linguagem natural. No entanto, esses agregados gerados por LLMs frequentemente contêm afirmações alucinadas (por exemplo, "a maioria das avaliações é positiva" quando não é) que não estão fundamentadas nos dados subjacentes.

Verificar essas afirmações é desafiador devido a quatro fatores principais:

1. Escala: Relações frequentemente excedem as janelas de contexto de LLMs (milhares de avaliações = centenas de milhares de tokens).
2. Complexidade: Afirmações envolvem quantificadores (todos, alguns, maioria), agrupamentos e comparações entre grupos, exigindo uma mistura de raciocínio semântico (compreensão de texto) e raciocínio simbólico (contagem/comparação).
3. Custo: A verificação por força bruta requer invocar um LLM para cada tupla, o que é proibitivamente caro e lento.
4. Explicabilidade: Os usuários exigem citações (evidências) para confiar no veredito, não apenas um binário "verdadeiro/falso".

Abordagens existentes falham em abordar isso de forma holística: métodos de LLM como juiz falham em contextos grandes; Geração Aumentada por Recuperação (RAG) luta com afirmações quantificadas sobre tuplas independentes; e LLMs baseados em programas transferem a otimização para o LLM, levando a desempenho subótimo.

2. Metodologia: O Sistema Evergreen

O Evergreen reformula a verificação de afirmações como uma tarefa de processamento de consultas semânticas. Em vez de pedir a um LLM para "verificar" uma afirmação, o Evergreen compila a afirmação em uma consulta declarativa de verificação semântica executada por um motor de consultas.

A. Decomposição e Compilação de Afirmações

1. Decomposição: Um LLM quebra o agregado em linguagem natural em afirmações atômicas e resolve referências vagas (por exemplo, pronomes) usando o contexto original.
2. Mapeamento Lógico: Afirmações são mapeadas para estruturas lógicas:
   • Existencial/Universal: $\exists t, \forall t$
   • Cardinal/Proporcional: $\exists \ge k, \exists \ge \rho$
   • Ordinal/Aninhado: Classificação de grupos ou quantificadores aninhados (por exemplo, "Todos os locais têm >2 reclamações").
3. Geração de Consulta: Afirmações são compiladas em uma API estilo DataFrame usando operadores relacionais padrão (filter, map, aggregate) e operadores semânticos (chamadas de LLM baseadas em prompts).
   • filter(prompt): Filtragem semântica.
   • map(prompt): Extração de atributos semânticos.
   • aggregate: Mapeia para quantificadores (por exemplo, bool_or $\to$ $\exists$, count_if $\to$ cardinalidade).

B. Otimizações Conscientes de Verificação

O Evergreen introduz otimizações específicas para minimizar chamadas de LLM mantendo a correção:

1. Parada Antecipada: O motor de consultas usa um modelo de iterador.
   • Para $\exists$ (por exemplo, "alguns"), ele para assim que uma testemunha for encontrada.
   • Para $\forall$ (por exemplo, "todos"), ele para assim que um contraexemplo for encontrado.
   • Para afirmações cardinais/proporcionais, ele empurra a lógica de comparação para baixo para parar assim que o limite for matematicamente determinado, independentemente das tuplas restantes.
2. Ordenação por Relevância: Para tornar a parada antecipada eficaz, as tuplas são pré-classificadas por relevância. Um LLM gera uma consulta de pesquisa baseada na lógica da afirmação; as tuplas são classificadas por similaridade de embeddings e correspondência de palavras-chave para que "testemunhas" apareçam cedo no fluxo.
3. Estimativa com Sequências de Confiança (CS): Para casos onde a parada antecipada é impossível (por exemplo, verificar se uma afirmação universal é verdadeira), o Evergreen usa Sequências de Confiança Válidas a Qualquer Momento. Diferentemente dos intervalos de confiança clássicos, as CSs permitem monitoramento contínuo sem inflar as taxas de erro. O sistema para de amostrar assim que o intervalo de confiança prova que a afirmação é verdadeira ou falsa com alta probabilidade.
4. Otimizações de Propósito Geral:
   • Fusão de Operadores: Combina múltiplos operadores semânticos (por exemplo, filter + map) em uma única chamada de LLM por tupla.
   • Filtragem por Similaridade: Um pré-filtro leve usando embeddings para descartar tuplas obviamente irrelevantes antes de invocar o LLM.
   • Cache de Prompts: Reutiliza respostas de LLM para prompts idênticos em diferentes afirmações.

C. Citações via Proveniência de Semianel

Para fornecer explicações, o Evergreen trata citações como proveniência de dados. Ele utiliza proveniência de semianel para lógica de primeira ordem:

• Cada tupla é anotada com tokens indicando se ela satisfaz a fórmula da afirmação.
• O sistema deriva um conjunto mínimo de tokens (monômios) que justificam o resultado.
• Se uma afirmação for verdadeira, retorna o conjunto mínimo de testemunhas. Se falsa, retorna o conjunto mínimo de contraexemplos. Isso garante que as explicações sejam concisas e matematicamente fundamentadas.

3. Contribuições Principais

1. Formalização Lógica: Identificou tipos comuns de afirmações em agregados semânticos e mapeou-os para estruturas lógicas bem definidas (existencial, universal, cardinal, proporcional, ordinal, aninhado).
2. Compilação Declarativa: Demonstrou como compilar afirmações em linguagem natural em consultas declarativas de verificação semântica, transferindo o ônus da otimização do LLM para o motor de consultas.
3. Otimizações Novas: Introduziu técnicas específicas de verificação (Parada Antecipada, Ordenação por Relevância, Estimativa de Sequência de Confiança) que reduzem drasticamente o custo e a latência.
4. Proveniência Formal: Aplicou proveniência de semianel para formalizar citações como explicações mínimas para resultados de verificação.
5. Avaliação Abrangente: Construiu um benchmark de 16 afirmações diversas sobre conjuntos de dados reais de avaliações de restaurantes para avaliar o sistema.

4. Resultados Experimentais

O sistema foi avaliado em três conjuntos de dados do Yelp (1,6k–1,8k tuplas cada) contra baselines: LLM como juiz (base_rm), Agente Aumentado por Recuperação (rag_agent) e um Evergreen Não Otimizado (evg_unopt).

• Qualidade vs. Custo:
  • LLMs Fortes: O Evergreen com um LLM forte (Opus) alcançou F1 = 1,00 (verificação perfeita) enquanto reduziu o custo em 3,2$\times$ e a latência em 4,0$\times$ comparado à versão não otimizada.
  • LLMs Fracos: O Evergreen usando um LLM fraco (Llama 8B) superou uma baseline de LLM forte como juiz (Opus) na pontuação F1 (0,89 vs. 0,82) com 48$\times$ menor custo e 2,3$\times$ menor latência.
  • vs. Agente RAG: O Evergreen igualou ou superou a qualidade do agente RAG com um LLM fraco a 63$\times$ menor custo e 4,2$\times$ menor latência.
• Estudo de Ablação:
  • Parada Antecipada foi a otimização mais crítica, reduzindo custo/latência em 6,7$\times$.
  • Estimativa (CS) e Cache de Prompts forneceram economias de 2$\times$–2,7$\times$.
  • Desativar otimizações geralmente degradou o desempenho significativamente, provando a necessidade da abordagem neuro-simbólica.
• Robustez: Mesmo com modelos mais fracos, o Evergreen manteve alta precisão de proveniência (0,84–0,99), garantindo que as citações fornecidas fossem confiáveis.

5. Significado

O Evergreen representa uma mudança significativa na forma como sistemas de dados semânticos lidam com a confiabilidade.

• Sinergia Neuro-Simbólica: Combina efetivamente a compreensão semântica de LLMs com a otimização rigorosa e o raciocínio lógico de motores de consultas de banco de dados.
• Escalabilidade: Resolve os gargalos de "janela de contexto" e "custo" que atualmente impedem o uso confiável de LLMs em análises de dados de produção.
• Confiabilidade: Ao fornecer citações mínimas e matematicamente fundamentadas, vai além das saídas de "caixa preta" de LLMs, tornando agregados semânticos auditáveis e confiáveis para uso empresarial.
• Direção Futura: Abre caminho para "Restrições de Integridade Semântica", onde sistemas de banco de dados podem automaticamente impor correção em insights gerados por LLMs.

Em resumo, o Evergreen demonstra que, ao tratar a verificação de afirmações como um problema de otimização de consultas, os sistemas podem alcançar qualidade de verificação perfeita ou quase perfeita a uma fração do custo e da latência das abordagens atuais baseadas em LLMs.