Technische Samenvatting: Modellering van Next-Token Predictie als Links-Geneste Intuïtionistische Implicatie

Probleemstelling

Fundamentele generatieve AI-modellen, met name Transformers, vertrouwen op ongesuperviseerde next-token predictie getraind op enorme datasets. Hoewel effectief, verbergt de standaard Transformer-architectuur de logische structuur van sequentievoorspelling. Het behandelt tokens als additieve embeddings die via aandachtmechanismen worden gemengd, wat expliciete positionele encodings vereist om volgorde te vangen. Deze aanpak biedt een beperkte verklarende verbinding met symbolische redenering of de constructieve aard van bewijsafleiding. Het artikel stelt een fundamentele vraag: kan next-token predictie worden begrepen als het uitbreiden van een bewijs in de intuïtionistische propositielogica, en kan deze interpretatie een levensvatbare, volgordegevoelige neurale architectuur opleveren zonder te vertrouwen op additieve embeddings of expliciete positionele encodings?

Methodologie

De auteurs stellen het Arrow Language Model voor, een neurale architectuur afgeleid van een intuïtionistisch-logische interpretatie van next-token predictie. De methodologie verloopt via symbolische logische afleiding, bewijsvoering en neurale realisatie.

1. Logisch Formalisme: Links-Geneste Implicatie

Het kerninzicht is om een sequentie van tokens $w_1, \dots, w_n$ niet te representeren als een verzameling of een rechts-geneste keten (die permutatie-invariant is onder conjunctie), maar als een links-geneste implicatieketen:
$$L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$$
In de intuïtionistische logica is deze structuur volgordegevoelig; het permuteren van tokens verandert het functionele type van het antecedent.

• Next-Token Predictie als Modus Ponens: Het voorspellen van het volgende token $w$ gegeven een prefix $P$ komt overeen met de logische inferentie $P \to w$. Als de prefix wordt gerepresenteerd als een implicatieketen $I_p$ en de volledige sequentie als $I_f = (I_p \to w)$, dan komt het afleiden van $w$ overeen met een instantie van modus ponens.
• Curry–Howard Correspondentie: Onder deze isomorfie zijn proposities types, en bewijzen zijn $\lambda$-termen. De prefix is een gedeeltelijk toegepast $\lambda$-term, en het voorspellen van het volgende token is het leveren van een argument om verdere functie-applicatie mogelijk te maken (implicatie-eliminatie).

2. Bewijsvoering en Symbolische Retrieval

De auteurs maken gebruik van gespecialiseerde Prolog-gebaseerde theorem provers (die de Roy Dyckhoff LJT-calculus implementeren) om eigenschappen van deze implicatieketens te valideren.

• Stellingen: Zij demonstreren dat links-geneste ketens zowel enkelvoudige als meerstaps-predicties ondersteunen. Bijvoorbeeld, stellingen tonen hoe een prefix kan worden "gecompileerd" naar herbruikbare continuatie-operators (bijv. het transformeren van $((E \to a) \to b) \to c$ naar een regel voor het genereren van $b$ en vervolgens $c$).
• Informatie Retrieval: Een symbolisch retrieval-mechanisme is geïmplementeerd waarbij zinnen worden opgeslagen als implicatieketens. Queries (sub-sequenties) fungeren als subformules om exacte completions uit de database te halen, wat dient als een logische baseline.

3. Neurale Realisatie: Het Arrow Model

Het artikel leidt een recurrente neurale architectuur af die de logische structuur weerspiegelt:

• Hidden State als Bewijscontext: De hidden state $h_t \in \mathbb{R}^d$ representeert de geaccumuleerde bewijscontext na het consumeren van een prefix.
• Tokens als Operators: In plaats van additieve embeddings fungeert elk token $t$ als een lineaire operator $M_t$ die de huidige staat transformeert.
• Low-Rank Parameterisatie: Om grote vocabulaire te verwerken, is de operator gedefinieerd als een low-rank update:
  $$M_t = I + U \text{diag}(s_t) V^\top$$
  waarbij $U, V$ gedeelde matrices zijn en $s_t$ een token-specifieke gate vector is afgeleid van een embedding lookup.
• State Update (Modus Ponens): De recurrentie implementeert implicatie-eliminatie:
  $$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$$
  Deze update is inherent niet-commutatief ($M_a M_b \neq M_b M_a$), waardoor volgorde intrinsiek wordt gecodeerd zonder positionele encodings.
• Training: Het model wordt getraind met standaard next-token cross-entropy met teacher forcing. De loss wordt in een streaming-modus berekend om geheugen te beheren op commodity GPU's.

Belangrijkste Bijdragen

1. Logica-gebaseerde Afleiding: Het artikel legt een formele correspondentie vast tussen de diepte van links-geneste intuïtionistische implicaties en de stappen van recurrente computatie, wat een bewijs-theoretische fundering biedt voor sequentiemodellering.
2. Arrow Architectuur: Het introduceert een specifieke neurale architectuur waarbij tokens state-transformerende operators zijn in plaats van additieve vectoren, waardoor de inductieve bias verschuift van "retrieval via attention" naar "transformatie via compositie".
3. Symbolisch-Neurale Brug: Het werk demonstreert een nauwe link tussen symbolische theorem proving (exacte retrieval via unificatie) en neurale predictie (benaderende retrieval via geleerde continuation scores).
4. Theoretische Analyse van Orde: Het bewijst dat links-geneste implicaties de volgorde natuurlijk behouden, terwijl rechts-geneste implicaties (gebruikelijk in standaard attention-formuleringen zonder positionele encodings) dat niet doen.

Experimentele Resultaten

De experimenten richten zich op het valideren van het vermogen van de architectuur om volgordegevoelige patronen te leren en in staat te zijn om symbolische retrieval te imiteren, in plaats van te concurreren met state-of-the-art taalmodellen op algemene benchmarks.

• Overfitting/Sanity Checks: Het model werd getest op kleine datasets (Project Gutenberg teksten) met een bewuste overfitting-regime. De trainingsset werd uitgebreid met alle opeenvolgende fragmenten van zinnen om de logische retrieval van subformules na te bootsen.
• Prestaties: Het model slaagde erin om te overfitten op de trainingsdata, waarbij een bijna nul-verlies op kleine documenten (bijv. The Wizard of Oz, Moby Dick) werd bereikt binnen enkele minuten op een enkele RTX 3090 GPU.
• Retrieval vs. Generatie:
  • Symbolische Baseline: Prolog-gebaseerde retrieval bereikte exacte matches voor queries tegen de opgeslagen implicatieketens.
  • Neurale Mimic: Het Arrow model kon bij een query met een prefix kandidaat-suffix completions (afgeleid van de trainingscorpus) rangschikken op basis van geleerde continuation scores, waarmee het het logische retrieval-proces effectief imiteerde.
  • Vrije Generatie: Het model kon vloeiende continuaties genereren die verder gingen dan exacte memoriseerde matches, wat aantoont dat de operator-compositie een generaliseerbare sequentiële structuur heeft geleerd.
• Schaalbaarheid: De trainingsdoorvoer was lineair ten opzichte van de sequentielengte, en het model schaalde naar boeklengte corpora (bijv. War and Peace) met beheersbaar geheugengebruik dankzij streaming loss-computatie.

Betekenis en Claims

Het artikel claimt een logica-eerst fundament te bieden voor next-token predictie dat onderscheidend is van similarity-gebaseerde attention en convolutie/state-space alternatieven.

• Intrinsieke Orde: Door de volgorde te coderen via niet-commutatieve operator-compositie, elimineert het Arrow-model de noodzaak voor expliciete positionele encodings, waardoor de architectuur dichter bij de constructieve aard van bewijs-extensie komt te staan.
• Verklaarbaarheid: De architectuur biedt een directe mapping naar de intuïtionistische logica, waarbij state-updates corresponderen met bewijsstappen (modus ponens) en hidden states corresponderen met bewijscontexten. Dit biedt een potentiële weg naar meer interpreteerbare neurale modellen.
• Alternatief Paradigma: Dit werk positioneert zichzelf als een levensvatbaar alternatief voor Transformer-gebaseerde fundamentele modellen, door te suggereren dat multiplicatieve RNN's (waar het Arrow-model op lijkt) natuurlijk voortvloeien uit een bewijs-theoretische interpretatie van sequentie-predictie.

De auteurs blijven bescheiden over de generalisatie naar ruisige, real-world prompts, waarbij zij opmerken dat de huidige experimenten steunen op exacte opeenvolgende substructuren. Zij presenteren dit werk als een stap naar een "bewijs-theoretische account van transformers", waarbij zij toekomstige richtingen suggereren waar attention-mechanismen geïnterpreteerd kunnen worden als benaderende implicatie-eliminatie en soft hypothese-selectie.