Technische Samenvatting: Over de (Intuïtionistische) Logica van Volgende-Token Voorspelling

Probleemstelling

Het artikel behandelt het gebrek aan logische transparantie in huidige fundamentele generatieve AI-modellen, met name Transformers. Hoewel Transformers effectief leren via volgende-token voorspelling door ongesuperviseerd trainen op enorme datasets, verhult hun afhankelijkheid van positionele encodings en op gelijkenis gebaseerde aandachtmechanismen de onderliggende logische structuur van sequentievoorspelling. De auteur stelt dat de taak van het voorspellen van het volgende token niet louter als statistische patroonherkenning kan worden geherinterpreteerd, maar als een constructieve bewijs-voltooiingstaak binnen de intuïtionistische implicatielogica. De kernuitdaging is het afleiden van een neurale architectuur die deze logische interpretatie van nature belichaamt, waarbij aandachtmechanismen worden vervangen door operatorcompositie die orde intrinsiek codeert.

Methodologie

1. Logische Formalisering: Links-geneste Implicatie

De auteur stelt voor om tokensequenties te modelleren als links-geneste intuïtionistische implicaties. In tegenstelling tot rechts-geneste implicaties (die inklappen tot conjuncties en permutatie-invariant zijn), behouden links-geneste implicaties de gevoeligheid voor volgorde.

• Representatie: Een sequentie van tokens $w_1, \dots, w_n$ wordt gecodeerd als $L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$.
• Inferentiemechanisme: Voorspelling van het volgende token wordt in kaart gebracht als Modus Ponens. Gegeven een prefix-implicatie $I_p$ en een volledige implicatie $I_f = (I_p \to w)$, komt het voorspellen van $w$ overeen met de eliminatiestap $I_f \to (I_p \to I_f) \to w$.
• Curry-Howard Correspondentie: Onder deze isomorfie zijn proposities types, bewijzen $\lambda$-termen, en is het voorspellen van het volgende token de constructie van een term die een implicatieve type bewoont. Het proces van het voorspellen van een sequentie wordt gezien als opeenvolgende $\beta$-reducties (toestandsupdates).

2. Theoretische Instrumenten

De auteur maakt gebruik van Roy Dyckhoffs LJT-calculus, een sequentencalculus voor propositionele intuïtionistische logica die beperkt is tot het implicatieve fragment. Zij implementeren gespecialiseerde theorem provers in Prolog (lprove/2) om:

• De geldigheid van de logische codering te valideren.
• Aan te tonen dat volgorde behouden blijft in links-geneste ketens (bijv. $((p \to q) \to r)$ is niet equivalent aan $((q \to p) \to r)$).
• Informatie-extractie uit te voeren door zinsfragmenten te behandelen als subformules (suffixen van prefixen) van opgeslagen implicatieketens.

3. Neurale Architectuur: Het Arrow Language Model

Het artikel leidt een recurrente neurale architectuur af, het Arrow Model, dat dient als een numerieke realisatie van de logische bewijsconstructie.

• Verborgen Toestand als Bewijscontext: De verborgen toestand $h_t \in \mathbb{R}^d$ vertegenwoordigt de geaccumuleerde bewijscontext (aannames en rechtvaardigingen) na het verwerken van een prefix.
• Tokens als Operatoren: In plaats van additieve embeddings, fungeert elk token $t$ als een lineaire operator $M_t: \mathbb{R}^d \to \mathbb{R}^d$ die de huidige toestand transformeert.
• Low-Rank Parameterisatie: Om grote vocabulaire efficiënt te verwerken, wordt de operator gedefinieerd als $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 embeddings.
• Toestandsupdate (Modus Ponens): De recurrente relatie implementeert implicatie-eliminatie:
  $$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$$
  Deze update is niet-commutatief ($M_a M_b \neq M_b M_a$), wat betekent dat de tokenvolgorde intrinsiek wordt gecodeerd door de algebra van operatorcompositie, waardoor expliciete positionele encodings overbodig worden.
• Training: Het model gebruikt standaard volgende-token cross-entropie met teacher forcing. Om het geheugenbeheer voor grote vocabularia te beheren, wordt de loss op een streaming wijze berekend.

Belangrijkste Bijdragen

1. Logische Interpretatie van Volgende-Token Voorspelling: Het artikel legt een formele correspondentie vast waarbij het voorspellen van het volgende token gelijkstaat aan constructieve bewijsverlenging (Modus Ponens) in de intuïtionistische implicatielogica.
2. Afleiding van het Arrow Model: Het artikel leidt een nieuwe recurrente architectuur af die direct voortkomt uit de bewijs-theoretische interpretatie, waarbij tokens fungeren als toestands-transformerende operatoren in plaats van statische embeddings.
3. Ordegevoeligheid zonder Positionele Encodings: Het model toont aan dat niet-commutatieve operatorcompositie de volgorde van sequenties inherent codeert, wat een alternatief biedt voor de strategieën van positionele encoding die in Transformers worden gebruikt.
4. Symbolisch-Neuraal Retrieval Framework: De auteur demonstreert een verenigd framework waar zowel symbolische retrieval (via Prolog theorem proving op implicatieketens) als neurale retrieval (via het Arrow model) opereren op dezelfde onderliggende logische structuur.

Experimentele Resultaten

De auteur heeft experimenten uitgevoerd om de logica-gebaseerde algoritmen en hun neurale equivalenten te valideren met behulp van publiek domein teksten van Project Gutenberg.

• Setup: De experimenten maakten gebruik van een "Sanity Check" regime waarbij de modellen werden getraind om kleine corpora te overfitten (bijv. The Wizard of Oz, Moby Dick) om de leercapaciteit en architecturale efficiëntie te verifiëren.
• Data Augmentatie: Om de logische niveau-retrieval van subformules na te bootsen, werd de trainingsset uitgebreid met alle opeenvolgende fragmenten van zinnen.
• Prestaties:
  • Trainingsefficiëntie: Het Arrow model trainde op grote documenten (bijv. War and Peace met ~560k woorden) in minder dan 8 minuten op een enkele consumenten GPU (RTX 3090).
  • Inference: De retrieval-first pipeline (kandidaat-enumeratie gevolgd door neurale scoring) bereikte inferentietijden van 0,1–0,3 seconden per query, grotendeels onafhankelijk van de totale corpusgrootte.
  • Symbolische Baseline: Het Prolog-gebaseerde retrieval systeem demonstreerde snelle database-initialisatie (1–2 seconden) en interactieve query-tijden (~0,5 seconden), wat de haalbaarheid van het gebruik van logica-niveau retrieval als een interpreteerbare baseline bevestigt.

Betekenis en Claims

Het artikel presenteert het Arrow Language Model als een logica-eerst fundament voor volgende-token voorspelling dat onderscheidt van gelijkenis-gebaseerde aandacht (Transformers) en convolutie/state-space alternatieven.

• Verklarende Kracht: Door neurale operaties in kaart te brengen naar bewijs-theoretische concepten (implicatie-eliminatie, $\beta$-reductie), biedt het model een verklarende verbinding tussen neurale dynamiek en symbolisch redeneren die Transformers missen.
• Architecturaal Perspectief: Het Arrow Model wordt gepositioneerd als een logica-gestuurd alternatief voor taken waar ordegevoeligheid en constructieve bewijsverlenging van belang zijn, hoewel de auteur expliciet opmerkt dat het nog geen directe vervanging is voor fundamentele modellen in algemene settings.
• Beperkingen: De auteur erkent dat het huidige werk zich richt op exacte opeenvolgende substructuren. Het adresseert nog niet de robuustheidseisen van moderne taalmodellering, zoals het omgaan met spelfouten, parafrases of niet-opeenvolgende bewijslast, wat gebieden zijn voor toekomstig onderzoek.
• Toekomstige Richtingen: Het artikel identificeert de emulatie van Transformer-stijl inferentie (benaderende matching) met behulp van vergelijkbare logica-gebaseerde technieken als een centrale openstaande uitdaging.

Het werk wordt gepresenteerd als een stap naar "alternatieven voor transformer-gebaseerde fundamentele modellen", geworteld in de intuïtie dat de logische structuur van sequentievoorspelling expliciet en constructief gemaakt kan worden door middel van de intuïtionistische logica.