Autoformalization of Agent Instructions into Policy-as-Code

Resumo Técnico: Autoformalização de Instruções de Agentes em Política-como-Código

Declaração do Problema
A implantação de agentes autônomos de Grandes Modelos de Linguagem (LLM) em domínios de alto risco (ex: saúde) apresenta um compromisso crítico de segurança: os agentes requerem privilégios elevados para realizar tarefas complexas, mas esses privilégios expandem a superfície de ataque para técnicas adversariais, como o prompt injection. As práticas atuais da indústria dependem fortemente de salvaguardas probabilísticas, como classificadores de segurança ajustados (fine-tuned, ex: Llama Guard) ou direcionamento baseado em prompts. Embora esses métodos ofereçam alguma utilidade, eles carecem de garantias formais e são frequentemente inadequados para aplicações de segurança crítica onde a aplicação determinística é necessária. Por outro lado, a aplicação simbólica codificada manualmente oferece garantias formais, mas falha em escalar para a amplitude e complexidade das especificações de políticas do mundo real.

Metodologia
Os autores propõem um pipeline de autoformalização que traduz instruções de agentes em linguagem natural, descrições de ferramentas do Protocolo de Contexto de Modelo (MCP) e documentos de política em políticas formalmente verificadas escritas na Linguagem de Política Cedar. Este pipeline opera via um loop gerador-crítico estruturado como um "Sanduíche de Verificação" com três camadas distintas:

1. A Camada de Fundamentação (Base): Esta camada estabelece a fundação ao extrair entidades, identificar esquemas de ferramentas (ex: esquemas JSON da OpenAI) e definir uma ontologia de principal-recurso-ação. Ela garante que o agente opere dentro de um ambiente estruturado onde as ações potenciais mapeiam para entidades do mundo real e identificadores de sistema válidos. Crucialmente, ela gera programaticamente um esquema Cedar a partir das definições de ferramentas MCP para servir como um mecanismo estrito de verificação de tipos.
2. A Camada do Modelo (Meio): Utilizando LLMs de última geração, esta camada interpreta instruções em linguagem natural e gera conjuntos de políticas candidatas. Ela aproveita o conhecimento paramétrico para propor políticas que reflitam a lógica pretendida do agente.
3. A Camada de Segurança (Topo): Esta camada emprega um mecanismo de duplo crítico para validar os candidatos:
   • Crítico Rígido (Hard Critic): Uma verificação determinística e programática usando as ferramentas de análise estática integradas do Cedar. Ele verifica a sintaxe, impõe a conformidade do esquema e detecta contradições lógicas (ex: políticas vazias ou regras conflitantes).
   • Crítico Suave (Soft Critic): Um LLM-como-juiz que avalia o alinhamento semântico contra uma rubrica predefinida. Ele garante que a lógica formal reflita fielmente o espírito das instruções originais em linguagem natural e dos documentos de política.

O loop itera, alimentando o feedback dos dois críticos de volta ao gerador até que o conjunto de políticas passe tanto nos testes rígidos quanto nos suaves. As políticas resultantes são aplicadas em tempo de execução por um motor de política externo e determinístico, desacoplando a lógica de segurança do contexto de raciocínio do LLM.

Principais Contribuições

• Arquitetura de Sanduíche de Verificação: Uma abordagem em camadas inovadora para autoformalização que combina fundamentação, raciocínio generativo e verificação de modo duplo (rígido/suave) para traduzir política não estruturada em código formal.
• Implementação de Código Aberto: O lançamento de um harness de política de código aberto para estruturas de agentes implementadas em Cedar, incluindo bindings customizados em Python.
• Autoformalização Escalável: Um pipeline que converte automaticamente cartões de agentes (instruções + esquemas de ferramentas) em políticas de autorização verificadas, abordando as limitações de escalabilidade da aplicação simbólica manual.
• Estrutura de Avaliação: Uma avaliação rigorosa no benchmark MedAgentBench, comparando a abordagem autoformalizada com salvaguardas simbólicas codificadas manualmente anteriores.

Resultos
O sistema foi avaliado no MedAgentBench, um benchmark para agentes de uso de ferramentas em prontuários eletrônicos (EMR). O estudo comparou três condições: Ferramentas HTTP puras, uma Linha de Base com ferramentas MCP tipadas, e uma condição de Salvaguarda (Guardrail) usando as políticas Cedar dos autores versus as salvaguardas simbólicas codificadas manualmente de Hong et al.

• Cobertura: O pipeline de autoformalização cobriu substancialmente mais da especificação de linguagem natural de 88 regras do que a abordagem codificada manualmente, que implementou apenas 23 regras.
• Taxas de Bloqueio: Na condição de "Salvaguarda", o motor de política Cedar bloqueou uma porcentagem significativamente maior de violações de política em comparação com a linha de base codificada manualmente, particularmente em cenários adversariais.
  • No conjunto de dados Original, o Cedar bloqueou 55,7% das trajetórias (167/300), enquanto as salvaguardas codificadas manualmente bloquearam 0% (por construção, já que cobriam apenas um subconjunto de regras).
  • No conjunto de dados Adversarial, o Cedar bloqueou 85,7% das trajetórias (42/49).
• Análise de Tentativa de Escrita: Ao filtrar as trajetórias contendo tentativas reais de escrita (requisições POST), a taxa de bloqueio do Cedar aproximou-se de 100% (ex: 100,0% na condição de Salvaguarda Adversarial), demonstrando que o sistema impede efetivamente modificações de dados não autorizadas quando elas ocorrem.
• Robustez: O sistema impediu com sucesso o "jailbreaking" e o prompt injection indireto ao aplicar as regras fora da janela de contexto do LLM.

Significância e Alegações
O artigo alega que esta abordagem fornece fortes garantias formais sobre o comportamento do agente, uma capacidade ausente nas salvaguardas probabilísticas. Ao desacoplar a aplicação da política do contexto de raciocínio do LLM, a arquitetura mitiga o risco de um atacante convencer a camada de segurança a ignorar suas regras. O uso do Cedar garante que as políticas sejam legíveis por humanos, auditáveis e formalmente verificadas, preenchendo a lacuna entre a flexibilidade da linguagem natural e o rigor da lógica simbólica.

Os autores reconhecem um "compromisso entre fricção e utilidade", observando que políticas excessivamente restritivas podem degradar a utilidade do agente. Eles postulam que o Loop Gerador-Crítico, particularmente a inclusão de um crítico suave, é essencial para alcançar uma "zona de equilíbrio" (Goldilocks zone) onde os agentes são suficientemente restringidos, mas permanecem funcionais. O trabalho demonstra que a autoformalização pode escalar a aplicação de políticas para especificações complexas do mundo real sem sacrificar as garantias formais exigidas em domínios de alto risco.

Limitações e Trabalhos Futuros
Os autores observam que o Cedar é, por design, sem estado (stateless), o que limita sua capacidade de lidar com fluxos de trabalho de múltiplos turnos dependentes da ordem das ações ou contexto persistente. Trabalhos futuros visam abordar isso integrando lógica temporal para sequências de pré-requisitos e desenvolvendo políticas conscientes de memória que permitam ao motor referenciar o histórico de trajetória de um agente.