Resumo Técnico: Interpretação Agêntica para Análise de Programas Baseada em LLM

1. Declaração do Problema

Os Modelos de Linguagem de Grande Escala (LLMs) oferecem capacidades únicas para análise de programas ao acessar informações além do código-fonte, como documentação, avisos de segurança, metadados específicos de versão e contratos informais de API. No entanto, confiar em LLMs para análise de "um único disparo" (one-shot) de programas inteiros é inerentemente frágil por três razões principais:

1. Sensibilidade ao Contexto: Estudos empíricos indicam que o desempenho do modelo degrada-se à medida que o comprimento do contexto e a complexidade da tarefa aumentam, e os resultados dependem fortemente da ordenação das informações no prompt. Evidências críticas (por exemplo, um aviso de segurança específico) podem ser fornecidas, mas não utilizadas de forma confiável.
2. Falta de Estado Persistente: Respostas monolíticas de LLM carecem de um estado persistente para rastrear quais alegações específicas foram apoiadas, refutadas ou deixadas em aberto. Isso dificulta o tratamento de raciocínios autocontraditórios ou de raciocínios que não sustentam suas próprias conclusões.
3. Ausência de Estrutura de Dependência: Uma resposta de disparo único não fornece nenhum mecanismo para feedback. Se descobertas posteriores revelarem que uma pergunta anterior foi delimitada incorretamente ou que um componente a montante requer reexame sob uma hipótese diferente, uma resposta não estruturada não pode facilitar esse refinamento iterativo.

Consequentemente, há necessidade de um framework que faça a ponte entre o prompting ad-hoc de LLMs e a análise estática totalmente especificada, especificamente para análises de programas dependentes de evidências, onde os fatos relevantes não estão totalmente contidos no código-fonte ou em especificações formais.

2. Metodologia: Interpretação Agêntica

O artigo propõe a Interpretação Agêntica, um framework que aplica a disciplina da análise estática baseada em reticulados (lattices) ao raciocínio orientado por LLMs. A metodologia decompõe objetivos de análise de alto nível em alegações localizadas ancoradas a pontos do programa e limites de componentes, gerenciando sua evolução através de um reticulado de altura finita e um algoritmo de lista de trabalho.

2.1 Componentes Principais

• Grafo de Avaliação ($G^*$): Uma extensão de um grafo derivado do programa ($G_{prog}$) que inclui:
  • Nós Auxiliares: Nós representando interações entre componentes ou objetivos que não mapeiam para um único ponto do programa.
  • Arestas de Contexto: Arestas de fluxo direto que garantem que, quando uma alegação no nó $n$ é avaliada, ela receba o estado de avaliação atual e as evidências de seus predecessores.
  • Arestas de Feedback: Arestas de fluxo reverso que acionam a reavaliação de nós a montante quando uma avaliação a jusante muda (por exemplo, uma alegação de composição refutada aciona uma busca direcionada em um componente opaco).
• Domínio de Avaliação (Reticulado): Um semirreticulado de união (join-semilattice) de altura finita ($A$) que resume o estado evidencial de uma alegação.
  • O artigo ilustra isso com o reticulado AGraded: $\{ \perp, w, s \} \times \{ \perp, w, s \}$, onde a primeira coordenada representa evidências de suporte e a segunda representa evidências de refutação. Os valores variam de ausente ($\perp$) a fraco ($w$) a forte ($s$).
  • O reticulado é um domínio epistêmico sobre estados de evidência, não um domínio abstrato sobre estados concretos do programa. Ele registra se uma alegação foi apoiada ou refutada e a força dessa evidência.
• Acionador de Lista de Trabalho (Worklist Harness): Um laço de controle que gerencia o estado da análise.
  • Contextualização: Para um nó $n$, o acionador constrói um contexto de prompt ($\Gamma_n$) usando código-fonte, o objetivo de alto nível e as avaliações atuais dos nós predecessores.
  • Transformadores de Nó: O agente LLM realiza duas operações:
    1. Avaliação: Avalia alegações existentes contra o contexto, retornando uma avaliação atualizada e registros de evidência.
    2. Geração: Propõe novas alegações relevantes com base no contexto.
  • Propagação: Se a união (join) da nova avaliação com a avaliação antiga resultar em um aumento estrito na ordem do reticulado, os sucessores estendidos do nó são enfileirados para reavaliação.

2.2 O Processo de Análise

O processo é ilustrado através de uma revisão de segurança de um programa com componentes de terceiros opacos (um analisador JSON e um verificador de assinatura).

1. Inicialização: A lista de trabalho é semeada com todos os nós do programa e nós auxiliares.
2. Refinamento Iterativo:
   • Fase I: Avaliação independente inicial dos componentes (por exemplo, revisão da documentação do analisador e do verificador).
   • Fase II: Composição de evidências. O framework avalia alegações entre componentes (por exemplo, "Os componentes garantem conjuntamente a segurança?"). Se uma alegação de composição for fracamente refutada, as arestas de feedback acionam uma reinvestigação dos componentes a montante.
   • Fase III: Refinamento orientado por feedback. O contexto da composição refutada (por exemplo, "o processador não realiza nenhuma validação") orienta o LLM a realizar uma busca direcionada por vulnerabilidades específicas (por exemplo, poluição de protótipo) em vez de uma revisão ampla.
   • Fase IV: Estabilização. A evidência a montante fortalecida propaga-se para frente, levando a uma forte refutação do objetivo global. A lista de trabalho esvazia-se quando não ocorrem mais aumentos estritos na avaliação.

3. Contribuições Principais

O artigo apresenta três contribuições principais:

1. Proposta de Framework: Introduz a Interpretação Agêntica como uma abordagem estruturada para análise de programas dependentes de evidências, identificando um domínio de problema adequado onde LLMs são necessários, mas o prompting direto é insuficiente.
2. Modelo Formal: Formaliza o modelo central, definindo o grafo de avaliação, o domínio de avaliação, os transformadores de nó e o algoritmo de lista de trabalho.
3. Caracterização do Espaço de Design: Explora o espaço de design, incluindo:
   • Reticulados de Avaliação: Discutindo trade-offs entre reticulados grosseiros (por exemplo, presença/ausência) e reticulados de granularidade fina (por exemplo, força, base de confiança). Introduz o AStratified, um domínio que rastreia a força da evidência e a base de confiança (por exemplo, "apenas modelo" vs. "verificado") separadamente.
   • Gerenciamento de Alegações: Abordando a canonicidade, granularidade e escopo das alegações.
   • Design de Consultas: Diferenciando entre consultas de avaliação (suporte/refutação) e consultas generativas (proposição de novas alegações).
   • Terminação: Provando que o algoritmo termina para reticulados de altura finita com geração de alegações limitada, mesmo na presença de respostas não determinísticas de LLMs, desde que as atualizações sejam monótonas (via união/join).

4. Resultados e Limitações

• Resultados: O artigo fornece um exemplo resolvido (uma revisão de segurança de um manipulador com componentes opacos) demonstrando como o framework decompõe um objetivo, utiliza laços de feedback para refinar a busca e estabiliza em uma avaliação final. Mostra como o framework pode detectar que um objetivo global de segurança foi violado, combinando evidências fracas de múltiplas fontes em uma forte refutação.
• Limitações:
  • O artigo descreve trabalho em andamento. Não inclui uma implementação prática ou avaliação experimental.
  • O framework garante terminação e limitação, mas não garante correção (soundness) no sentido tradicional (ou seja, não prova que as conclusões do LLM estão corretas). Torna o papel evidencial do LLM explícito e auditável.
  • O framework não pode corrigir um agente que consistentemente julga mal as evidências; apenas torna tais erros visíveis.
  • A prova de terminação depende da suposição de que as alegações nunca são revogadas e que as avaliações apenas aumentam via união. Mecanismos para revisão de crenças (rebaixamento de avaliações) são discutidos como trabalho futuro, exigindo substituição limitada ou recomputação epocal.

5. Significância

A significância deste trabalho reside na sua tentativa de trazer disciplina estrutural ao raciocínio baseado em LLMs na análise de programas. Ao afastar-se do paradigma "gerar-e-verificar" (que requer um verificador formal para a saída do LLM) e do paradigma "oráculo heurístico" (onde o LLM não pode afetar a correção), a Interpretação Agêntica visa um meio-termo.

É significativa para análises dependentes de evidências onde:

• Os fatos relevantes não são formalizáveis (por exemplo, contratos informais de API, avisos de segurança).
• Um verificador completo não existe.
• A análise requer a síntese de informações de diversas fontes não relacionadas a código.

O framework transforma o LLM de um gerador de caixa-preta em um componente limitado e auditável de um sistema de análise maior. Garante que a análise prossiga de maneira controlada e principista, permitindo a separação de preocupações: o LLM fornece evidências, e o acionador baseado em reticulados garante que a análise seja limitada e rastreável. Esta abordagem visa inspirar discussões futuras sobre o design de técnicas fundamentadas formalmente para sistemas agênticos na análise de programas.