Technische Samenvatting: Een PyTorch-bibliotheek van Turing-volledige Neurale Netwerken

Probleemstelling

Hoewel de theoretische literatuur al lang heeft vastgesteld dat neurale netwerken Turing-machines (TM's) kunnen simuleren – met name via recurrente netwerken (Siegelmann & Sontag, 1995) en transformers met harde attention (Pérez et al., 2021; Wei, Chen, & Ma, 2021) – blijft er een aanzienlijke kloof bestaan tussen wiskundige bewijzen die gewichtsmatrices specificeren en uitvoerbare, concrete implementaties. Bestaande bewijzen vertrouwen vaak op oneindige precisie of abstracte constructies die moeilijk te instantiëren zijn in standaard deep learning-frameworks. Dit artikel adresseert de behoefte aan een "concrete, uitvoerbare referentie" die de symbolische en neurale domeinen overbrugt door een Turing-machinebeschrijving direct te compileren tot een neurale netwerk met vaste, interpreteerbare gewichten, zonder dat training vereist is.

Methodologie

De auteurs presenteren een PyTorch-pakket dat neurale netwerken construeert op basis van een gegeven TM-overgangsfunctie ($\delta$) en een verzameling terminale toestanden. De compilatie verloopt via een hiërarchie van componenten, waarbij wordt gegarandeerd dat de forward pass van het netwerk exact één stap van de gespecificeerde machine implementeert. Twee verschillende architecturen zijn geïmplementeerd, die elk een ander theoretisch resultaat realiseren:

1. Kerncomponenten

De constructie vertrouwt op het bouwen van complexe logica uit basis-ReLU-geactiveerde poorten:

• Booleaanse logica: Het artikel demonstreert hoe ReLU-netwerken elementaire poorten (EN, OF, NIET, XOR) implementeren en deze composeert tot Disjunctieve Normale Vorm (DNF)-schakelingen.
• Overgangsfunctie: De eindige zoektabel $\delta$ wordt gerealiseerd als een DNF-schakeling van twee lagen, waarbij één verborgen neuron bestaat voor elk toestands-symboolpaar.
• Binaire rekenkunde: Ripple-carry-adders, opgebouwd uit half-adders en full-adders, worden gebruikt om de koppositie bij te werken (het inkrementeren of decrementeren van binaire gecodeerde gehele getallen).
• Positieve opzoeking: Harde attention-mechanismen (benaderd via een softmax met hoge temperatuur) voeren exacte positieve opzoekingen uit op de tape-historie en de originele invoer door binaire sleutel-query-vectoren te matchen.

2. Architectuur A: WCM21 (Transformer-gebaseerd)

Gebaseerd op de constructie van Wei, Chen en Ma (2021), is dit een encoder-decoder transformer:

• Encoder: Slaat de initiële tape op als een vaste matrix met one-hot symboolcoderingen en binaire positie-indices.
• Decoder: Volgt autoregressief de berekeningshistorie. Elke stap omvat een pijplijn van:
  1. Overgang: Een feedforward-laag die de TM-overgangsfunctie implementeert via DNF.
  2. Rekenkunde: Een keten van ripple-carry-adders werkt de koppositie bij.
  3. Historie-oproep: Zelf-attention-lagen voeren een binaire zoekopdracht uit over de decoder-historie om de meest recente schrijving op de huidige koppositie te vinden.
  4. Tape-oproep: Cross-attention leest het originele tapesymbool uit de encoder.
  5. Symboolassemblage: Een prioriteit-gebaseerde feedforward-laag selecteert het juiste symbool (laatste schrijving > originele tape > leeg).
• Precisie: Gebruikt binaire positionele codering om fractionele ties in attention-scores te vermijden, waardoor implementatie met eindige precisie (float32) mogelijk is.

3. Architectuur B: SS95 (Recurrent-gebaseerd)

Gebaseerd op Siegelmann en Sontag (1995), reformuleert deze benadering de TM als een stack-machine:

• Codering: Stacks worden gecodeerd als enkele rationale getallen binnen een Cantor-set (met basis $b=4$ en parameter $\rho=1/2$).
• Operaties: Stack-operaties (push, pop, peek) worden gerealiseerd als lineaire of stuksgewijs lineaire functies van de gecodeerde waarde, gemanipuleerd via matrixvermenigvuldigingen en verzadigde lineaire activeringen ($\sigma(x) = \text{clamp}(x, 0, 1)$).
• Implementatie: Twee versies worden geboden:
  • Een expliciete pijplijnversie van 4 lagen.
  • Een "real-time" recurrente versie van 1 laag.
• Precisie: De variant van 1 laag is gevoelig voor afrondingsfouten (versterkt door de basis $b$), wat float64 vereist en het aantal betrouwbare operaties beperkt in vergelijking met de variant van 4 lagen.

Belangrijkste Bijdragen

1. Constructieve Expositie: Een systematische afleiding van hoe ReLU-netwerken Booleaanse schakelingen realiseren, gaande van individuele poorten tot DNF-formules en binaire adders.
2. Uitvoerbare Implementatie: Een compleet PyTorch-pakket dat een TM-beschrijving als invoer neemt en een model uitvoert met gewichten die direct uit de machine-definitie worden gespecificeerd. Er is geen training vereist; het netwerk is "correct door constructie".
3. Open-Source Fundament: De codebase dient als basislijn voor het bestuderen van de stabiliteit van geconstrueerde oplossingen onder verstoring en op basis van gradiënten fine-tuning, waarmee de kloof tussen theoretisch bestaan en praktische optimalisatie wordt overbrugd.

Resultaten en Capaciteiten

Het pakket simuleert succesvol Turing-machines, gedemonstreerd via een evenwichtige haakjeschecker.

• WCM21: Voor een machine met 6 toestanden, 5 symbolen en 100 stappen heeft het model een embedding-breedte van 59. Het opereert met numerieke exactheid in float32, aangezien alle tussenliggende waarden in $\{0, 1\}$ blijven.
• SS95: De versie van 4 lagen is stabiel voor typische invoer. De versie van 1 laag, hoewel dichter bij de originele theoretische constructie, vertoont na ongeveer 8 pop-operaties precisiedegradatie als gevolg van accumulatie van afrondingsfouten in de Cantor-codering.

Betekenis en Aanspraken

Het artikel positioneert zichzelf niet als een voorstel voor nieuwe toepassingen of een claim van superieure prestaties ten opzichte van getrainde modellen, maar als een fundamenteel hulpmiddel voor interpreteerbaarheid en theoretische verificatie.

• Interpreteerbaarheid door Constructie: In tegenstelling tot netwerken die via gradiëntafdalend worden getraind, waar neuronen kunnen worden gepermuteerd of verstrengeld, heeft elke gewicht in deze geconstrueerde netwerken een bekende, interpreteerbare doel (bijvoorbeeld een specifieke poort, een specifiek bit van de adder).
• Overbrugging van Theorie en Praktijk: Het werk sluit de kloof tussen abstracte bewijzen van Turing-volledigheid en uitvoerbare code, en biedt een concrete referentie voor de "symbolisch-neurale brug".
• Toekomstige Nuttigheid: De auteurs suggereren dat de modellen dienen als initialisaties voor het bestuderen van het verlieslandschap rondom geconstrueerde oplossingen, specifiek onderzoekend hoeveel gewichtverstoring de simulatie kan tolereren en of fine-tuning kortere paden oplevert die door de algemene constructie worden gemist.

Het artikel concludeert dat hoewel deze constructies theoretisch sound en praktisch uitvoerbaar zijn, ze de inherente afwegingen benadrukken tussen theoretische Turing-volledigheid en praktische numerieke stabiliteit, met name in de context van rekenen met eindige precisie.