Resumo Técnico: Governança Transparente a Efeitos para Arquiteturas de Fluxos de Trabalho de IA

Declaração do Problema

À medida que os sistemas de fluxos de trabalho de IA atuam cada vez mais no mundo — consultando Modelos de Linguagem de Grande Escala (LLMs), gerenciando estado e invocando ferramentas externas —, há uma necessidade crescente de mecanismos de governança para prevenir comportamentos inseguros ou não autorizados. Uma premissa predominante no campo é que a governança inevitavelmente sacrifica a capacidade: acredita-se que restrições destinadas a aumentar a segurança reduzem o espaço de comportamentos que um sistema pode exibir. Este artigo desafia essa premissa ao formalizar uma alternativa arquitetônica onde a governança é imposta na fronteira de efeitos em vez de modificar a computação interna ou processar as saídas posteriormente. A questão semântica central abordada é se a governança altera o que os programas permitidos computam.

Metodologia

Os autores apresentam uma formalização verificada por máquina de arquiteturas de fluxos de trabalho de IA estruturalmente governadas usando Árvores de Interação dentro do assistente de prova Rocq 8.19 (anteriormente Coq). O desenvolvimento consiste em 36 módulos, 12.000 linhas de código e 454 teoremas, com zero lemas admitidos.

Formalismo Central

1. Árvores de Interação (ITrees): Os programas são modelados como árvores coindutivas sobre um tipo de evento $E$, definidos como Ret(v), Tau(t) ou Vis(e, k). Isso permite a representação de programas recursivos e impuros.
2. Tipo de Evento de Diretriz: O sistema define um tipo DirectiveE contendo construtores para capacidades primitivas: morfismos de computação, operações de memória, chamadas de oráculo (LLM), chamadas de ferramentas externas e eventos de observabilidade.
3. Operador de Governança ($G$): A governança é implementada como um envoltório sobre a interpretação de efeitos, seguindo a tradição dos manipuladores de efeitos algébricos. O operador $G(h)$ media toda diretriz emitida por um manipulador base $h$. Ele realiza verificações prévias (confiança, permissão, validação de fase) e instrumentação pós (proveniência, observabilidade). Se uma verificação falhar, a execução diverge via ITree.spin; se passar, a diretriz é delegada ao manipulador subjacente.
4. Predicado de Segurança: A segurança é definida via um predicado coindutivo gov_safe usando coindução parametrizada (paco). Este predicado distingue entre eventos exclusivos de governança (que são sempre permitidos) e eventos reais de E/S (que requerem autorização explícita).

Principais Contribuições e Resultados

O artigo estabelece sete propriedades primárias (P1–P7) provando que a governança e a expressividade computacional são dimensões ortogonais.

1. Transparência Semântica (O Teorema Central)

A contribuição central é um teorema verificado por máquina provando a transparência semântica. Para todas as execuções onde as verificações de governança têm sucesso, a interpretação governada é observacionalmente equivalente (módulo eventos exclusivos de governança) à interpretação não governada.

• Implicação: Programas permitidos computam exatamente a mesma função parcial e produzem os mesmos valores de retorno alcançáveis como o fariam sem governança. A governança restringe a fronteira de efeitos sem alterar a computação interna dos caminhos permitidos.

2. Expressividade Governada (P1 e P2)

Os autores provam que o envoltório de governança não reduz o poder computacional:

• Completude de Turing Governada: O sistema permanece completo de Turing sob governança. Programas de máquina de registradores podem ser traduzidos em árvores de interação governadas sem perda de expressividade.
• Expressividade de Oráculo Governada: A arquitetura suporta extensões de oráculo (consultas LLM) sob governança, mantendo a capacidade de modelar fluxos de trabalho de raciocínio complexos.

3. Fronteira de Decidibilidade (P3)

O artigo formaliza uma fronteira estrita entre o que a governança pode decidir e o que não pode:

• Predicados de Governança: Estes são estruturais, sintáticos, totais e fechados sob composição booleana (E, OU, NÃO). Eles podem decidir propriedades como níveis de confiança e classes de capacidade.
• Propriedades Semânticas: Propriedades de programas, como a parada, permanecem não triviais e indecidíveis pela governança. O artigo prova que a governança não pode decidir a parada, pois dois programas podem compartilhar estruturas de diretrizes idênticas (e, portanto, passar nas verificações de governança) mas diferir no comportamento global de terminação. Isso alinha-se com o Teorema de Rice aplicado à fronteira estrutural.

4. Minimalidade Expressiva (P5)

Os autores provam que o conjunto de capacidades primitivas (computação, memória, raciocínio, chamada externa, observabilidade) é mínimo necessário.

• Hierarquia Estrita: As capacidades formam uma cadeia estrita: código < código + memória < código + memória + raciocínio < código + memória + raciocínio + chamada.
• Necessidade: Remover qualquer capacidade primitiva única reduz estritamente o poder expressivo do sistema. Por exemplo, diretrizes de memória são estruturalmente necessárias para a completude de Turing, e diretrizes de LLMCall são necessárias para extensões de oráculo.

5. Assimetria de Subsumção (P6)

O artigo estabelece uma separação estrita entre governança estrutural e filtragem em nível de conteúdo:

• Estrutura Subsume Conteúdo: A governança estrutural subsume estritamente a filtragem de conteúdo. Ao mediar efeitos na fronteira de interpretação, a governança estrutural impede que eventos de E/S não autorizados ocorram.
• Conteúdo Não Subsume Estrutura: Filtros de conteúdo (por exemplo, reescrita de saída) podem alterar valores, mas não podem impedir a ocorrência de um passo de efeito não autorizado. Portanto, a filtragem de conteúdo sozinha não implica segurança de efeitos.

6. Preservação de Objetivos (P4)

Em todas as execuções onde a governança permite, o sistema preserva os objetivos do programa. Se um programa é projetado para alcançar um valor de retorno específico $v$, e as verificações de governança passam, a execução governada alcançará $v$.

7. Segurança via Negação (Vitalidade vs. Segurança)

Quando uma verificação de governança falha, o sistema troca vitalidade por segurança. A execução diverge (spin) em vez de produzir um resultado incorreto. O sistema garante que nenhum efeito não autorizado ocorra jamais e que nenhum valor de retorno "inseguro" seja jamais produzido.

Significado e Escopo

O artigo afirma demonstrar que governança e expressividade computacional são ortogonais. A governança pode ser imposta para restringir a fronteira de efeitos de programas sem reduzir sua expressividade computacional interna ou alterar sua semântica em trajetórias permitidas.

• Fronteira de Confiança: As garantias valem em relação a uma Base de Computação Confiável (TCB) consistindo no kernel Rocq, na biblioteca de Árvores de Interação e na implementação em tempo de execução do operador $G$. O artigo traça um paralelo com compiladores verificados (CompCert) e kernels de SO (seL4), observando que a lacuna entre o modelo formal e o tempo de execução implantado é preenchida por testes (validados contra mais de 70.000 sequências geradas).
• Limitações: O teorema de transparência aplica-se apenas a execuções permitidas; execuções negadas divergem. O modelo abstrai o esgotamento de recursos, o agendamento e comportamentos probabilísticos de modelos. Os teoremas aplicam-se à arquitetura abstrata e ao interpretador, não a garantias ponta a ponta em binários compilados.

Este trabalho estende desenvolvimentos mecanizados anteriores (McCann [2026b, 2026e]) ao adicionar transparência semântica, minimalidade expressiva e uma fronteira de decidibilidade formal, fornecendo uma base rigorosa para "governança transparente a efeitos" em sistemas de IA.