Resumo Técnico: Continuação Fundamentada: Um Verificador de Runtime de Tempo Linear para Conversas de LLM

Declaração do Problema

Modelos de Linguagem de Grande Escala (LLMs) implantados em conversas de múltiplas voltas frequentemente geram continuações que são localmente fluentes e pragmaticamente plausíveis, mas desfundamentadas na história estabelecida da conversa. Essas saídas podem repousar em premissas, observações ou hipóteses que a conversa já abandonou ou revisou. Essa "lacuna de fundamentação" é empiricamente severa: estudos indicam que LLMs falham em revisar suposições incorretas mesmo quando voltas posteriores as contradizem, levando a uma queda significativa de desempenho em configurações de múltiplas voltas em comparação com interações de volta única. Além disso, essa lacuna é ativamente explorada por ataques de manipulação de contexto, onde agentes produzem continuações que são localmente consistentes, mas desconectadas de compromissos anteriores, potencialmente desencadeando ações não autorizadas.

Soluções existentes, como Geração Aumentada por Recuperação (RAG), abordam a fundamentação externa (rastreando alegações a documentos citados), mas falham na fundamentação interacional (rastreando alegações aos próprios compromissos evolutivos da conversa). Sistemas de memória conversacional geralmente rastreiam o que foi dito, mas carecem do mapa de dependência estrutural que conecta declarações às conclusões derivadas delas.

Metodologia

Os autores propõem um verificador de runtime que mantém um grafo de dependência explícito para rastrear a proveniência de alegações ao longo de uma conversa. O sistema opera por meio de uma arquitetura híbrida composta por um Interpretador de LLM e um Motor Simbólico.

1. Fundação Formal

O verificador é construído sobre quatro formalismos:

• Lógica Epistêmica Dinâmica (DEL): Modela o que os agentes sabem, acreditam e têm consciência.
• Raciocínio Abducativo: Gera hipóteses para explicar observações surpreendentes.
• Lógica da Consciência: Rastreia a expansão dos conjuntos de consciência dos agentes.
• Estruturas de Argumentação: Modela ataques e suportes entre argumentos (estilo Dung).

Estes são unificados em uma Estrutura de Dependência $D_t = (M_t, AF_t, Cmt_t, Dep_t)$, onde:

• $M_t$: Modelo de plausibilidade epistêmica (estados de conhecimento/crença).
• $AF_t$: Estrutura de argumentação (argumentos e relações de ataque).
• $Cmt_t$: Compromissos públicos dos agentes.
• $Dep_t$: Um mapa ligando argumentos às proposições que os sustentam.

2. A Taxonomia de 8 Operações

Um Interpretador de LLM classifica cada enunciado em uma de oito operações de atualização, que o Motor Simbólico aplica para atualizar a estrutura de dependência:

1. OBSERVAR: Anúncio público rígido (adiciona fatos).
2. HIPOTETIZAR: Upgrade lexicográfico suave (introduz hipóteses explicativas).
3. SUSTENTAR: Aumenta a plausibilidade de uma alegação com base em evidências.
4. ENFRAQUECER: Diminui a plausibilidade de uma alegação (ex.: via evidência contraditória).
5. REVISAR: Retirada rígida ou adição de aresta de ataque (abandona uma alegação).
6. EXPANDIR-CONSCIÊNCIA: Adiciona novas proposições aos conjuntos de consciência dos agentes.
7. RESOLVER: Compromisso consensual ou autoritativo com uma conclusão.
8. PERGUNTAR: Sinaliza uma observação não explicada como um problema abducativo.

3. Verificação e Retirada

• Verificação de Continuação Fundamentada: Para verificar se uma continuação candidata $c$ é fundamentada, o sistema verifica se existe um argumento $\alpha_c$ na estrutura de argumentação atual tal que $claim(\alpha_c) = \phi_c$ (a proposição assertada por $c$). Isso reduz-se a uma travessia de grafo no mapa de dependência.
• Retirada Seletiva: Se uma premissa $p$ for retirada, o sistema calcula $Affected(p)$, o conjunto de conclusões que perdem fundamentação. Isso é computado percorrendo o mapa de dependência para encontrar todos os argumentos $\alpha$ onde $p \in Dep(\alpha)$.
• Complexidade: A verificação por volta e a propagação de retirada são lineares no tamanho da representação do motor ($O(|Args| + |Att|)$), evitando o crescimento linear com o comprimento da conversa típico de métodos de replay de histórico.

Principais Contribuições

1. Verificador de Runtime para Fundamentação Interacional: Um sistema que verifica, a cada volta, se uma continuação candidata remonta a compromissos anteriores por meio de uma estrutura de dependência mantida, operando em tempo linear ao tamanho do estado do motor.
2. Substrato Formal Componível: Um framework unificado combinando DEL, argumentação e lógica da consciência com uma garantia de correção para retirada seletiva (Proposição 2.1). O sistema garante que, quando uma premissa é retirada, o conjunto de conclusões afetadas é livre de conflitos e bem definido.
3. Decomposição Correção-Fielidade: Os autores separam o problema em uma verificação estrutural correta (a lógica do motor, que é comprovadamente correta) e fiabilidade de extração (a capacidade do LLM de classificar corretamente operações e extrair dependências). Isso permite uma medição precisa de onde ocorrem falhas.
4. Validação Empírica: O sistema é avaliado em cenários controlados de múltiplos agentes e benchmarks externos, demonstrando sua capacidade de detectar premissas obsoletas e abster-se de confabulações onde as linhas de base falham.

Resultados

Cenários Controlados (Fase 2 e 3)

• Detecção de Premissas Obsoletas: Em um subconjunto de 15 itens de casos de "premissas obsoletas" (onde uma alegação depende de uma premissa retirada anteriormente), o verificador alcançou 100% de precisão, comparado a 93,3% para a linha de base apenas de LLM. O verificador identificou corretamente que uma recomendação baseada em uma hipótese abandonada era desfundamentada, enquanto a linha de base a tratou como plausível.
• Latência de Retirada: No regime limitado (onde hipóteses resolvidas/abandonadas são aposentadas), a latência do verificador estagna à medida que o comprimento da conversa aumenta, enquanto as linhas de base de replay de histórico crescem linearmente. Em 2.000 voltas, o verificador foi 84 vezes mais rápido do que reler o transcript completo.

Benchmarks Externos

• LongMemEval-KU (Oráculo): Em 78 itens testando atualizações de conhecimento com supersessão, o verificador (com conteúdo e recuperação) alcançou 89,7% de precisão, superando a linha de base apenas de LLM (88,5%) e uma linha de base transcript-RAG (87,2%). As vitórias foram concentradas em casos onde a linha de base confabulou em itens sem informações de suporte, enquanto o verificador absteve-se corretamente.
• LoCoMo: Em 60 itens oficiais de QA, o verificador foi competitivo com linhas de base aumentadas por recuperação, consistente com seu foco na fundamentação interacional em vez de puro recall de entidade-relação.

Robustez e Extração

• Precisão de Classificação: Com prompts "Definições" e "Estado-aumentado", o Interpretador de LLM alcançou altas pontuações F1 (ex.: 0,91 para Claude Sonnet 4 na Fase 2).
• Análise de Gargalo: A limitação primária é a fiabilidade de extração (a capacidade do LLM de mapear corretamente linguagem natural para operações formais), não a verificação estrutural em si. Especificamente, recuperar arestas de dependência entre hipóteses (ex.: quando uma nova hipótese subsume uma antiga) exigiu uma correção específica de esquema na operação RESOLVE, que não foi alcançável apenas via engenharia de prompts.

Significado e Alegações

O artigo afirma fornecer o primeiro mecanismo de runtime que vincula estruturalmente a continuação de um agente à sua história de interação real, abordando uma vulnerabilidade crítica em agentes LLM implantados.

• Segurança: Oferece uma defesa contra ataques de manipulação de contexto, garantindo que ações sejam tomadas apenas se forem suportadas pelo grafo de dependência atual.
• Confiabilidade: Permite abstenção correta. Quando uma continuação carece de suporte, o sistema a sinaliza como "desfundamentada" em vez de alucinar uma justificativa que soa plausível.
• Eficiência: Ao manter um grafo de dependência simbólico, alcança verificação e propagação de retirada em tempo linear, tornando-o escalável para conversas de longo horizonte onde reler o histórico é computacionalmente proibitivo.
• Garantias Formais: O sistema fornece uma garantia livre de conflitos para retirada seletiva, garantindo que o estado da conversa permaneça logicamente consistente após a retirada de premissas.

Os autores permanecem modestos, observando que a eficácia do sistema é limitada pela capacidade do LLM de extrair fielmente a estrutura formal da linguagem natural, e que a implementação atual foca na fundamentação interacional em vez de recuperação factual externa (embora o framework possa ser estendido para o último).