Resumo Técnico: Modelagem da Predição do Próximo Token como Implicação Intuicionista Aninhada à Esquerda

Declaração do Problema

Modelos de IA generativa fundamentais, particularmente os Transformers, baseiam-se na predição de próximo token não supervisionada treinada em conjuntos de dados massivos. Embora eficaz, a arquitetura padrão do Transformer obscurece a estrutura lógica da predição de sequências. Ela trata os tokens como embeddings aditivos misturados via mecanismos de atenção, exigindo codificações posicionais explícitas para capturar a ordem. Esta abordagem oferece uma conexão explicativa limitada com o raciocínio simbólico ou a natureza construtiva da derivação de provas. O artigo propõe uma questão fundamental: a predição do próximo token pode ser entendida como a extensão de uma prova na lógica proposicional intuicionista, e pode essa interpretação gerar uma arquitetura neural viável, sensível à ordem, sem depender de embeddings aditivos ou codificações posicionais explícitas?

Metodologia

Os autores propõem o Arrow Language Model, uma arquitetura neural derivada de uma interpretação de lógica intuicionista da predição de próximo token. A metodologia procede através de derivação lógica simbólica, prova de teoremas e realização neural.

1. Formalismo Lógico: Implicação Aninhada à Esquerda

A ideia central é representar uma sequência de tokens $w_1, \dots, w_n$ não como um conjunto ou uma cadeia aninhada à direita (que é invariante à permutação sob conjunção), mas como uma cadeia de implicações aninhadas à esquerda:
$$L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$$
Na lógica intuicionista, esta estrutura é sensível à ordem; permutar os tokens altera o tipo funcional do antecedente.

• Predição do Próximo Token como Modus Ponens: Predizer o próximo token $w$ dado um prefixo $P$ corresponde à inferência lógica $P \to w$. Se o prefixo é representado como uma cadeia de implicações $I_p$ e a sequência completa como $I_f = (I_p \to w)$, então derivar $w$ é uma instância de modus ponens.
• Correspondência de Curry–Howard: Sob este isomorfismo, proposições são tipos e provas são termos $\lambda$. O prefixo é um termo $\lambda$ parcialmente aplicado, e a predição do próximo token é o fornecimento de um argumento para permitir a aplicação de função subsequente (eliminação de implicação).

2. Prova de Teoremas e Recuperação Simbólica

Os autores utilizam provadores de teoremas especializados baseados em Prolog (implementando o cálculo LJT de Roy Dyckhoff) para validar propriedades destas cadeias de implicação.

• Teoremas: Eles demonstram que cadeias aninhadas à esquerda suportam predições de passo único e de múltiplos passos. Por exemplo, teoremas mostram como um prefixo pode ser "compilado" em operadores de continuação reutilizáveis (ex: transformando $((E \to a) \to b) \to c$ em uma regra para gerar $b$ depois $c$).
• Recuperação de Informação: Um mecanismo de recuperação simbólica é implementado onde sentenças são armazenadas como cadeias de implicação. Consultas (subsequências) atuam como subfórmulas para recuperar complementos exatos do banco de dados, servindo como uma linha de base lógica.

3. Realização Neural: O Modelo Arrow

O artigo deriva uma arquitetura neural recorrente que espelha a estrutura lógica:

• Estado Oculto como Contexto de Prova: O estado oculto $h_t \in \mathbb{R}^d$ representa o contexto de prova acumulado após consumir um prefixo.
• Tokens como Operadores: Em vez de embeddings aditivos, cada token $t$ atua como um operador linear $M_t$ que transforma o estado atual.
• Parametrização de Baixo Rank: Para lidar com grandes vocabulários, o operador é definido como uma atualização de baixo rank:
  $$M_t = I + U \text{diag}(s_t) V^\top$$
  onde $U, V$ são matrizes compartilhadas e $s_t$ é um vetor de porta específico do token derivado de um lookup de embedding.
• Atualização de Estado (Modus Ponens): A recorrência implementa a eliminação de implicação:
  $$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$$
  Esta atualização é inerentemente não-comutativa ($M_a M_b \neq M_b M_a$), codificando a ordem intrinsecamente sem codificações posicionais.
• Treinamento: O modelo é treinado usando a entropia cruzada padrão de próximo token com teacher forcing. A perda é computada de forma streaming para gerenciar a memória em GPUs comuns.

Principais Contribuições

1. Derivação Baseada em Lógica: O artigo estabelece uma correspondência formal entre a profundidade das implicações intuicionistas aninhadas à esquerda e os passos da computação recorrente, fornecendo uma base teoria-da-prova para modelagem de sequências.
2. Arquitetura Arrow: Introduz uma arquitetura neural específica onde os tokens são operadores de transformação de estado em vez de vetores aditivos, deslocando o viés indutivo de "recuperação via atenção" para "transformação via composição".
3. Ponte Simbólico-Neural: O trabalho demonstra um vínculo estreito entre a prova de teoremas simbólicos (recuperação exata via unificação) e a predição neural (recuperação aproximada via pontuações de continuação aprendidas).
4. Análise Teórica de Ordem: Prova que implicações aninhadas à esquerda preservam a ordem naturalmente, enquanto implicações aninhadas à direita (comuns em formulações de atenção padrão sem codificações posicionais) não o fazem.

Resultados Experimentais

Os experimentos focam em validar a capacidade da arquitetura de aprender padrões sensíveis à ordem e sua habilidade de mimetizar a recuperação simbólica, em vez de competir com modelos de linguagem de estado da arte em benchmarks gerais.

• Overfitting/Testes de Sanidade: O modelo foi testado em pequenos conjuntos de dados (textos do Project Gutenberg) sob um regime de overfitting deliberado. O conjunto de treinamento foi aumentado com todos os fragmentos contíguos de sentenças para mimetizar a recuperação de nível lógico de subfórmulas.
• Desempenho: O modelo conseguiu realizar o overfitting aos dados de treinamento, alcançando perda de treinamento próxima de zero em pequenos documentos (ex: O Mágico de Oz, Moby Dick) em minutos em uma única RTX 3090.
• Recuperação vs. Geração:
  • Baseline Simbólico: A recuperação baseada em Prolog alcançou correspondências exatas para consultas contra as cadeias de implicação armazenadas.
  • Mímico Neural: O modelo Arrow, quando consultado com um prefixo, pôde classificar candidatos a complementos de sufixo (derivados do corpus de treinamento) com base em pontuações de continuação aprendidas, mimetizando efetivamente o processo de recuperação lógica.
  • Geração Livre: O modelo pôde gerar continuações fluentes além das correspondências exatas memorizadas, demonstrando que a composição de operadores aprendeu uma estrutura sequencial generalizável.
• Escalabilidade: O throughput de treinamento foi linear em relação ao comprimento da sequência, e o modelo escalou para corpora de extensão de livros (ex: Guerra e Paz) com uso de memória gerenciável devido ao cálculo de perda em streaming.

Significância e Alegações

O artigo afirma oferecer uma fundação baseada em lógica para a predição do próximo token que é distinta da atenção baseada em similaridade e das alternativas de convolução/estado-espaço.

• Ordem Intrínseca: Ao codificar a ordem através da composição de operadores não-comutativos, o modelo Arrow elimina a necessidade de codificações posicionais explícitas, alinhando a arquitetura mais de perto com a natureza construtiva da extensão de provas.
• Explicabilidade: A arquitetura fornece um mapeamento direto para a lógica intuicionista, onde as atualizações de estado correspondem a passos de prova (modus ponens) e os estados ocultos correspondem a contextos de prova. Isso oferece um caminho potencial para modelos neurais mais interpretáveis.
• Paradigma Alternativo: O trabalho posiciona-se como uma alternativa viável aos modelos fundacionais baseados em Transformers, sugerindo que RNNs multiplicativas (as quais o modelo Arrow se assemelha) surgem naturalmente de uma interpretação teoria-da-prova da predição de sequências.

Os autores mantêm-se modestos quanto à generalização para prompts ruidosos do mundo real, observando que os experimentos atuais dependem de subestruturas contíguas exatas. Eles enquadram este trabalho como um passo em direção a uma "conta teoria-da-prova de transformers", sugerindo direções futuras onde mecanismos de atenção poderiam ser interpretados como eliminação de implicação aproximada e seleção de hipóteses suave.