Resumo Técnico: Agentes de LLM Provavelmente Auditáveis e Seguros a partir de Ontologias Elaboradas por Humanos

1. Declaração do Problema

Agentes de Grandes Modelos de Linguagem (LLMs) exibem comportamento não determinístico e alucinações, impondo riscos significativos em domínios de missão crítica que exigem auditabilidade linear, como conformidade em saúde e segurança financeira. As abordagens atuais para a segurança de agentes dependem de "grades de proteção" (guardrails) operacionais (ex: troca de harnesses de agentes ou uso de LLMs como juízes), que carecem de garantias semânticas. Especificamente, sistemas multi-agentes frequentemente sofrem de anomalias de "Write Skew" (viés de escrita), onde agentes atuando em fatias locais de estado disjuntas propõem ações independentes que, quando combinadas, violam invariantes globais do sistema (ex: exceder um orçamento ou violar restrições regulatórias). Os frameworks existentes lutam para fornecer uma garantia matemática de que as transições de estado global sempre preservarão esses invariantes, independentemente do comportamento do agente ou de entradas externas adversárias.

2. Metodologia

2.1 Arquitetura Agentic Redux

O artigo introduz o Agentic Redux, uma arquitetura de agente inspirada no padrão de gerenciamento de estado Redux. Ela separa o sistema em três camadas:

1. Sub-agentes: Cada agente opera em uma "fatia" isolada do estado global. Os agentes propõem ações baseadas em sua visão local, podendo utilizar LLMs ou ferramentas. Eles não podem modificar diretamente o estado global nem observar as fatias de outros agentes.
2. Meta-agente: Um adjudicador central com visibilidade total do estado global. Ele recebe propostas de sub-agentes e as avalia contra um conjunto de invariantes declarados (regras que devem ser sempre verdade sobre o estado global).
3. Disciplina de Commit: O meta-agente é a única entidade permitida a alterar o estado global. Ele só realiza o commit de uma transição de estado se o estado resultante preservar todos os invariantes. Se uma proposta violar um invariante, ela é rejeitada ou escalonada.

2.2 Design de Agente Baseado em Ontologia (Ontology-First)

Para aplicar o Agentic Redux a domínios específicos, os autores propõem uma metodologia chamada Ontology-First Agent Design:

1. Ontologização: Um especialista humano constrói uma "ontologia inferior" do domínio do problema usando a Basic Formal Ontology (BFO). Isso define continuantes independentes (ex: Pacientes, Vulnerabilidades), processos e papéis.
2. Derivação de Papéis: Um LLM é incumbido de analisar a ontologia para derivar papéis de agentes. Isso envolve agrupar processos com pegadas de estado (state footprints) sobrepostas e atribuí-los a papéis. O objetivo são papéis granulares que obedeçam ao Princípio do Menor Privilégio (PoLP), garantindo que os agentes vejam apenas o estado necessário para suas tarefas específicas.
3. Derivação de Invariantes: Um LLM extrai invariantes do sistema da ontologia, classificando-os como locais (aplicáveis por uma única fatia de agente) ou transversais (cross-cutting, exigindo a visão global do meta-agente).
4. Construção do Módulo de Domínio: A ontologia e os papéis/invariantes derivados são convertidos em um Módulo de Domínio tipado, que é então executado no kernel Agentic Redux.

2.3 Verificação Formal

O artigo utiliza cálculo lambda tipado para modelar formalmente a arquitetura Agentic Redux. O sistema é definido como um "Functor de Arquitetura" que recebe um Módulo de Domínio como entrada. Os autores provam que, para qualquer execução bem tipada:

• Preservação de Invariantes: Se o estado inicial satisfaz os invariantes, cada estado alcançável em qualquer execução (incluindo aquelas com saídas de LLM não determinísticas ou agendamento adversário) preserva esses invariantes.
• Confinamento de Agente: Agentes são matematicamente restritos a observar e afetar apenas suas fatias de estado atribuídas.
• Auditabilidade Linear: O sistema mantém um registro (ledger) de adição exclusiva (append-only) onde cada decisão (aprovação, rejeição ou escalonamento) é registrada com uma prova do motivo pelo qual a decisão foi tomada.

3. Principais Contribuições

• Arquitetura Agentic Redux: Um novo framework de agentes que fornece uma garantia semântica de segurança ao impor a preservação de invariantes através de um meta-agente centralizado, eliminando efetivamente anomalias de Write Skew.
• Provas Formais: A primeira aplicação de cálculo lambda tipado para provar que execuções de agentes de LLM são semanticamente garantidas de serem corretas (preservadoras de invariantes) e linearmente auditáveis, mesmo quando sub-agentes são bugados, maliciosos ou alucinam.
• Design de Agente Baseado em Ontologia: Uma metodologia para derivar semi-automaticamente frameworks de agentes a partir de ontologias elaboradas por humanos, utilizando LLMs para extração de papéis e código, mantendo a construção crítica da ontologia nas mãos humanas.
• Extensão da Fila de Conselheiro (Counselor Queue): Um mecanismo para lidar com casos de borda onde a intervenção humana é necessária. O sistema permite que um "Conselheiro" humano sobrescreva decisões, mas o sistema rastreia formalmente essas sobrescritas no log de auditoria, distinguindo entre "Commits de Conselheiro Seguros" (que preservam invariantes) e violações de política.
• Estudos de Caso de Grau de Produção: Os autores demonstram a arquitetura em dois domínios distintos:
  1. Conformidade de Faturamento de Saúde (UDT): Garantindo que o faturamento de Testes de Drogas na Urina (Urine Drug Test) adira a regulamentações complexas e dependentes do tempo (ex: níveis de abstinência), onde agentes clínicos e de faturamento independentes poderiam, de outra forma, causar erros de cobertura.
  2. Divulgação de Vulnerabilidade de Segurança: Gerenciando o pipeline de divulgação para vulnerabilidades de software, garantindo a coordenação entre desenvolvimento de patches, aplicação de embargo e atribuição de CVE sem vazar informações sensíveis entre divulgações simultâneas.

4. Resultados

• Garantias Teóricas: O artigo apresenta o Teorema 1 (Preservação de Invariante), provando que execuções do Agentic Redux nunca atingem um estado que viole os invariantes declarados, desde que o estado inicial seja válido. O Teorema 2 (Integridade do Log de Auditoria) prova que o sistema gera um log linear de adição exclusiva de todas as decisões com procedência completa. O Corolário 1 estabelece que execuções de Write Skew são estruturalmente impossíveis sob esta arquitetura.
• Implementação: O código funcional para o kernel Agentic Redux e os dois exemplos de domínio (Conformidade UDT e Divulgação de Vulnerabilidade de Segurança) é fornecido em um repositório de suporte. O código demonstra a auto-derivação de agentes a partir de ontologias BFO.
• Comparação com Padrões Existentes: A arquitetura mostra-se isomórfica ao framework "Risk Agents" usado pela CashApp, sugerindo que o Agentic Redux captura um padrão arquitetônico "natural" para fluxos de trabalho complexos e regulados.

5. Significância e Alegações

O artigo alega que o Agentic Redux desloca o ônus da segurança do monitoramento operacional em tempo de execução para o design arquitetônico. Ao usar propriedades de teoria de tipos, a arquitetura garante que "comportamentos ruins nunca aconteçam" no nível semântico, independentemente da imprevisibilidade dos LLMs atuando como sub-agentes.

Os autores enfatizam que esta abordagem permite que engenheiros construam sistemas onde o "harness" (o mecanismo de segurança) não precisa ser trocado conforme os LLMs evoluem, porque a segurança é garantida pela teoria de tipos da arquitetura, não pelo output do modelo específico. A metodologia de Design de Agente Baseado em Ontologia é apresentada como uma forma escalável de traduzir a expertise de domínio humana em frameworks de agentes provadamente seguros, focando o esforço humano na ontologia (a "verdade") e utilizando LLMs para a derivação mecânica de papéis e código.

O artigo delimita explicitamente suas alegações à segurança (prevenir coisas ruins) e auditabilidade, observando que a vivacidade (liveness - garantir que coisas boas eventualmente aconteçam) e métricas de complexidade são tratadas em trabalhos futuros. Reconhece-se que, embora a arquitetura previna violações de invariantes, ela não impede que o sistema se comporte mal se os próprios invariantes forem mal especificados; portanto, a qualidade da ontologia elaborada pelo humano permanece sendo o fator crítico.