From categorized neural architectures to subexponential proof theory

Resumo Técnico: Da Arquitetura Neural Categorizada à Teoria da Prova Subexponencial

1. Problema e Motivação

O artigo aborda a questão fundamental de como extrair uma disciplina lógica rigorosa diretamente de uma classe de arquiteturas neurais, sem partir de uma lógica pré-existente.

• Contexto: O uso da teoria das categorias em machine learning (aprendizado composicional, backpropagation) e a lógica categórica (estudo de doutrinas e linguagens internas) são campos maduros. No entanto, a conexão direta entre a estrutura de recursos de uma arquitetura neural e um sistema de prova formal ainda carece de fundamentação teórica.
• O Desafio: Arquiteturas neurais modernas possuem comportamentos diferenciados de recursos: algumas informações são reutilizáveis (memória persistente), outras descartáveis, outras lineares (uso único) e outras sujeitas a coerção entre zonas. A pergunta central é: pode-se começar com uma família de arquiteturas neurais organizadas, passar para uma descrição categórica de seu comportamento de recursos e, em seguida, extrair uma lógica apropriada dessa estrutura?
• Objetivo: Demonstrar que é possível construir uma lógica de prova (especificamente um cálculo de sequentes tensorial com subexponenciais) cujas regras estruturais (enfraquecimento e contração) são determinadas estritamente pelas permissões de recursos da arquitetura, e não impostas externamente.

2. Metodologia

O autor propõe um pipeline de construção em quatro etapas, onde a lógica é "lida" a partir dos dados categóricos:
$$\text{Família de Arquiteturas} \xrightarrow{\text{Categorização}} \text{Arquitetura Categorizada} \xrightarrow{\text{Extração}} \text{Assinatura Subexponencial} \xrightarrow{\text{Definição}} \text{Teoria da Prova}$$

Etapas Principais:

1. Definição da Categoria Arquitetural ($Arch_Z$):

   • Introduz-se uma categoria onde os objetos são contextos de recursos tipados (listas finitas de pares $(z, A)$, onde $z$ é um rótulo de zona e $A$ é um objeto de uma categoria base $Ctx$ com produtos finitos).
   • Os morfismos são blocos computacionais parametrizados $(P, \phi)$, onde $P$ é um objeto de parâmetros e $\phi$ é um morfismo que consome o contexto de entrada e produz o de saída.
   • Define-se uma relação de equivalência para blocos que diferem apenas por reparametrização isomórfica.
   • Resultado: Prova-se que $Arch_Z$ é uma categoria monoidal simétrica, permitindo composição sequencial e paralela de blocos.

2. Disciplina de Zonas Coerente ($Lic$):

   • Para capturar a sensibilidade a recursos, define-se uma "disciplina de zona coerente" sobre $Arch_Z$.
   • Esta disciplina especifica quais transformações estruturais são "licenciadas" pela arquitetura:
     • Coerções de zona: Permissões para mover dados entre zonas refinadas ($z \preceq z'$).
     • Descarte licenciado ($\omega$): Permissão para descartar dados em certas zonas (enfraquecimento).
     • Diagonais licenciadas ($\delta$): Permissão para duplicar dados em certas zonas (contração).
   • Essas permissões devem ser coerentes com a estrutura monoidal e as morfismos da categoria.

3. Extração da Assinatura Subexponencial ($\Sigma_{Lic}$):

   • A partir da disciplina $Lic$, extrai-se uma assinatura subexponencial $\Sigma_{Lic} = (Z, \preceq, W, C)$, onde:
     • $Z$ é o conjunto de zonas.
     • $\preceq$ é a ordem prévia de refinamento.
     • $W$ (enfraquecimento) e $C$ (contração) são subconjuntos de zonas que correspondem exatamente às zonas onde a disciplina permite descarte e duplicação, respectivamente.
   • Teorema Chave: A reconstrução é fiel; as classes extraídas coincidem exatamente com as classes designadas na disciplina original.

4. Definição da Teoria da Prova ($TZ_{\Sigma}$):

   • Define-se um cálculo de sequentes tensorial baseado na assinatura extraída.
   • O sistema inclui regras para o produto tensorial ($\otimes$), unidade ($I$) e regras estruturais de enfraquecimento ($W_z$) e contração ($C_z$) indexadas pelas zonas.
   • Restrição: O sistema é propositalmente modesto, focando no fragmento tensorial, pois a implicação linear exigiria estrutura categórica adicional (como adjunções linear-não-linear) não presente nesta fase.

3. Contribuições Principais

O artigo apresenta cinco contribuições teóricas principais:

1. Definição da Categoria $Arch_Z$: Formalização de blocos de arquitetura parametrizados como uma categoria monoidal simétrica.
2. Conceito de Disciplina de Zona Coerente: Introdução de dados estruturais que refinam a categoria para capturar comportamentos de recursos diferenciados (descarte, duplicação, coerção).
3. Teorema de Extração: Demonstração de que uma assinatura subexponencial pode ser canonicamente reconstruída a partir da disciplina categórica, garantindo que a lógica derivada reflete fielmente a arquitetura.
4. Eliminação de Corte (Cut Elimination): Prova de que o cálculo de sequentes extraído admite eliminação de corte, garantindo consistência e propriedades de normalização.
5. Teorema de Corretude (Soundness): Prova de que toda derivação no sistema de prova extraído é interpretada por um morfismo na categoria arquitetural original, construído a partir dos blocos licenciados e das famílias estruturais (descarte/diagonal) específicas.

4. Resultados Técnicos

• Estrutura Monoidal: A categoria de arquiteturas é provada ser monoidal simétrica, permitindo a composição natural de redes neurais.
• Correspondência Estrutural: O teorema 2.18 estabelece que as zonas de enfraquecimento e contração na lógica extraída são exatamente as zonas onde a arquitetura permite descarte e duplicação. Não há "ruído" ou regras lógicas adicionais não justificadas pela arquitetura.
• Eliminação de Corte no Fragmento Tensorial: O artigo prova que, embora o sistema seja um fragmento da lógica linear intuicionista com subexponenciais, a eliminação de corte é válida e preserva o fragmento tensorial (Lema 3.6).
• Corretude Semântica: O Teorema 4.8 garante que a lógica não é apenas sintática, mas possui uma semântica concreta na própria arquitetura:
  • A regra de enfraquecimento $W_z$ é interpretada pelo morfismo de descarte licenciado $\omega_z$.
  • A regra de contração $C_z$ é interpretada pelo morfismo de diagonal licenciado $\delta_z$.
  • A ausência de uma regra lógica corresponde à ausência de um morfismo estrutural licenciado na arquitetura.

5. Significado e Impacto

• Mudança de Paradigma: O trabalho inverte a direção tradicional de "Lógica $\to$ Semântica". Em vez de impor uma lógica a uma rede neural, ele extrai a lógica da disciplina de recursos da arquitetura. A lógica é uma consequência da organização arquitetural.
• Fundamentação para Arquiteturas de Recursos: Oferece uma base matemática rigorosa para entender por que certas arquiteturas (como Transformers com mecanismos de atenção ou memórias externas) comportam-se de maneira diferente em termos de reutilização de dados.
• Exemplo Concreto: O artigo ilustra o processo com uma arquitetura neural de dois blocos que utiliza memória persistente ($p$), contexto recuperado ($r$) e observação atual ($\ell$).
  • A memória persistente permite descarte e cópia (zona $p \in W, C$).
  • O contexto recuperado permite cópia, mas não descarte silencioso (zona $r \in C, \notin W$).
  • A observação atual é estritamente linear (zona $\ell \notin W, C$).
  • A lógica extraída reflete exatamente essas restrições, validando o pipeline proposto.
• Contribuição para a Pesquisa: O artigo posiciona-se como um primeiro passo "carregado de teoremas" no programa Arquitetura $\to$ Categoria $\to$ Lógica, sugerindo extensões futuras para incluir implicação linear e adjunções, mas estabelecendo que o fragmento estrutural já é suficientemente rico para ser formalizado.

Em suma, o artigo demonstra que a "disciplina lógica" de uma rede neural não é uma camada externa de especificação, mas uma propriedade intrínseca que pode ser lida e formalizada a partir da maneira como a arquitetura gerencia, copia e descarta seus recursos de memória e contexto.