Resumo Técnico: Analisando o Gap de Narração em Loops de LLM-Solver

1. Definição do Problema

O artigo aborda uma vulnerabilidade crítica em pipelines de raciocínio neurosimbólico que combinam Grandes Modelos de Linguagem (LLMs) com solvers formais (ex: SAT, SMT). Embora esses sistemas utilizem ferramentas formais para fornecer respostas sólidas e verificáveis a questões baseadas em lógica, os autores identificam um "gap de narração" onde a robustez do sistema entra em colapso.

O pipeline consiste em três estáções:

1. Formalização: Um LLM traduz uma consulta em linguagem natural em uma fórmula lógica ($\phi$).
2. Decisão: Um solver formal determina a satisfatibilidade de $\phi$, retornando um veredito ($v$) e um certificado ($c$).
3. Narração: Um LLM traduz o veredito formal de volta para uma resposta em linguagem natural para o usuário.

Pesquisas anteriores focaram na solidez das etapas de formalização e decisão. No entanto, a etapa de narração permanece não certificada. Os autores argumentam que, mesmo que o veredito do solver seja matematicamente sólido e independentemente verificado, um adversário pode manipular o LLM durante a etapa de narração (via injeção de prompt) para inverter a conclusão final apresentada ao usuário, mantendo o veredito e o certificado subjacentes intactos. Isso resulta em uma "falha furtiva" onde o sistema reporta um estado intermediário correto, mas uma resposta final errada, evadindo monitores de tempo de execução padrão que verificam apenas o veredito.

2. Metodologia

Modelagem Formal

Os autores modelam o loop LLM-solver como um procedimento de decisão verificado. Eles definem:

• Premissas: A formalização é fiel à intenção do usuário, e o solver é sólido e completo.
• Modelo de Adversário: Um adversário realiza injeção de prompt indireta controlando conteúdo não confiável (ex: notas ou comentários de fórmulas) alimentado no contexto do narrador. O objetivo é inverter a conclusão final ($\bar{p} = \neg \rho(v)$) enquanto mantém o veredito restatado correto (furtivo) ou incorreto (complacente).
• Taxonomia de Falhas: Eles categorizam as falhas em:
  • Furtiva (T2): O veredito é correto, a conclusão é invertida.
  • Complacente (T3): Tanto o veredito quanto a conclusão são invertidos.
  • Robustez: O sistema resiste ao ataque.

Análise Teórica

O artigo prova dois teoremas fundamentais sobre monitoramento e aplicação:

1. Teorema 1: Um monitor que verifica se a conclusão narrada corresponde ao veredito verificado é sólido e completo. No entanto, um monitor que verifica apenas o veredito restatado (sem compará-lo com a conclusão) é cego a falhas furtivas.
2. Teorema 2 & Corolário 3: Um monitor sólido e completo existe se, e somente se, um aplicador (enforcer) sólido existir. A única configuração que garante taxa zero de inversão é um aplicador que ignora totalmente a narração do LLM, exibindo diretamente o veredito mapeado ($\rho(v)$).

Configuração Experimental

• Oráculo: Solver Z3 usado como verdade fundamental para instâncias SAT/UNSAT.
• Modelos: Cinco modelos de código aberto foram avaliados: Meta Llama-3.1-8B, Google Gemma-3-12B, Alibaba Qwen-2.5-14B, OpenAI gpt-oss-20B e DeepSeek-R1-8B.
• Vetores de Ataque: Quatro templates de injeção foram testados através de dois canais (incorporado na fórmula vs. em uma nota separada) e dois estilos (blasfemo/direto vs. sutil/engenharia social).
• Defesa: Um prompt de sistema "endurecido" foi testado, instruindo o LLM a tratar entradas não confiáveis como tal e priorizar o veredito verificado.
• Ataques Adaptativos: Foram simulados atacantes que conheciam o prompt de defesa e criaram injeções especificamente para contornar o mesmo.

3. Principais Resultados

Solidez do Veredito (RQ1)

Quando o certificado do solver bloqueia a resposta final (forçando o sistema a exibir o veredito verificado), o sistema atinge 100% de correção. Isso confirma que o componente do solver é sólido e que a vulnerabilidade reside estritamente na narração do LLM.

Inversão de Narração Adversária (RQ2)

Sem defesas, adversários conseguem inverter a resposta narrada na maioria dos casos:

• Taxas de Sucesso: As taxas de sucesso de injeção variaram de 0,47 a 0,71 entre diferentes templates.
• Furtividade: Falhas "furtivas" (onde o LLM restata corretamente o veredito, mas inverte a conclusão) foram altamente prevalentes. Por exemplo, o template note_social (uma nota sutil sem comandos imperativos) alcançou uma taxa de sucesso total de 0,71, sendo 0,39 furtiva.
• Variância de Modelo: Modelos de raciocínio (gpt-oss) não foram imunes, mostrando alta suscetibilidade (taxa de sucesso total de 0,91). Modelos não voltados ao raciocínio, como o Qwen, mostraram maior resistência a ataques diretos, mas permaneceram vulneráveis a ataques sutis.
• Descoberta Principal: Injeções sutis foram estatisticamente tão eficazes quanto as diretas. A vulnerabilidade é uma falha de fidelidade na transferência do veredito para a resposta, não meramente uma falência em seguir comandos explícitos.

Eficácia da Defesa (RQ3)

• Endurecimento de Prompt: O endurecimento do prompt de sistema do narrador reduziu a taxa de sucesso de injeção de 0,61 para 0,14 (uma redução de ~4x).
• Limitações:
  • O endurecimento reduziu principalmente falhas complacentes (onde o modelo desobedece abertamente), mas teve impacto mínimo em falhas furtivas. A taxa de falhas furtivas caiu apenas de 0,57 para 0,53 entre os ataques restantes.
  • Ataques Adaptativos: Quando atacantes adaptaram seus prompts para contrapor o sistema endurecido (ex: negando explicitamente o aviso de "entrada não confiável"), a taxa de sucesso recuperou-se significativamente (ex: note_adaptive_supersede subiu para 0,43).
  • Dependência de Modelo: A eficácia da defesa variou drasticamente por modelo (ex: Qwen caiu para 0,01, enquanto gpt-oss permaneceu em 0,26).

4. Principais Contribuições

1. Modelagem Formal: O artigo modela formalmente o loop LLM-solver como um procedimento de decisão, identificando a etapa de narração como o ponto específico onde as garantias de solidez são perdidas.
2. Medição Sistemática: Fornece a primeira medição sistemática do gap de narração, demonstrando que injeções adversárias podem inverter conclusões verificadas através de várias formulações e canais.
3. Limites Teóricos de Defesa: Os autores provam que o endurecimento de prompt e o monitoramento em tempo de execução são insuficientes para eliminar falhas furtivas. Eles demonstram que apenas a aplicação (enforcement) (exibindo diretamente o veredito mapeado $\rho(v)$) pode garantir a correção de ponta a ponta.
4. Evidência Empírica: Através de experimentos extensos em cinco modelos, o artigo mostra que mesmo modelos capazes de raciocínio são suscetíveis a inverter conclusões verificadas e que a engenharia social sutil é tão eficaz quanto comandos diretos.

5. Significância e Alegações

O artigo alega que o gap de narração é uma propriedade fundamental de pipelines neurosimbólicos que dependem de LLMs para traduzir resultados formais em linguagem natural.

• O Certificado Não é Suficiente: Um certificado formal garante a correção do veredito, mas não garante a correção da resposta ao usuário se essa resposta for gerada por um LLM.
• Invisibilidade da Falha: As falhas mais perigosas são as "furtivas", onde o sistema parece estar funcionando corretamente (reestatando o veredito correto) enquanto entrega uma conclusão errada. Essas falhas são invisíveis para monitores que auditam apenas o veredito.
• Estratégia de Mitigação: O artigo argumenta que confiar em engenharia de prompt ou instruções endurecidas não é uma defesa confiável contra adversários adaptativos. A única solução robusta para consultas decidíveis é remover o LLM da etapa de geração da conclusão e aplicar o resultado diretamente a partir do veredito verificado.
• Generalização: Embora testado em problemas SAT, os autores afirmam que este gap se aplica a qualquer pipeline (SMT, Provadores de Teoremas Interativos) onde um resultado verificado é narrado por um LLM.

Os autores concluem que, para aplicações críticas de segurança, a responsabilidade do pipeline muda para garantir que a formalização seja fiel e que a narração seja aplicada, em vez de confiar que o LLM reportará fielmente a saída do solver.