Technische Samenvatting: Transformers zijn inherent beknopt

Probleemstelling

Het artikel onderzoekt de beknoptheid van Transformers met vaste precisie als maatstaf voor hun expressieve kracht, onderscheiden van de traditionele vraag welke talen ze kunnen herkennen. Hoewel recente theoretisch werk heeft vastgesteld dat Transformers met vaste precisie specifieke subclasses van reguliere talen herkennen (specifiek ster-vrije talen), betoogt dit artikel dat expressieve capaciteit alleen een onvoldoende lens is voor vergelijking.

Het kernprobleem dat wordt aangepakt is de groottekloof tussen Transformers en andere formalismen (Lineaire Temporele Logica, Recurrente Neuronale Netwerken en Eindige Automaten) bij het beschrijven van dezelfde taal. Specifiek vragen de auteurs: Kunnen Transformers bepaalde talen beschrijven met aanzienlijk minder parameters (symbolen) dan deze alternatieve modellen? Verder, wat zijn de computationele gevolgen van deze beknoptheid voor verificatietaken zoals leegte- en equivalentiecontrole?

Methodologie

De auteurs hanteren een aanpak gebaseerd op formele taaltheorie en complexiteitstheorie, waarbij de volgende modellen en technieken worden gebruikt:

1. Formele Modellen:

   • Unieke-Hard Attention Transformers (UHAT): Een vereenvoudigde, veelgebruikte abstractie van self-attention mechanismen. De studie richt zich op rekenen met vaste precisie (rationele getallen), wat de realiteit van hardware-implementaties nabootst.
   • Booleaanse RASP (B-RASP): Een programmeertaal waarvan is bewezen dat deze expressief equivalent is aan UHAT's, gebruikt als tussenstap voor het construeren van bewijzen.
   • Lineaire Temporele Logica (LTL) en Eindige Automaten: Standaard benchmarks voor beknoptheidsvergelijkingen.
   • Recurrente Neuronale Netwerken (RNN's): Gemodelleerd als machines met vaste precisie, waarvan is aangetoond dat ze qua omvang van de toestandsruimte equivalent zijn aan eindige automaten.

2. Belangrijkste Technische Constructie:

   • Dubbel Exponentiële Telling: De centrale technische innovatie is het aantonen dat Transformers tellers kunnen implementeren variërend van $0$ tot $2^{2^N}$ door middel van een subtiel codering via attention-mechanismen. Dit wordt bereikt door constraints te stapelen die het model in staat stellen sequenties te verifiëren waarbij het kortst mogelijke geaccepteerde woord een dubbel exponentiële lengte heeft ten opzichte van de modelgrootte.
   • Reductie vanuit Tegelpuzzelproblemen: Om ondergrenzen voor beknoptheid en hardheid te bewijzen, reduceren de auteurs het $2^N$-tegelpuzzelprobleem (een EXPSPACE-volledig probleem) tot het niet-leegteprobleem van B-RASP-programma's en UHAT's. Ze construeren programma's van polynomiale grootte die coderingen van geldige tegelpuzzels accepteren, waarbij de geldige tegelpuzzels corresponderen met uitvoeringssporen van exponentiële lengte.

3. Vertaling en Bovengrenzen:

   • De auteurs bieden een constructieve vertaling van UHAT's met vaste precisie naar LTL-formules. Cruciaal bewijzen ze dat de rationele waarden die tijdens de uitvoering van een Transformer worden berekend, slechts polynomiaal veel bits vereisen (Propositie 12). Dit maakt het mogelijk om de verzameling mogelijke tussenliggende toestanden in exponentiële tijd te enumereren, wat een vertaling naar een LTL-formule van exponentiële grootte mogelijk maakt, een verbetering ten opzichte van eerdere dubbel exponentiële grenzen.

Belangrijkste Bijdragen en Resultaten

1. Beknoptheidshiërarchieën

Het artikel vestigt strikte beknoptheidskloven tussen Transformers en andere formalismen:

• Transformers versus LTL en RNN's: Transformers zijn exponentieel beknopter dan zowel Lineaire Temporele Logica als Recurrente Neuronale Netwerken. Er bestaan families van talen die door Transformers van polynomiale grootte herkend kunnen worden, maar die exponentieel grotere LTL-formules of RNN's vereisen.
• Transformers versus Eindige Automaten: Transformers zijn dubbel exponentieel beknopter dan eindige automaten. Er bestaan families van talen die door Transformers van polynomiale grootte beschreven kunnen worden, waarvan de kleinste equivalente eindige automaat dubbel exponentieel groot is.
• Overeenkomende Bovengrenzen: De auteurs bewijzen dat elke Transformer met vaste precisie kan worden omgezet in een LTL-formule met ten hoogste een exponentiële toename in grootte. Bijgevolg kan elke Transformer worden omgezet in een eindige automaat met een dubbel exponentiële toename. Dit vestigt dat de beknoptheidskloven strak zijn (tot op polynomiale factoren).

2. Complexiteit van Verificatie

Als direct gevolg van de vastgestelde beknoptheid bewijst het artikel dat basisverificatieproblemen voor Transformers computationeel onberekenbaar zijn:

• Niet-Leegte: Het probleem om te bepalen of een gegeven UHAT een niet-lege taal herkend, is EXPSPACE-volledig.
• Equivalentie: Het probleem om te beslissen of twee UHAT's dezelfde taal herkennen, is EXPSPACE-volledig.
• Implicatie: Onder standaard complexiteitsaannames kan geen enkel algoritme deze problemen oplossen in minder dan dubbel exponentiële tijd. Dit staat in schril contrast met eindige automaten, waarbij deze problemen in polynomiale tijd oplosbaar zijn.

3. Precisie en Realisme

De resultaten gelden onder rekenen met vaste precisie (rationele getallen met een constant aantal bits), wat volgens de auteurs de setting is die het meest trouw is aan realistische hardware. Dit onderscheidt het werk van modellen die oneindige precisie veronderstellen, wat vaak tot andere expressiviteitsresultaten leidt.

Betekenis en Aanspraken

Het artikel beweert dat beknoptheid een kritieke, tot nu toe onderbelichte dimensie is van Transformer-expressiviteit. De auteurs betogen dat hoewel Transformers mogelijk dezelfde klasse van talen herkennen (ster-vrij) als LTL of teller-vrije automaten, hun vermogen om deze talen compact te beschrijven veruit superieur is.

De betekenis van deze bevinding is tweeledig:

1. Theoretisch Inzicht: Het verfijnt het begrip van Transformer-capaciteiten, en toont aan dat hun "kracht" niet alleen ligt in wat ze kunnen herkennen, maar in hoe efficiënt ze complexe structurele afhankelijkheden kunnen coderen (specifiek, dubbel exponentiële telling) die andere modellen niet kunnen comprimeren.
2. Verificatiegrenzen: De EXPSPACE-volledigheid van verificatieproblemen dient als een formele verklaring voor de praktische moeilijkheid van het verifiëren van Transformers. Het artikel stelt dat de compactheid van Transformers elke besluitprocedure dwingt om een enorme hoeveelheid onderliggende structuur te "ontvouwen", waardoor formele verificatie inherent moeilijker is voor Transformers dan voor eindige automaten of LTL.

De auteurs concluderen dat hun resultaten een eerste stap vormen naar het begrijpen van de relatieve beknoptheid van Transformers ten opzichte van andere taalacceptor-modellen, terwijl ze opmerken dat de leerbaarheid van dergelijke beknopte representaties een open empirische vraag blijft.