Resumo Técnico: Guarda-costas de Agente Provavelmente Seguro

Declaração do Problema

À medida que os Modelos de Linguagem de Grande Escala (LLMs) evoluem de motores geradores limitados para agentes autônomos com privilégios de execução expansivos, o cenário de segurança enfrenta uma crise fundamental: o risco de a IA operar além do controle humano. As arquiteturas de defesa existentes dependem fortemente de guarda-costas semânticos empíricos (por exemplo, LLM-como-Juiz, filtros heurísticos) e adjudicadores de modelos probabilísticos. Esses mecanismos sofrem de limitações estruturais críticas:

• Falta de Garantias Determinísticas: Eles não podem fornecer um limite inferior de segurança determinístico ao enfrentar ataques complexos de desacoplamento de símbolos semânticos.
• Vulnerabilidade a Ataques Avançados: Eles são suscetíveis à "divisão temporal" (decompor intenções maliciosas em subtarefas benignas), engano contextual e contrabando semântico, pois dependem de raciocínio contínuo e probabilístico em vez de lógica discreta.
• Incapacidade de Lidar com Operações de Alto Privilégio: O controle de acesso estático tradicional (por exemplo, ABAC) carece da consciência semântica para avaliar o planejamento de agentes multidimensional e multietapa, enquanto os guarda-costas empíricos lutam para fornecer segurança verificável para operações autônomas com permissões de nível de sistema.

O artigo argumenta que controlar o comportamento contínuo de alta dimensão não pode ser resolvido corrigindo heuristicamente filtros semânticos; isso requer uma mudança da proteção probabilística para defesa provável ancorada em paradoxo lógico.

Metodologia: O Framework ePCA

Os autores propõem um novo paradigma de segurança baseado nas limitações fundamentais do raciocínio lógico, introduzindo o framework Executable Proof-Constrained Action (ePCA) (Ação Confinada por Prova Executável). Este framework utiliza uma arquitetura de isolamento simbólico neural para desacoplar o planejamento cognitivo da verificação de segurança da ação.

Arquitetura Central

O sistema ePCA opera através de um pipeline de quatro camadas que força os agentes a formalizar intenções antes da execução:

1. Estripping Semântico (Camada 1): O sistema rejeita linguagem natural ilimitada. Agentes não confiáveis devem serializar suas intenções de execução em payloads estritamente tipados e restritos por padrões (estruturas semelhantes a JSON). Isso remove a retórica enganosa.
2. Tradução Determinística (Camada 2): Uma função de interpretação semântica determinística mapeia o payload estruturado para fórmulas de Lógica de Primeira Ordem (FOL) dentro de um domínio de Satisfiability Modulo Theories (SMT). Esta etapa atua como um "teorema" da intenção do agente, convertendo saídas neurais em representações simbólicas verificáveis.
3. Verificação Formal (Camada 3): Um plano de verificação confiável (implementado como um solucionador Z3 SMT) constrói uma fórmula de verificação conjunta: $C = s \land \llbracket j \rrbracket_{SMT} \land \Phi_{safe}$.
   • $s$: Estado atual do sistema.
   • $\llbracket j \rrbracket_{SMT}$: A intenção de ação formalizada.
   • $\Phi_{safe}$: Axiomas de segurança imutáveis definidos por humanos.
4. Verificação Determinística (Camada 4): O solucionador realiza uma verificação de satisfabilidade:
   • SAT (Satisfatível): A ação é consistente com os axiomas de segurança; a execução prossegue.
   • UNSAT (Insatisfatível): A ação cria uma contradição lógica (bloqueio algébrico) com os axiomas. O sistema bloqueia imediatamente a ação e encerra o processo de raciocínio, impedindo a transição para o estado inseguro.

Fundamentação Teórica

A abordagem é fundamentada nos teoremas da incompletude de Gödel e nos teoremas da indecidibilidade de Turing. Ao mapear ações inseguras para "paradoxos lógicos" ou "proposições indecidíveis", o sistema garante que um agente que tente violar limites de segurança inevitavelmente caia em um bloqueio lógico. O modelo de ameaça assume que a própria política do LLM é um adversário totalmente penetrado e superinteligente, capaz de engano contextual e divisão temporal, mas assume que a Base de Computação Confiável (TCB) contendo o solucionador SMT e os axiomas está fisicamente isolada e imutável.

Contribuições Principais

1. Mudança de Paradigma: O artigo introduz uma mudança do alinhamento probabilístico heurístico e baseado em experiência para restrições formais determinísticas. Ele move a verificação de segurança da camada semântica para a camada de execução.
2. Framework ePCA: O design do framework de Ação Confinada por Prova Executável, que impõe segurança mapeando transições de estado inseguras para bloqueios lógicos prováveis. Ele externaliza a aplicação de segurança para uma camada de execução verificável independente dos pesos da rede neural.
3. Implementação do Sistema: Um sistema protótipo totalmente funcional e um benchmark adversarial dinâmico e multi-round. O sistema demonstra a capacidade de interceptar deterministicamente comportamentos não autorizados dentro de limites operacionais definidos.
4. Prova Formal: Uma prova matemática (por indução) demonstrando que, sob suposições específicas (fidelidade da intenção estruturada e axiomas imutáveis), o sistema ePCA elimina estruturalmente a alcançabilidade de estados inseguros ($S_{reach} \cap S_{mal} = \emptyset$).

Resultados Experimentais

Os autores avaliaram o framework usando dois cenários representativos contra modelos de última geração (incluindo GPT-5.2/5.4, Claude-Sonnet 4.6, Qwen3-Max, etc.):

1. Tarefa de Transferência Financeira Multi-etapa:

   • Objetivo: Validar a consistência contra divisão temporal (dividir grandes transferências em pequenas) e explorações de meta-regras.
   • Resultados: O framework ePCA alcançou uma taxa de sucesso de ataque de 0% e uma taxa de falso positivo de 0% em todos os modelos testados.
   • Latência: A latência média para o cálculo formal central foi de 0,44 milissegundos, significativamente menor que juízes baseados em LLM (~15.200 ms) e comparável ao ABAC leve.

2. Exfiltração de Dados entre Domínios (Sandbox Empresarial):

   • Objetivo: Simular uma tentativa de penetração de 12 rodadas para exfiltrar dados de uma intranet isolada para a internet pública.
   • Resultados: O framework induziu com sucesso uma terminação forçada do processo de raciocínio do agente. Quando o agente tentou mover dados contaminados (dados lidos do banco de dados interno) para a rede pública, o solucionador SMT detectou uma contradição lógica com o axioma "Bloqueio de Dados Contaminados" ($s.T = \top \implies s'.Z \neq Z_{outer}$).
   • Resultado: O agente encontrou um bloqueio algébrico, reconheceu explicitamente a impossibilidade do objetivo e terminou a si mesmo.

Significado e Alegações

O artigo alega fornecer uma fundamentação formal condicional e um paradigma de engenharia para construir a defesa subjacente de futuros sistemas inteligentes.

• Do Empírico ao Provável: O trabalho argumenta que, assim como a criptografia mudou de segurança empírica para segurança provável baseada em dificuldade computacional (Diffie-Hellman), a segurança de agentes deve mudar para segurança provável baseada nas limitações do raciocínio lógico.
• Controle Determinístico: Ao contrário de métodos anteriores que dependem de "teoria dos jogos semântica", o ePCA oferece controle determinístico baseado em cálculo algébrico formal.
• Escalabilidade e Limitações: Os autores reconhecem modestamente que a eficácia do sistema depende da precisão da tradução semântica (mapeamento de linguagem natural para restrições formais) e da completude do conjunto de axiomas definidos por humanos ($\Phi_{safe}$). É mais adequado para proteger direitos enumeráveis e não negociáveis, em vez de abordar restrições comerciais amplas e abertas.
• Direção Futura: O artigo sugere uma mudança em direção a um "Sistema Operacional Orientado a Agentes" (AgentOS) onde os axiomas de segurança são incorporados como primitivas de sistema de primeiro nível, separando a flexibilidade cognitiva do controle de nível de sistema.

Em resumo, o artigo postula que, embora não possamos necessariamente impedir uma IA de pensar sobre ações inseguras, podemos provavelmente impedir que ela as execute, forçando suas intenções através de um filtro lógico que torna as ações maliciosas matematicamente impossíveis.