🤖 AI

Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries

Este artigo apresenta uma semântica algébrica mecanizada para execução governada, formalizada em 32 módulos Rocq utilizando árvores de interação e coindução, que estabelece uma categoria monoidal simétrica onde a governança é axiomatizada, composicional e coterminante com a expressibilidade, garantindo que todos os programas construtíveis sejam governados enquanto preservam a completude de Turing e excluem entrada/saída não mediada.

Autores originais: Alan L. McCann

Publicado 2026-05-06

📖 5 min de leitura🧠 Leitura aprofundada

CC0 1.0

Autores originais: Alan L. McCann

Artigo original dedicado ao domínio público sob CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está construindo um robô complexo capaz de pensar, falar, lembrar coisas e até sair ao mundo para fazer compras ou ligar para um amigo. Você deseja que esse robô seja incrivelmente inteligente e capaz, mas também precisa garantir que ele nunca faça nada perigoso, ilegal ou contra as regras enquanto trabalha.

Este artigo apresenta uma nova maneira de projetar o "cérebro" e as "regras" para tal robô. Em vez de apenas esperar que o robô se comporte, os autores construíram uma fortaleza matemática ao redor de suas ações. Eles chamam isso de "Execução Governada".

Abaixo está a explicação de sua ideia usando analogias simples:

1. O Problema: O "Faroeste" da IA

Atualmente, tentamos controlar a IA de duas maneiras:

A Abordagem do "Filtro": Treinamos a IA para ser educada ou filtramos suas respostas depois que ela fala. Isso é como tentar parar uma torneira que goteja esfregando o chão. Não impede que a água saia; apenas tenta limpá-la depois.
A Abordagem do "Guardrail" (Barreira): Colocamos cercas ao redor do robô. Mas, muitas vezes, essas cercas são apenas sugestões ou regras brandas que o robô pode pular acidentalmente (ou intencionalmente).

Os autores argumentam que precisamos de um sistema onde as regras estejam codificadas na própria estrutura da capacidade do robô de agir. Se o robô tentar fazer algo sem permissão, ele literalmente não consegue fazê-lo.

2. A Solução: O "Taburete de Três Pernas" (A Álgebra)

Os autores criaram um framework matemático chamado Álgebra de Governança. Pense nisso como um taburete de três pernas que deve estar perfeitamente equilibrado para o sistema funcionar. Se qualquer perna faltar, tudo cai. As três pernas são:

Segurança: O robô nunca deve realizar uma ação sem um "bilhete de permissão" (uma verificação de governança).
Transparência: Se o robô tiver permissão, as regras não devem alterar o que ele faz, apenas que ele verificou primeiro. (Não deve atrasar o robô nem alterar sua resposta, apenas garantir que seja seguro).
Propriedade: As regras devem ser consistentes. Se dois robôs fizerem a mesma coisa, as regras devem tratá-los exatamente da mesma maneira.

3. A "Árvore de Interação": O Processo de Pensamento do Robô

Para provar que isso funciona, eles representam o pensamento do robô como uma enorme Árvore.

Os Ramos: Cada vez que o robô pensa, ele se divide em ramos.
As Folhas: As ações finais (como "Ligar para um amigo" ou "Escrever um arquivo").
O Tronco: O caminho que o robô percorre para chegar lá.

Em seu sistema, cada ramo dessa árvore deve passar por um Portão de Segurança (o Operador de Governança) antes de poder crescer. Se um ramo tentar crescer sem passar pelo portão, a árvore simplesmente se recusa a existir.

4. A "Dupla Garantia": O Crachá e o Guarda de Segurança

O artigo introduz um sistema de segurança inteligente em duas partes:

O Crachá (Capacidades): Antes mesmo do robô começar, ele recebe um crachá que lista exatamente o que ele tem permissão para fazer (ex: "Pode ler arquivos", "Não pode deletar arquivos"). Esta é uma lista estática.
O Guarda de Segurança (Governança): À medida que o robô se move, um Guarda de Segurança verifica cada passo. Mesmo que o robô tenha um crachá, o Guarda o impede se a ação específica parecer suspeita naquele momento.

O artigo prova que ambos devem acontecer ao mesmo tempo. Você não pode ter apenas o crachá (porque o robô pode ficar confuso) e não pode ter apenas o guarda (porque o guarda pode deixar algo passar). Eles trabalham juntos para garantir que cada ação seja tanto autorizada quanto verificada.

5. A "Fronteira Coterminante": A Correspondência Perfeita

Esta é a parte mais emocionante do artigo. Os autores provam um teorema de "Correspondência Perfeita".

A Alegação: Em seu sistema, tudo o que o robô é capaz de construir é automaticamente seguro.
A Analogia: Imagine uma fábrica de brinquedos onde os únicos brinquedos que você pode construir são aqueles que vêm com um certificado de segurança. Você não pode acidentalmente construir um brinquedo inseguro. Se não for seguro, a máquina da fábrica nem sequer permitirá que você comece a construí-lo.
O Resultado: A zona "segura" e a zona "possível" têm exatamente o mesmo tamanho. Não há uma "área cinzenta" onde um robô possa fazer algo arriscado. Se o robô puder expressar um pensamento ou uma ação, é garantido que ele será governado.

6. A Prova da "Caixa Preta"

Os autores não apenas escreveram isso; eles construíram uma máquina de prova digital massiva (usando uma ferramenta chamada Rocq) com mais de 12.000 linhas de código e 454 provas matemáticas.

Eles provaram que, se você seguir suas regras, o robô não pode acidentalmente fazer algo ruim.
Eles provaram que o robô ainda é inteligente o suficiente para realizar tarefas complexas (é "Turing completo", o que significa que pode resolver qualquer problema que um computador possa).
Eles até construíram um "Livro-Registro" (como um diário à prova de adulteração) que registra cada verificação de permissão e ação, para que, se alguém tentar trapacear depois, o diário prove que o fizeram.

Resumo

Este artigo diz: "Construímos uma gaiola matemática para as ações da IA. Dentro dessa gaiola, a IA é livre para fazer o que quiser, mas é fisicamente impossível que ela faça algo inseguro. As regras não são apenas sugestões; são as leis da física para este sistema específico."

Eles provaram isso matematicamente, testaram com milhões de cenários aleatórios e mostraram que a versão "segura" da IA funciona tão rápido quanto a versão "insegura". É uma maneira de tornar a IA poderosa sem torná-la perigosa.

Resumo Técnico: Semântica Algébrica da Execução Governada

Declaração do Problema

Os sistemas atuais de fluxo de trabalho de IA, que compõem chamadas de modelos de linguagem com recuperação de dados, execução de código e acesso a APIs externas, carecem de um quadro formal para execução governada. As abordagens de governança existentes dividem-se em duas categorias:

Abordagens comportamentais (por exemplo, RLHF, IA Constitucional, guardrails) que filtram ou treinam as saídas do modelo, mas falham em abordar se os efeitos estruturais do sistema (chamadas de API, gravações de arquivo) passam por uma fronteira de governança.
Abordagens estruturais que impõem invariantes na camada de execução, mas frequentemente carecem de provas verificadas por máquina ou falham em abordar a composição. Elas tipicamente verificam programas individuais em vez de provar que a governança é fechada sob os operadores de composição do sistema.

O desafio central é estabelecer uma semântica onde a governança não seja meramente um filtro externo, mas uma propriedade intrínseca e composicional do próprio modelo de execução, garantindo que o conjunto de programas expressíveis coincida com o conjunto de programas governados.

Metodologia

O artigo desenvolve uma semântica algébrica para execução governada, mecanizada em 32 módulos Rocq (aproximadamente 12.000 linhas de código, 454 teoremas, 0 lemas admitidos). O quadro de trabalho baseia-se em três pilares técnicos principais:

Árvores de Interação (ITrees): Os programas são representados como árvores coindutivas com três tipos de nós: Ret (valores puros), Tau (passos silenciosos) e Vis (eventos visíveis). O sistema utiliza o tipo DirectiveE para modelar 14 capacidades externas distintas (por exemplo, chamadas de LLM, solicitações HTTP, operações de arquivo).
Álgebra de Governança: A governança é axiomatizada como um registro paramétrico (GovernanceAlgebra) definido por três axiomas:
- Segurança: O operador de governança G garante que os programas interpretados satisfaçam um predicado de segurança coindutivo (gov safe).
- Transparência: Sob condições permissivas (todas as verificações passam), a interpretação governada é observacionalmente equivalente à interpretação não governada.
- Propriedade: Manipuladores equivalentes produzem manipuladores governados equivalentes.
Categorias Monoidais e Efeitos Algébricos: O quadro de trabalho estende a categoria de programas (Mashin) com uma estrutura monoidal simétrica. Ele restringe o sistema de efeitos algébricos de modo que apenas manipuladores que carregam um certificado de segurança verificado por máquina (GovernedHandler) possam ser construídos no fragmento seguro.

A formalização utiliza coindução parametrizada (via a biblioteca paco) para provar propriedades como gov safe e within caps (limites de capacidade). O sistema é extraído para OCaml e integrado como uma Função Implementada Nativa (NIF) no tempo de execução BEAM, com testes baseados em propriedades (mais de 70.000 entradas aleatórias) verificando a equivalência comportamental entre a especificação e o tempo de execução.

Principais Contribuições

1. Álgebra de Governança Paramétrica e Estrutura Monoidal

O artigo define um registro GovernanceAlgebra. A partir dos três axiomas, deriva convergência, fechamento composicional e preservação de objetivos para qualquer sistema que satisfaça esses axiomas.

Estrutura Monoidal: A categoria Mashin é provada como admitindo uma estrutura monoidal simétrica com coerência de pentágono, triângulo e hexágono verificada.
Preservação da Governança: Crucialmente, toda composição tensorial (composição independente paralela/sequencial) preserva a governança. As provas são computacionais e não coindutivas, pois os morfismos estruturais são puros.

2. Efeitos Algébricos Governados

Diferentemente dos sistemas padrão de efeitos algébricos onde qualquer manipulador é válido, este quadro de trabalho restringe a álgebra de manipuladores.

GovernedHandlers: Apenas manipuladores agrupados com uma prova de que sua interpretação satisfaz gov safe podem habitar o tipo GovernedHandler.
Sem Efeitos Ambientais: Um teorema prova que programas no conjunto de capacidades vazio emitem apenas diretivas de observabilidade. Eles não podem realizar chamadas de LLM, solicitações HTTP ou outros efeitos, a menos que explicitamente autorizados pelo conjunto de capacidades.

3. Composição Indexada por Capacidade e Garantia Dual

Os programas são agrupados com limites de capacidade verificados por máquina (CapMorphisms) validados por um reticulado de confiança.

Composição: Os operadores de composição sequencial, tensorial e de ramo preservam os limites de capacidade.
Garantia Dual: Um teorema central estabelece que, para qualquer programa, os limites de capacidade (o que o programa pode fazer) e a segurança de governança (o que o programa tem permissão para fazer) são válidos simultaneamente. As capacidades estáticas limitam os efeitos potenciais, enquanto a governança dinâmica garante que cada efeito passe por uma verificação antes da execução.

4. A Fronteira Coterminante

O resultado culminante do artigo define a relação entre expressibilidade e governança dentro do modelo formal:

Expressível (E): Programas construíveis a partir de quatro morfismos primitivos (code, reason, memory, call).
Governado (G): Programas onde a interpretação através de G satisfaz gov safe.
Resultado: $E = G$ . Todo programa expressível é governado sob interpretação, e todo programa governado é a imagem de um programa expressível.
Implicações: A completude de Turing é preservada dentro da governança. A E/S não mediada é estruturalmente excluída do fragmento governado. A negação da governança é modelada como divergência coindutiva segura (não-terminação), garantindo que nenhum resultado inseguro seja jamais produzido.

Resultados e Verificação

Verificação Formal: Todo o quadro de trabalho é mecanizado em Rocq com zero lemas admitidos.
Extração de Tempo de Execução: O código OCaml extraído executa como uma NIF no tempo de execução BEAM.
Testes: Testes baseados em propriedades com mais de 70.000 entradas aleatórias mostraram zero discordâncias entre a especificação Rocq, a NIF extraída e o interpretador Elixir.
Desempenho: O caminho de execução governada não adiciona sobrecarga mensurável (mediana de 0,23 ms vs. 0,24 ms para execução não governada).
Semântica de Rastros: O quadro de trabalho deriva propriedades ao nível de rastros, provando que a execução governada produz rastros "bem governados" onde cada evento de E/S é precedido por uma verificação de governança aprovada. Esses rastros mapeiam para um livro-razão à prova de adulteração via encadeamento de hash.

Significado e Alegações

O artigo alega fornecer o primeiro quadro mecanizado que combina interpretação restrita por governança, efeitos algébricos limitados por capacidade e um teorema de expressibilidade/governança coterminante sobre um modelo de execução baseado em árvores de interação.

Governança Estrutural vs. Conteúdo: O trabalho distingue-se das abordagens comportamentais (que filtram saídas) ao impor governança estrutural (mediando efeitos). O Teorema 3.3 estabelece que a governança estrutural fornece garantias que controles orientados a saída não podem replicar dentro deste modelo formal.
Parametricidade: A GovernanceAlgebra é paramétrica; teoremas derivados valem para qualquer sistema que satisfaça os três axiomas, não apenas para a instanciação específica Mashin.
Composicionalidade: O quadro de trabalho prova que a governança é fechada sob todos os operadores de composição do sistema, abordando uma lacuna em trabalhos anteriores que verificavam programas individuais, mas não sua composição.
Limitações: Os autores observam que o produto tensorial é independente-sequencial (não verdadeiramente concorrente), a cadeia de hash depende de um hash injetivo abstrato (requerendo trabalho adicional para hashes criptográficos concretos) e o próprio wrapper NIF não é formalmente verificado. A fronteira coterminante é estabelecida especificamente para o modelo de execução de quatro primitivas.

Em resumo, o artigo argumenta que, ao axiomatizar a governança como uma estrutura algébrica sobre árvores de interação, é possível alcançar um sistema onde a governança é coterminante com a expressibilidade: se um programa pode ser escrito no sistema, é estruturalmente garantido que ele será governado.