Resumo Técnico: Metaprogramação Governada para Sistemas Inteligentes

1. Declaração do Problema

Sistemas de IA modernos, incluindo Modelos de Linguagem de Grande Porte (LLMs) e agentes autônomos, sintetizam cada vez mais estruturas executáveis em tempo de execução. Esses sistemas geram fluxos de trabalho, planos de chamada de ferramentas e código auto-modificável. Em linguagens homoicônicas clássicas (por exemplo, Lisp) e linguagens em estágios (por exemplo, MetaOCaml), a transição de uma representação de código (dados) para um programa executável é tratada por primitivas como eval ou run. Essas transições são tradicionalmente irrestritas: qualquer representação válida pode tornar-se imediatamente código em execução.

No contexto de sistemas inteligentes governados — que exigem limites explícitos de efeitos, controle de capacidades e auditabilidade —, essa transição irrestrita cria uma vulnerabilidade crítica. Se um sistema puder gerar um novo programa que contorne as restrições de governança do original, todo o modelo de governança fica comprometido. O artigo identifica isso como uma "saída de emergência de metaprogramação": um sistema governado no nível de execução, mas não governado no nível de geração de código, é fundamentalmente inseguro.

2. Metodologia Central: Reclassificação de eval

A contribuição metodológica central do artigo é a reclassificação de eval (ou a transição de forma para execução) de uma primitiva de linguagem para um efeito governado.

Os autores propõem um framework chamado Metaprogramação Governada, construído sobre os seguintes pilares:

• Formas de Máquina: Representações de programas são tratadas como valores de primeira classe (mapas de dados estruturados) em vez de strings opacas ou bytecode.
• Manipulação Pura de Formas: Todas as operações sobre essas formas (inspeção, transformação, composição, diffing) são classificadas como computação pura. Elas não emitem diretivas e não possuem capacidade de realizar I/O ou invocar modelos.
• Materialização como Alocação de Autoridade: A transição de uma forma de máquina para uma máquina executável é definida como materialização. Isso não é meramente computação; é a alocação de autoridade executável (o poder de invocar modelos, realizar I/O e consumir recursos). Consequentemente, a materialização é classificada como um efeito governado.
• Inspeção Estrutural: Antes que a materialização seja permitida, um sistema de governança realiza uma inspeção estrutural decidível da forma. Essa inspeção analisa requisitos de capacidade, conformidade com políticas, autorização de modelos e estimativas de recursos.

3. Semântica Operacional Formal

O artigo formaliza o sistema usando dois julgamentos distintos para impor a fronteira entre computação pura e execução governada:

1. Avaliação Pura de Formas ($\Gamma \vdash pure\ e \Downarrow v$):

   • Opera sobre valores de forma.
   • Emite zero diretivas ($Dir(e) = \emptyset$).
   • Inclui construção de citação, avaliação de interpolação, navegação e transformação.
   • Garante que nenhuma sequência de operações puras possa produzir uma máquina autorizada.

2. Materialização Governada ($\Gamma; \Pi; \sigma \vdash materialize(v_f) \rightsquigarrow \langle Machine, d \rangle$):

   • Recebe uma forma, um contexto de política ($\Pi$) e um conjunto de capacidades ($\sigma$).
   • Requer um registro de decisão de governança ($d$) para cada resultado (aprovação ou rejeição).
   • Emite exatamente uma diretiva governada.
   • O sistema de governança inspeciona a estrutura da forma para verificar:
     • Contenção de capacidades ($CapSet(f) \subseteq \Pi.allowed\ caps$).
     • Autorização de modelos.
     • Conformidade estrutural com políticas.
     • Limites de recursos.

4. Contribuições Principais

O artigo apresenta cinco contribuições primárias:

1. Reclassificação de eval: Uma caracterização precisa da materialização como alocação de autoridade, movendo-a de uma primitiva para um efeito governado.
2. Formas de Máquina: Um tipo de dado concreto para representação estruturada de programas com construtos para quote, splice e reflection.
3. Semântica Formal: Uma definição do sistema usando dois julgamentos (avaliação pura e materialização governada) que separa estritamente a manipulação de dados da execução.
4. Propriedades Verificadas por Máquina: Três propriedades centrais são formalmente verificadas em Rocq:
   • Pureza da Manipulação de Formas: Operações de forma não emitem diretivas.
   • O Teorema de Não Contorno: Nenhuma sequência de operações puras pode causar execução diretamente.
   • Preservação de Fronteiras: Adicionar capacidades de metaprogramação não divide as fronteiras de expressividade e governança (elas permanecem coincidentes).
5. Auto-modificação Governada: Um mecanismo concreto que permite que máquinas proponham mudanças estruturais a si mesmas por meio de um livro-razão de evolução, sujeito à mesma inspeção de governança que a geração de código externa.

5. Implementação e Resultados

O design é implementado em MashinTalk, uma linguagem específica de domínio para fluxos de trabalho de IA que compila para bytecode BEAM (máquina virtual Erlang).

• Arquitetura do Sistema: A implementação consiste em três módulos: Form (construção e manipulação), FormInspector (verificações de governança) e FormMaterializer (compilação governada).
• Verificação: As propriedades centrais são mecanizadas em Rocq (anteriormente Coq) com 26 teoremas e 662 linhas de código, apresentando zero lemas admitidos. Esses teoremas integram-se a uma formalização existente de 454 teoremas em 36 módulos.
• Testes: Um conjunto de testes de 51 testes unitários valida a correção funcional e as propriedades de governança. Todos os testes passam.
• Desempenho: Em processadores Apple série M, a construção de formas leva <1 µs, e a inspeção estrutural leva <100 µs para máquinas típicas. A sobrecarga é negligenciável em comparação com a compilação para bytecode BEAM.

6. Significado e Alegações

O artigo afirma fechar a "saída de emergência de metaprogramação" em sistemas inteligentes governados. Sem esse mecanismo, um sistema governado no nível de execução permanece vulnerável porque não pode governar a geração de novas estruturas executáveis.

Os autores argumentam que, em sistemas de IA sintetizando sua própria estrutura executável, a alocação de autoridade executável deve ser:

1. Visível: A transição de dados para código é um evento distinto e observável.
2. Mediada: Deve passar por um interpretador de governança que inspeciona a estrutura.
3. Registrada: As decisões são registradas em um livro-razão apenas de adição (o livro-razão de evolução).

O artigo reconhece explicitamente limitações:

• Teorema de Rice: A inspeção estrutural é decidível, mas não pode raciocinar sobre comportamento semântico. A governança garante mediação, não a correção semântica do programa gerado.
• Escopo: O argumento de preservação de fronteira é arquitetural; uma prova completa de conservatividade relativa a conjuntos de assinatura de efeitos é adiada para trabalhos futuros.
• Aplicabilidade: O design é específico para linguagens com estruturas de limites de efeitos (como MashinTalk); sua aplicabilidade a linguagens de propósito geral é uma questão em aberto.

Em conclusão, o artigo estabelece que eval não é meramente uma função computacional, mas um evento de alocação de autoridade. Ao tratá-lo como um efeito governado, sistemas inteligentes podem sintetizar e modificar com segurança suas próprias estruturas executáveis sem comprometer seus modelos de governança.