💻 computer science

On the (Intuitionistic) Logic of Next-Token Prediction

Cet article modélise la prédiction du prochain jeton dans les réseaux de neurones autorégressifs en utilisant la logique implicationnelle intuitionniste et la correspondance de Curry-Howard, où la génération de jetons correspond au modus ponens et le traitement de séquences à l'extension de preuve constructive, dérivant finalement une architecture neuronale équivalente aux RNN multiplicatifs et validant ses propriétés à travers des prouveurs de théorèmes spécialisés.

Auteurs originaux : Paul Tarau (University of North Texas)

Publié 2026-08-11

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Paul Tarau (University of North Texas)

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez d'apprendre à un robot comment raconter une histoire. Vous lui donnez les premiers mots et il doit deviner le suivant. La plupart des robots modernes, comme ceux qui alimentent les chatbots d'aujourd'hui, font cela en regardant toute l'histoire jusqu'ici et en se demandant : « Quel mot traîne habituellement avec ceux-là ? » Ils utilisent un immense projecteur appelé « attention » pour scanner les mots passés et trouver la meilleure correspondance. C'est comme un bibliothécaire qui se souvient de chaque livre jamais écrit et trouve celui qui ressemble le plus à celui que vous tenez.

Mais il y a une autre façon de voir les choses. Au lieu de simplement chercher des mots similaires, et si le robot traitait l'histoire comme une chaîne d'étapes logiques ? Imaginez que chaque mot n'est pas seulement un mot, mais une petite instruction qui modifie l'état de l'histoire. Si vous dites « Le chat », ce n'est pas seulement une description ; c'est une commande qui instaure une attente spécifique pour ce qui suit. Dans cette perspective, prédire le mot suivant revient à résoudre un casse-tête mathématique ou à compléter une démonstration : si vous avez les conditions initiales correctes, la prochaine étape est la seule chose logique qui puisse arriver. Ce document explore cette idée, demandant si nous pouvons construire un robot qui apprend en suivant ces chaînes logiques plutôt qu'en imitant des motifs.

Le Modèle Arrow : Quand les mots deviennent des clés à molette

Dans cet article, Paul Tarau propose une nouvelle façon de regarder comment l'IA prédit le mot suivant dans une phrase. Il appelle sa nouvelle idée l'Arrow Language Model (Modèle de Langage Fléché). Au lieu de la méthode habituelle où l'IA scanne une immense liste de mots passés pour trouver des similitudes, Tarau suggère de traiter la séquence de mots comme une preuve logique.

Voici l'idée centrale : Imaginez que vous construisez une tour avec des blocs. Dans l'ancienne méthode (comme les Transformers), vous regardez toute la tour et demandez : « Quel bloc sient le mieux au sommet ? » Dans la nouvelle méthode de Tarau, chaque bloc que vous ajoutez est en fait un outil spécial, comme une clé à molette ou un tournevis. Lorsque vous ajoutez un bloc, il ne se contente pas de rester là ; il modifie la forme de la tour située en dessous de lui. Le prochain bloc que vous ajouterez devra s'adapter à la nouvelle forme créée par le précédent.

Tarau utilise une branche des mathématiques appelée logique intuitionniste pour décrire cela. Dans cette logique, une phrase n'est pas seulement une liste de mots ; c'est une longue chaîne imbriquée d'énoncés « si-alors ».

Si vous avez le mot « Le », cela établit une condition.
Si vous ajoutez « chat », cela modifie cette condition.
Si vous ajoutez « s'assoit », cela la modifie à nouveau.

L'article suggère que prédire le mot suivant est exactement comme le Modus Ponens, une règle de logique célèbre qui dit : « Si j'ai "Si P alors Q", et que j'ai "P", alors je dois avoir "Q" ». Dans le cerveau de l'IA, l'état actuel de la phrase est le « Si P alors Q », et le nouveau mot est le « P ». Le résultat ? Le mot suivant surgit comme étant le « Q ».

Comment la machine fonctionne

Pour faire fonctionner cela dans un véritable ordinateur, Tarau a construit un réseau neuronal où chaque mot est un opérateur. Considérez la mémoire de l'IA (son « état caché ») comme un morceau d'argile.

Dans l'IA normale, les mots sont comme des autocollants que l'on colle sur l'argile.
Dans le Modèle Arrow, les mots sont comme des mains qui pressent et tordent l'argile.

Quand le mot « Le » arrive, il tord l'argile d'une certaine manière. Quand « chat » arrive, il la tord d'une manière différente. Parce que tordre l'argile avec « Le » puis avec « chat » crée une forme différente que de faire « chat » d'abord puis « Le », l'ordre des mots est intégré directement dans les mathématiques. Vous n'avez pas besoin de dire à l'ordinateur « ce mot est premier » ou « ce mot est second » avec des codes supplémentaires ; l'action de torsion se souvient naturellement de l'ordre.

L'article montre que cette action de torsion est mathématiquement la même chose que de multiplier des matrices (une façon pour les ordinateurs de faire des mathématiques avec des grilles de nombres). Cela rend le modèle très efficace. Il n'a pas besoin de regarder en arrière tout l'historique de la phrase à chaque fois ; il a juste besoin de connaître la forme actuelle de l'argile et d'appliquer la torsion suivante.

Les Expériences : Peut-il apprendre ?

L'auteur a testé cette idée avec un objectif très précis : voir si le modèle pouvait « mémoriser » un livre en apprenant la structure logique de ses phrases. Ils ont pris des livres du domaine public (comme Guerre et Paix et Moby Dick) et les ont injectés dans le modèle.

Pour s'assurer que le test était équitable et clair, ils n'ont pas demandé au modèle d'écrire de nouvelles histoires. Au lieu de cela, ils lui ont demandé de terminer des phrases qu'il avait déjà vues.

La configuration : Ils ont donné au modèle un morceau de phrase (comme « Le chat ») et lui ont demandé de prédire la suite.
Le contrôle de la logique : Ils ont également construit un « robot logique » (en utilisant un langage de programmation appelé Prolog) qui pouvait résoudre les mêmes phrases en utilisant des règles mathématiques pures.
Le résultat : Le Modèle Arrow a appris à prédire les mots suivants presque parfaitement, correspondant aux réponses du robot logique.

L'article rapporte que le modèle pouvait s'entraîner sur de grands livres très rapidement. Par exemple, il a fallu environ 7 minutes et 52 secondes pour s'entraîner sur Guerre et Paix (qui compte plus de 560 000 mots) en utilisant une carte graphique standard. Il pouvait aussi terminer une phrase en environ 0,1 à 0,3 seconde.

Ce que cela signifie (et ce que cela ne signifie pas)

L'article suggère que nous n'avons pas besoin du gigantesque « projecteur » (l'attention) que la plupart des IA modernes utilisent pour comprendre l'ordre. Au lieu de cela, l'ordre peut être construit directement dans la façon dont les mots modifient l'état de l'IA. Cela offre une manière différente, et peut-être plus simple, de construire des modèles de langage.

Cependant, l'auteur prend soin de souligner les limites. Cette expérience a fonctionné parce que l'IA n'a été demandée que de terminer des phrases qu'elle avait déjà vues, comme un étudiant récitant un poème qu'il a mémorisé. L'article admet que ce modèle pourrait avoir des difficultés si vous lui donnez une phrase avec une faute de frappe, un mot manquant ou une formulation étrange qu'il n'a pas vue auparavant. Le langage du monde réel est désordonné, et cette approche par « preuve logique » est actuellement plus efficace pour gérer des motifs propres et précis.

L'auteur note également que, bien que ce modèle soit excellent pour comprendre l'ordre grâce aux torsions et aux rotations, il ne gère pas encore les connexions de la « vue d'ensemble » que la méthode du projecteur permet de saisir. C'est une nouvelle direction prometteuse, suggérant que l'avenir de l'IA ne sera peut-être pas seulement de trouver des mots similaires, mais de comprendre comment chaque mot transforme logiquement l'histoire.

En bref, cet article propose que le secret pour prédire le mot suivant n'est pas seulement de se souvenir du passé, mais de traiter chaque mot comme un outil qui façonne le futur. C'est une façon ludique, logique et mathématiquement élégante de penser à la manière dont les machines pourraient apprendre à parler.

Résumé Technique : Sur la Logique (Intuitionniste) de la Prédiction du Prochain Jeton

Énoncé du Problème

Le document traite du manque de transparence logique des modèles actuels d'IA générative fondamentale, particulièrement les Transformers. Bien que les Transformers apprennent efficacement la prédiction du prochain jeton via un apprentissage non supervisé sur des ensembles de données massifs, leur dépendance aux encodages positionnels et aux mécanismes d'attention basés sur la similitude occulte la structure logique sous-jacente de la prédiction de séquence. L'auteur postule que la tâche de prédiction du prochain jeton peut être réinterprétée non pas simplement comme une reconnaissance de formes statistiques, mais comme une tâche de complétion de preuve constructive au sein de la logique implicative intuitionniste. Le défi central consiste à dériver une architecture neurale qui incarne naturellement cette interprétation logique, en remplaçant les mécanismes d'attention par une composition d'opérateurs qui encode intrinsèquement l'ordre.

Méthodologie

1. Formalisme Logique : Implication à Imbrication Gauche

L'auteur propose de modéliser les séquences de jetons comme des implications intuitionnistes à imbrication gauche. Contrairement aux implications à imbrication droite (qui s'effondrent en conjonctions et sont invariantes par permutation), les implications à imbrication gauche préservent la sensibilité à l'ordre.

Représentation : Une séquence de jetons $w_1, \dots, w_n$ est encodée sous la forme $L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$ .
Mécanisme d'Inférence : La prédiction du prochain jeton est mappée sur le Modus Ponens. Étant donné une implication de préfixe $I_p$ et une implication complète $I_f = (I_p \to w)$ , prédire $w$ correspond à l'étape d'élimination $I_f \to (I_p \to I_f) \to w$ .
Correspondance de Curry-Howard : Sous cet isomorphisme, les propositions sont des types, les preuves sont des termes $\lambda$ , et la prédiction du prochain jeton est la construction d'un terme habitant un type implicatif. Le processus de prédiction d'une séquence est vu comme des $\beta$ -réductions successives (mises à jour d'état).

2. Outils Théoriques

L'auteur utilise le calcul LJT de Roy Dyckhoff, un calcul de séquents pour la logique propositionnelle intuitionniste restreint à la fragmentation implicative. Ils implémentent des prouveurs de théorèmes spécialisés en Prolog (lprove/2) pour :

Valider la validité de l'encodage logique.
Démontrer que l'ordre est préservé dans les chaînes à imbrication gauche (par exemple, $((p \to q) \to r)$ n'est pas équivalent à $((q \to p) \to r)$ ).
Effectuer la recherche d'information en traitant les fragments de phrases comme des sous-formules (suffixes de préfixes) de chaînes d'implication stockées.

3. Architecture Neurale : Le Modèle de Langage "Arrow"

Le document dérive une architecture récurrente, le Modèle Arrow, qui sert de réalisation numérique de la construction de preuve logique.

État Caché comme Contexte de Preuve : L'état caché $h_t \in \mathbb{R}^d$ représente le contexte de preuve accumulé (hypothèses et justifications) après le traitement d'un préfixe.
Jetons comme Opérateurs : Au lieu d'embeddings additifs, chaque jeton $t$ agit comme un opérateur linéaire $M_t: \mathbb{R}^d \to \mathbb{R}^d$ qui transforme l'état actuel.
Paramétrage de Bas Rang : Pour gérer efficacement les grands vocabulaires, l'opérateur est défini comme $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é des embeddings.
Mise à jour d'État (Modus Ponens) : La relation de récurrence implémente l'élimination de l'implication :
$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$
Cette mise à jour est non-commutative ( $M_a M_b \neq M_b M_a$ ), ce qui signifie que l'ordre des jetons est encodé intrinsèquement par l'algèbre de la composition d'opérateurs, éliminant ainsi le besoin d'encodages positionnels explicites.
Entraînement : Le modèle utilise l'entropie croisée standard du prochain jeton avec "teacher forcing". Pour gérer la mémoire pour les grands vocabulaires, la perte est calculée de manière séquentielle (streaming).

Contributions Clés

Interprétation Logique de la Prédiction du Prochain Jeton : Le document établie une correspondance formelle où la prédiction du prochain jeton est équivalente à l'extension de preuve constructive (Modus Ponens) dans la logique implicative intuitionniste.
Dérivation du Modèle Arrow : Une nouvelle architecture récurrente est dérivée directement de l'interprétation de la théorie de la preuve, où les jetons fonctionnent comme des opérateurs de transformation d'état plutôt que comme des embeddings statiques.
Sensibilité à l'Ordre sans Encodages Positionnels : Le modèle démontre que la composition non-commutative d'opérateurs encode intrinsèquement l'ordre des séquences, offrant une alternative aux stratégies d'encodage positionnel utilisées dans les Transformers.
Cadre de Récupération Symbolique-Neurale : L'auteur démontre un cadre unifié où tant la récupération symbolique (via le prouveur de théorèmes Prolog sur les chaînes d'implication) que la récupération neurale (via le modèle Arrow) opèrent sur la même structure logique sous-jacente.

Résultats Expérimentaux

L'auteur a mené des expériences pour valider les algorithmes logiques et leurs équivalents neuraux en utilisant des textes du domaine public issus de Project Gutenberg.

Configuration : Les expériences ont utilisé un régime de "Vérification de Cohérence" (Sanity Check) où les modèles ont été entraînés pour sur-apprendre (overfit) de petits corpus (ex: Le Magicien d'Oz, Moby Dick) afin de vérifier la capacité d'apprentissage et l'efficacité architecturale.
Augmentation de Données : Pour imiter la récupération de sous-formules au niveau logique, l'ensemble d'entraînement a été augmenté avec tous les fragments contigus de phrases.
Performance :
- Efficacité d'Entraînement : Le modèle Arrow entraîné sur de grands documents (ex: Guerre et Paix avec ~560k mots) en moins de 8 minutes sur un seul GPU grand public (RTX 3090).
- Inférence : Le pipeline de récupération par priorité (énumération des candidats suivie d'un scoring neural) a atteint des temps d'inférence de 0,1 à 0,3 seconde par requête, largement indépendant de la taille totale du corpus.
- Référence Symbolique : Le système de récupération basé sur Prolog a démontré une initialisation de base de données rapide (1-2 secondes) et des temps de requête interactifs (~0,5 seconde), confirmant la faisabilité de l'utilisation de la récupération au niveau logique comme une référence interprétable.

Signification et Revendications

Le document présente le Modèle de Langage Arrow comme une fondation axée sur la logique pour la prédiction du prochain jeton, distincte de l'attention basée sur la similitude (Transformers) ou des alternatives de convolution/espace d'état.

Pouvoir Explicatif : En mappant les opérations neurales sur des concepts de théorie de la preuve (élimination de l'implication, $\beta$ -réduction), le modèle offre un lien explicatif entre la dynamique neurale et le raisonnement symbolique qui fait défaut aux Transformers.
Perspective Architecturale : Le Modèle Arrow est positionné comme une alternative pilotée par la logique pour les tâches où la sensibilité à l'ordre et l'extension de preuve constructive sont primordiales, bien que l'auteur note explicitement qu'il n'est pas encore un remplacement direct pour les modèles fondamentaux dans des contextes généraux.
Limites : L'auteur reconnaît que le travail actuel se concentre sur les sous-structures contigues exactes. Il ne traite pas encore des exigences de robustesse des modèles de langage modernes, telles que la gestion des fautes d'orthographe, des paraphrases ou des preuves non contiguës, qui sont des domaines de travaux futurs.
Directions Futures : Le document identifie l'émulation de l'inférence de type Transformer (correspondance approximative) en utilisant des techniques similaires basées sur la logique comme un défi central ouvert.

Le travail est présenté comme une étape vers des "alternes aux modèles de fondation basés sur les Transformers", ancrée dans l'intuition que la structure logique de la prédiction de séquence peut être rendue explicite et constructive grâce à la logique intuitionniste.