Résumé Technique : Modéliser la prédiction du prochain jeton comme une implication intuitionniste à imbrication gauche

Énoncé du problème

Les modèles d'IA générative fondamentaux, en particulier les Transformers, reposent sur la prédiction de jetons (tokens) non supervisée entraînée sur des ensembles de données massifs. Bien qu'efficaces, l'architecture Transformer standard occulte la structure logique de la prédiction de séquence. Elle traite les jetons comme des plongements (embeddings) additifs mélangés via des mécanismes d'attention, nécessitant des encodages de position explicites pour capturer l'ordre. Cette approche offre un lien explicatif limité avec le raisonnement symbolique ou la nature constructive de la dérivation de preuves. Le papier pose une question fondamentale : la prédiction du prochain jeton peut-elle être comprise comme l'extension d'une preuve dans la logique propositionnelle intuitionniste, et cette interprétation peut-elle engendrer une architecture neurale viable, sensible à l'ordre, sans dépendre des plongements additifs ou des encodages de position explicites ?

Méthodologie

Les auteurs proposent l'Arrow Language Model, une architecture neurale dérivée d'une interprétation de la logique intuitionniste de la prédiction du prochain jeton. La méthodologie procède par dérivation logique symbolique, preuve de théorèmes et réalisation neurale.

1. Formalisme logique : Implication à imbrication gauche

L'idée centrale est de représenter une séquence de jetons $w_1, \dots, w_n$ non pas comme un ensemble ou une chaîne à imbrication droite (qui est invariante par permutation sous la conjonction), mais comme une chaîne d'implications à imbrication gauche :
$$L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$$
Dans la logique intuitionniste, cette structure est sensible à l'ordre ; permuter les jetons modifie le type fonctionnel de l'antécédent.

• Prédiction du prochain jeton comme Modus Ponens : Prédire le jeton suivant $w$ étant donné un préfixe $P$ correspond à l'inférence logique $P \to w$. Si le préfixe est représenté comme une chaîne d'implication $I_p$ et la séquence complète comme $I_f = (I_p \to w)$, alors dériver $w$ est une instance de modus ponens.
• Correspondance de Curry–Howard : Sous cet isomorphisme, les propositions sont des types, et les preuves sont des $\lambda$-termes. Le préfixe est un $\lambda$-terme partiellement appliqué, et la prédiction du jeton suivant consiste à fournir un argument pour permettre une application de fonction ultérieure (élimination d'implication).

2. Preuve de théorèmes et récupération symbolique

Les auteurs utilisent des prouveurs de théorèmes spécialisés basés sur Prolog (implémentant le calcul LJT de Roy Dyckhoff) pour valider les propriétés de ces chaînes d'implication.

• Théorèmes : Ils démontrent que les chaînes à imbrication gauche supportent des prédictions à étape unique et multi-étapes. Par exemple, des théorèmes montrent comment un préfixe peut être « compilé » en opérateurs de continuation réutilisables (par exemple, transformer $((E \to a) \to b) \to c$ en une règle pour générer $b$ puis $c$).
• Récupération d'information : Un mécanisme de récupération symbolique est implémenté où les phrases sont stockées sous forme de chaînes d'implication. Les requêtes (sous-séquences) agissent comme des sous-formules pour récupérer les complétions exactes de la base de données, servant de référence basée sur la logique.

3. Réalisation neurale : Le modèle Arrow

Le papier dérive une architecture récurrente qui reflète la structure logique :

• État caché comme contexte de preuve : L'état caché $h_t \in \mathbb{R}^d$ représente le contexte de preuve accumulé après la consommation d'un préfixe.
• Jetons comme opérateurs : Au lieu de plongements additifs, chaque jeton $t$ agit comme un opérateur linéaire $M_t$ qui transforme l'état actuel.
• Paramétrage de faible rang : Pour gérer de grands vocabulaires, l'opérateur est défini comme une mise à jour de faible rang :
  $$M_t = I + U \text{diag}(s_t) V^\top$$
  où $U, V$ sont des matrices partagées et $s_t$ est un vecteur de porte spécifique au jeton dérivé d'une recherche de plongement (embedding lookup).
• Mise à jour de l'état (Modus Ponens) : La récurrence implémente l'élimination d'implication :
  $$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$$
  Cette mise à jour est intrinsèquement non commutative ($M_a M_b \neq M_b M_a$), encodant l'ordre intrinsèquement sans encodages de position.
• Entraînement : Le modèle est entraîné en utilisant l'entropie croisée standard du prochain jeton avec teacher forcing. La perte est calculée de manière séquentielle (streaming) pour gérer la mémoire sur des GPU grand public.

Contributions clés

1. Dérivation basée sur la logique : Le papier établit une correspondance formelle entre la profondeur des implications intuitionnistes à imbrication gauche et les étapes de calcul récurrent, fournissant une fondation de théorie de la preuve à la modélisation de séquences.
2. Architecture Arrow : Il introduit une architecture neurale spécifique où les jetons sont des opérateurs de transformation d'état plutôt que des vecteurs additifs, déplaçant le biais inductif de la « récupération via l'attention » vers la « transformation via la composition ».
3. Pont symbolique-neurale : Le travail démontre un lien étroit entre la preuve de théorèmes symboliques (récupération exacte via l'unification) et la prédiction neurale (récupération approximative via des scores de continuation appris).
4. Analyse théorique de l'ordre : Il prouve que les implications à imbrication gauche préservent naturellement l'ordre, tandis que les implications à imbrication droite (communes dans les formulations d'attention standard sans encodages de position) ne le font pas.

Résultats expérimentaux

Les expériences se concentrent sur la validation de la capacité de l'architecture à apprendre des motifs sensibles à l'ordre et à imiter la récupération symbolique, plutôt que de rivaliser avec les modèles de langage à l'état de l'art sur des benchmarks généraux.

• Surapprentissage/Tests de cohérence : Le modèle a été testé sur de petits ensembles de données (textes de Project Gutenberg) avec un régime de surapprentissage délibéré. L'ensemble d'entraînement a été augmenté de tous les fragments contigus de phrases pour imiter la récupération de niveau logique des sous-formules.
• Performance : Le modèle a réussi à surapprendre les données d'entraînement, atteignant une perte d'entraînement proche de zéro sur de petits documents (ex: Le Magicien d'Oz, Moby Dick) en quelques minutes sur un seul RTX 3090.
• Récupération vs Génération :
  • Référence symbolique : La récupération basée sur Prolog a obtenu des correspondances exactes pour les requêtes contre les chaînes d'implication stockées.
  • Imitation neurale : Le modèle Arrow, lorsqu'interrogé avec un préfixe, pouvait classer les candidats de complétion de suffixe (dérivés du corpus d'entraînement) en fonction de scores de continuation appris, imitant efficacement le processus de récupération logique.
  • Génération libre : Le modèle pouvait générer des continuations fluides au-delà des correspondances exactes mémorisées, démontant que la composition d'opérateurs a appris une structure séquentielle généralisable.
• Scalabilité : Le débit d'entraînement était linéaire par rapport à la longueur de la séquence, et le modèle a pu passer à des corpus de longueur livre (ex: Guerre et Paix) avec une utilisation de mémoire gérable grâce au calcul de perte en mode streaming.

Signification et Revendications

Le papier prétend offrir une fondation basée sur la logique pour la prédiction du prochain jeton qui est distincte de l'attention basée sur la similitude ou des alternatives de convolution/espace d'état.

• Ordre Intrinsèque : En encodant l'ordre via la composition d'opérateurs non commutatifs, le modèle Arrow élimine le besoin d'encodages de position explicites, alignant l'architecture plus étroitement avec la nature constructive de l'extension de preuve.
• Explicabilité : L'architecture fournit une correspondance directe avec la logique intuitionniste, où les mises à jour d'état correspondent aux étapes de preuve (modus ponens) et les états cachés correspondent aux contextes de preuve. Cela offre une voie potentielle vers des modèles neuraux plus interprétables.
• Paradigme Alternatif : Ce travail positionne l'architecture comme une alternative viable aux modèles de fondation basés sur les Transformers, suggérant que les RNN multiplicatifs (auxquels le modèle Arrow ressemble) découlent naturellement d'une interprétation de la théorie des preuves de la prédiction de séquence.

Les auteurs restent modestes quant à la généralisation à des prompts réels et bruités, notant que les expériences actuelles reposent sur des sous-structures contiguës exactes. Ils présentent ce travail comme une étape vers un « compte de la théorie des preuves des transformers », suggérant des directions futures où les mécanismes d'attention pourraient être interprétés comme une élimination d'implication approximative et une sélection de l'hypothèse douce.