Resumo Técnico: Verificação Probabilística Eficiente e Robusta para Agentes de IA

Declaração do Problema

A implantação de agentes de IA baseados em Grandes Modelos de Linguagem (LLMs) em ambientes digitais complexos introduz riscos de segurança críticos, particularmente quando os agentes possuem acesso programático a interfaces de sistema, como terminais e sistemas de arquivos. Embora o monitoramento em tempo de execução via monitores de referência seja uma solução para a aplicação de políticas de segurança, as abordagens existentes limitam-se a políticas determinísticas. Em cenários práticos, os agentes frequentemente dependem de componentes de nível superior (ex: detectores de PII, ferramentas de redação ou classificadores) que produzem saídas probabilísticas com taxas de falha inerentes.

Os monitores determinísticos atuais lidam com essa ambiguidade aplicando limiares locais para converter saídas probabilísticas em decisões binárias. Essa discretização cria um equilíbrio frágil entre segurança e utilidade:

• Limiares altos correm o risco de não bloquear ações prejudiciais (falsos negativos).
• Limiares baixos correm o risco de bloquear ações seguras (falsos positivos).
• Suposições de Independência: Técnicas padrão de inferência probabilística (ex: Contagem de Modelos Pesados) frequentemente assumem que os fatos base são mutuamente independentes. Em configurações de agentes, essa suposição é frequentemente inválida; por exemplo, uma ferramenta de redação falhar em um arquivo pode estar perfeitamente correlacionada com sua falha em outro devido ao conteúdo compartilhado ou ao comportamento da ferramenta. Confiar na independência pode levar a uma subestimação severa do risco durante o encadeamento de múltiplas etapas de ferramentas.

O artigo aborda a necessidade de um framework de verificação que preserve o contexto probabilístico contínuo, lide com correlações arbitrárias entre predicados sem assumir independência e forneça limites superiores rigorosos e robustos sobre as probabilidades de violação de política em tempo real.

Metodologia

O framework proposto modela a execução do agente como um problema de otimização robusta à distribuição sobre uma trajetória de execução. A metodologia consiste em quatro etapas principais:

1. Modelagem Datalog Probabilística

O traço de execução do agente é compilado em um programa Datalog onde:

• Fatos Base ($F$): Representam observações iniciais do ambiente (ex: "o arquivo A contém PII") parametrizadas por limites de probabilidade marginal $[\ell_f, u_f]$ derivados das taxas de falha empíricas das ferramentas.
• Regras ($R$): Codificam a lógica de transição de estado (ex: propagação de dados, fusão, desclassificação) como regras intencionais.
• Grafo de Derivação: O traço de execução é traduzido em um Grafo Acíclico Dirigido (DAG) onde os nós representam fatos e as arestas representam aplicações de regras. Os autores provam que qualquer execução de política Datalog pode ser reescrita de tal forma que cada fato derivado dependa de no máximo dois fatos pais (aridade $\le 2$), permitindo que a lógica seja expressa via polinômios multilineares.

2. Formulação de Otimização Exata (Limite Teórico)

Para computar a probabilidade de pior caso de uma violação de política, os autores formulam um programa linear (LP) exato sobre o espaço de medidas de probabilidade conjunta $\mu$.

• Objetivo: Maximizar a probabilidade de atingir um estado inseguro (ex: dados sensíveis chegando a um destinatário externo).
• Restrições:
  • Consistência Estrutural: A medida $\mu$ deve atribuir probabilidade zero a estados que violem a lógica de transição determinística das regras Datalog.
  • Limites Marginais: A medida deve respeitar os limites inferiores e superiores conhecidos dos fatos base iniciais.
  • Robustez Distribuicional: Crucialmente, a formulação não faz suposições sobre a distribuição conjunta (independência, correlação positiva/negativa) a menos que explicitamente especificado. Ela busca a "pior distribuição conjunta" consistente com as marginais.
• Limitação: Este LP exato é exponencialmente dimensionado ($2^{|V_F|}$) e computacionalmente intratável para monitoramento em tempo real.

3. Relaxação de Programação Semidefinida (SDP)

Para alcançar eficiência em tempo de execução, os autores introduzem uma relaxação de Programação Semidefinida (SDP) de tamanho polinomial.

• Rastreamento de Momentos: Em vez de otimizar sobre a distribuição conjunta completa, o SDP rastreia apenas os primeiros e segundos momentos (expectativas e correlações de pares) da distribuição de estado.
• Linearização: Termos quadráticos não convexos decorrentes de restrições de covariância são linearizados usando envelopes de McCormick sobre os intervalos marginais.
• Classes de Correlação: O framework suporta restrições de correlação explícitas (Correlacionados Positivamente, Correlacionados Negativamente, Independentes) entre predicados específicos, permitindo que a otimização refine os limites quando o conhecimento de domínio está disponível.
• Robustez (Soundness): Os autores provam que a relaxação SDP produz um limite superior robusto ($R^*_{SDP} \ge R^*$) sobre o risco real de execução. Isso garante que o monitor nunca bloqueie a menos uma violação, preservando as garantias de segurança mesmo que ocasionalmente bloqueie demais (reduzindo a utilidade).

4. Aplicação em Tempo de Execução

O limite superior computado é comparado contra um limiar de segurança global $\tau$. Se o risco estimado exceder $\tau$, o monitor de referência bloqueia a chamada de ferramenta proposta; caso contrário, permite a execução.

Principais Contribuições

1. Modelo de Verificação Probabilística: Identificação de riscos de segurança em motores determinísticos para ambientes ambíguos e a introdução de um modelo para verificação probabilística que evita a binarização prematura.
2. Formalização de Risco Exato: Modelagem de trajetórias de agentes de múltiplas etapas via grafos de derivação Datalog e formalização do cálculo do risco de violação de política de pior caso como um problema de otimização exata sobre medidas conjuntas.
3. Relaxação SDP Robusta: Introdução de uma relaxação SDP de tamanho polinomial que rastreia momentos de segunda ordem para aproximar o risco de forma eficiente. O artigo prova formalmente que esta relaxação é um limite superior estrito sobre o risco de execução, garantindo a robustez sem suposições de independência.
4. Validação Empírica: Avaliação através de benchmarks de agentes de terminal (Intercode-NL2Bash, ATBench) e tarefas de vulnerabilidade de canal lateral (Praline), demonstrando um melhor equilíbrio segurança-utilidade em comparação com o estado da arte.

Resultados

O framework foi avaliado contra três baselines: Praline (um motor de inferência Datalog de última geração com tratamento de correlação), Monte Carlo (amostragem assumindo independência estrita) e um motor Determinístico com limiares locais.

• Equilíbrio Segurança-Utilidade: A abordagem SDP superou consistentemente os baselines em termos da Área Sob a Curva (AUC) para o equilíbrio segurança-utilidade.
  • vs. Monte Carlo: O Monte Carlo alcançou alta utilidade, mas falhou na segurança (altos falsos negativos) porque as suposições de independência subestimaram o risco de pior caso, especialmente quando os inputs estavam positivamente correlacionados.
  • vs. Praline: Embora o Praline tenha alcançado segurança perfeita, sofreu com timeouts de solver e limites frouxos em tarefas complexas, levando a excessivos falsos positivos (baixa utilidade). A abordagem SDP manteve a segurança perfeita enquanto alcançou maior utilidade e menor latência em benchmarks de terminal.
  • vs. Determinístico: Motores determinísticos mostraram desempenho ruim em ambas as métricas, frequentemente falhando em bloquear ações inseguras ou bloqueando ações seguras devido à perda de informação por limiarização.
• Latência: A relaxação SDP demonstrou escalabilidade polinomial. Nos benchmarks Intercode e ATBench, o SDP foi significativamente mais rápido (ex: ~221ms vs ~1015ms para o Praline no Intercode). Em tarefas complexas de canal lateral com muitas restrições de correlação, a latência do SDP aumentou, mas permaneceu previsível, evitando as latências de cauda exponenciais e timeouts associados ao raciocínio baseado em SMT exato.
• Sensibilidade à Correlação: Experimentos mostraram que, conforme as correlações de entrada aumentavam, a suposição de independência (Monte Carlo) levava a uma queda acentuada na utilidade (aumento de falsos positivos) porque superestimava o risco em configurações correlacionadas onde o limite real de pior caso era mais estreito. O framework SDP adaptou-se a essas restrições de forma eficaz.

Significância e Alegações

O artigo afirma fornecer uma mudança de paradigma da verificação determinística para a probabilística para agentes de IA. Sua principal significância reside em unir robustez (soundness) (garantias de segurança rigorosas) e tratabilidade (performance em tempo real) na presença de ambiguidade.

• Robustez: Ao utilizar otimização distribuicionalmente robusta, o framework garante que as garantias de segurança se mantenham independentemente de correlações desconhecidas entre predicados, um requisito crítico para implantações de agentes no mundo real onde as falhas de ferramentas podem estar acopladas.
• Praticidade: A relaxação SDP permite a aplicação de políticas de segurança complexas de múltiplas etapas com inputs probabilísticos contínuos sem a intratabilidade computacional da inferência exata ou os riscos de segurança das suposições de independência.
• Fundação: O trabalho estabelece uma base escalável para assegurar agentes autônomos operando em ambientes ambíguos, indo além de defesas heurísticas para a aplicação formal e probabilística.

Os autores reconhecem limitações, especificamente que os limites de risco podem degradar (convergir para 1.0) em horizontes de execução muito longos com altos graus de fusão de fatos, e que a abordagem depende de semânticas de ferramentas pré-definidas, o que pode ser desafiador para scripts arbitrários gerados por agentes. No entanto, o framework é apresentado como um passo significativo em direção à segurança de agentes que seja rigorosa e escalável.