Resumo Técnico: Aplicação Formal de Políticas para Sistemas Agênicos do Mundo Real

Declaração do Problema

Sistemas agênicos contemporâneos, que integram Modelos de Linguagem de Grande Escala (LLMs) com ferramentas externas para executar tarefas como envio de e-mails, execução de código e consulta a bancos de dados, carecem de mecanismos robustos para fazer cumprir políticas de segurança e organizacionais. As abordagens atuais dependem predominantemente da incorporação de políticas em linguagem natural dentro do prompt do sistema de um agente, delegando a conformidade às capacidades de raciocínio do agente. Esta metodologia sofre de três limitações críticas:

1. Falta de Garantias Formais: A conformidade é heurística e contingente à capacidade do modelo de seguir instruções, não oferecendo aplicação determinística.
2. Incapacidade de Expressar História Causal: Prompts em linguagem natural lutam para fazer cumprir políticas dependentes da história causal de uma execução (por exemplo, "permitir apenas a ação X se a aprovação Y foi obtida em uma etapa anterior").
3. Escalabilidade em Sistemas Multiagente: Abordagens existentes são inadequadas para ambientes multiagente onde a aplicação deve raciocinar através de limites de agentes e ordenações parciais de eventos, em vez de traços lineares.

Essas lacunas deixam os sistemas agênicos vulneráveis a injeção de prompts, uso não autorizado de ferramentas e reestruturação adversária, limitando sua implantação segura em cenários do mundo real.

Metodologia

Os autores propõem FORGE (FOrmal Runtime Guarantee Enforcement), um framework que trata a aplicação de políticas como uma preocupação transversal, fundamentada em Programação Orientada a Aspectos (AOP). O framework desacopla a lógica de políticas do raciocínio do agente, aplicando regras em cada ponto de decisão relevante para a política sem modificar os agentes subjacentes.

Arquitetura Central

1. Formulação Orientada a Aspectos:

   • Pontos de Junção: Definidos como ações candidatas (por exemplo, invocações de ferramentas) aguardando autorização.
   • Pointcuts: Funções booleanas sobre o estado de execução que determinam a quais ações uma regra se aplica.
   • Advice: O cálculo de aplicação realizado por um Monitor de Referência, que avalia a política e retorna um veredito Allow (Permitir) ou Deny (Negar).
   • Weaver (Tecelão): Uma camada de instrumentação que intercepta chamadas de ferramentas, suspende a execução, consulta o monitor e prossegue apenas após aprovação.

2. Linguagem de Políticas (Datalog):

   • As políticas são especificadas em Datalog com negação estratificada e extensões de função externa.
   • Expressividade: Suporta especificação declarativa de regras e recursão, permitindo a definição de relações transitivas (por exemplo, cadeias de supervisão) e controle de acesso baseado em relacionamento (ReBAC).
   • Analisabilidade: Permite análises estáticas para detecção de contradições, redundância, subsumção e alcançabilidade condicional, permitindo que os autores verifiquem a intenção da política e resolvam ambiguidades inerentes a especificações em linguagem natural.
   • Tradução: Um pipeline traduz documentos de política em linguagem natural em programas Datalog, anotados com links de nível de cláusula ao texto fonte para verificação de cobertura e entailment.

3. Substrato de Políticas e Contrato de Ambiente:

   • Substrato ($\Sigma$): Um conjunto de predicados abstratos (Função, Proveniência, Específicos de Domínio) que descrevem o contexto de execução.
   • Serviço de Observabilidade: Mantém um grafo de dependência causal de eventos (mensagens, chamadas de ferramentas, resultados) e popula os predicados do substrato.
   • Contrato Assume/Guarantee: A correção é garantida sob a suposição de que o ambiente satisfaz um contrato: deve preencher de forma sólida e suficiente os predicados do substrato com fatos consistentes com suas interpretações pretendidas (por exemplo, linhagem causal precisa). Se o contrato valer, as decisões do monitor de referência coincidirão com a semântica pretendida da política.

Contribuições Principais

1. Framework Formal para Aplicação Agênica: O artigo apresenta o primeiro framework capaz de aplicar automaticamente políticas em sistemas multiagente com garantias formais de correção, utilizando um paradigma AOP para separar preocupações transversais da lógica central.
2. Especificação de Políticas Baseada em Datalog: Introduz o Datalog como linguagem de política para sistemas agênicos, aproveitando seu suporte a recursão e análise estática para lidar com políticas complexas e com estado que prompts em linguagem natural não conseguem expressar.
3. O Sistema FORGE: Uma implementação prática composta por um tecelão de aspectos, um serviço de observabilidade e um monitor de referência. O FORGE instrumenta frameworks de agentes (por exemplo, Langroid, $\tau^2$) para aplicar políticas em tempo de execução sem alterar o código do agente.
4. Teorema de Correção: Os autores provam um teorema assume/guarantee afirmando que, se o ambiente satisfizer o contrato do substrato, as decisões de aplicação em tempo de execução são corretas em relação à semântica pretendida da política.

Resultados da Avaliação

O framework foi avaliado em três estudos de caso quantitativos e duas implantações do mundo real:

1. Defesa contra Injeção de Prompt (Fluxo de Informação):

   • Objetivo: Prevenir exfiltração de dados via injeção de prompt.
   • Resultado: Agentes não instrumentados tiveram uma taxa de sucesso de ataque de 100%. O FORGE reduziu isso para 0%, mantendo 100% de utilidade em tarefas benignas.
   • Sobrecarga: A latência aumentou em ~12–15 segundos por tentativa; o aumento de custo foi insignificante (<$0,003).

2. Fluxos de Trabalho de Atendimento ao Cliente ($\tau^2$-Bench):

   • Objetivo: Aplicar regras de negócios (cancelamentos, reembolsos, bagagem) em três modelos de ponta.
   • Resultado: A conformidade melhorou de 58% para 98%. O sucesso da tarefa foi preservado ou melhorado (por exemplo, as taxas de aprovação subiram de 58% para 98%).
   • Sobrecarga: A latência de ponta a ponta aumentou de 19% a 38% (decisão de autorização mediana de sub-milissegundo); o aumento de custo foi < $0,05 por tentativa.

3. Farmacovigilância Multiagente (MALADE):

   • Objetivo: Aplicar fluxos de trabalho de aprovação para acesso a dados da FDA em um pipeline multiagente.
   • Resultado: Acessos não autorizados à FDA caíram de 40 para 0 em 15 tentativas. A precisão da tarefa permaneceu em 100% (15/15 previsões corretas).
   • Sobrecarga: A latência aumentou de 72,5s para 95,4s (impulsionada por ciclos bloqueados-então-retentativa); o custo aumentou de $0,072 para $0,103 por tentativa.

Implantações do Mundo Real: O artigo também descreve aplicação bem-sucedida no OpenClaw (aplicação de privacidade entre agentes) e no VS Code Copilot Chat (bloqueio de git push até que a análise estática seja aprovada).

Significado e Alegações

O artigo alega que o FORGE representa um avanço significativo ao preencher a lacuna entre especificações de políticas informais e aplicação rigorosa em tempo de execução em sistemas agênicos. Seu significado principal reside em:

• Garantias Determinísticas: Diferentemente de abordagens baseadas em prompts, o FORGE elimina violações de políticas por construção, desde que o contrato de ambiente seja atendido.
• Aplicação com Estado: Suporta exclusivamente políticas dependentes de história causal e relações transitivas entre múltiplos agentes, uma capacidade ausente em sistemas existentes sem estado ou baseados em traços lineares.
• Modularidade: Ao tecer a aplicação no tempo de execução, permite a aplicação de políticas organizacionais complexas sem exigir alterações no raciocínio interno do agente ou nas ferramentas subjacentes.
• Analisabilidade: O uso de Datalog permite a detecção de contradições e ambiguidades de políticas antes da implantação, tratando políticas como artefatos revisáveis em vez de prompts opacos.

Os autores mantêm modéstia em relação ao pipeline de tradução, reconhecendo que, embora a tradução de linguagem natural para Datalog seja realizada via LLMs, atualmente carece de garantias formais de correção e exige revisão manual e validação iterativa. Eles identificam a robustez dessa tradução e a extensão para autores de políticas não especialistas como problemas abertos para trabalhos futuros.