Functorial Neural Architectures from Higher Inductive Types

Dit paper toont aan dat compositional generalisatie in neurale netwerken kan worden gegarandeerd door decoderarchitecturen te construeren als strikte monoidale functors afgeleid van Higher Inductive Types, wat leidt tot aanzienlijk betere prestaties dan bestaande methoden zoals self-attention.

De kern

De Kernboodschap: Waarom AI faalt bij "samenstellen"

Stel je voor dat je een robot hebt die geleerd heeft om één obstakel te omzeilen. Als je hem nu twee obstakels geeft, zou hij dat moeten kunnen door simpelweg het plan voor het eerste obstakel te koppelen aan het plan voor het tweede.

Helaas falen moderne AI-modellen (zoals de grote taalmodellen die we vandaag gebruiken) hier vaak op. Ze zijn geweldig in het leren van patronen, maar slecht in het samenstellen van bekende onderdelen tot iets nieuws. Ze leren het antwoord uit het hoofd, in plaats van de regel te begrijpen.

De auteurs van dit paper zeggen: "Het probleem zit niet in de hersenen van de AI, maar in de bouwplaat."

De Oplossing: Bouwen met wiskundige wetten

De auteurs hebben een nieuwe manier bedacht om neurale netwerken te bouwen. Ze gebruiken een heel geavanceerd stuk wiskunde genaamd Hogere Inductieve Types (HIT).

Laten we dit vergelijken met LEGO:

1. Het oude probleem (De "Attention" methode):
   Stel je voor dat je een LEGO-kasteel bouwt. De huidige AI (zoals een Transformer) kijkt naar alle blokken tegelijk. Als je een nieuwe toren toevoegt, kijkt de AI naar alle blokken in het kasteel om te beslissen hoe de nieuwe toren eruit moet zien.

   • Het probleem: Als je de volgorde van de blokken verandert, raakt de AI in de war. Het ziet de blokken als losse stukjes die met elkaar "praten" (via zogenoemde attention). Het begrijpt niet dat "eerst links, dan rechts" hetzelfde resultaat moet geven als "rechts, dan links" als de volgorde wiskundig niet uitmaakt. Het is te afhankelijk van de specifieke volgorde van de input.

2. De nieuwe methode (De "Functorial" methode):
   De auteurs zeggen: "Laten we de AI dwingen om te werken als een LEGO-robotarm die strikt regels volgt."

   • Ze definiëren eerst de regels van de wereld (bijvoorbeeld: "links en rechts mogen worden verwisseld" of "niet").
   • Dan bouwen ze de AI zo, dat hij per definitie die regels volgt.
   • De AI bouwt het plan voor het eerste obstakel, bouwt het plan voor het tweede, en plakt ze daarna simpelweg aan elkaar.
   • Het resultaat: Omdat de AI de regels van de "bouwplaat" (de wiskunde) al in zijn structuur heeft, kan hij niet anders dan het juiste antwoord geven, zelfs voor situaties die hij nooit eerder heeft gezien.

De Drie Experimenten: Van Torus tot Klein-fles

De auteurs testten hun idee op drie verschillende "werelden" om te zien of het werkte.

1. De Torus (Een donut):

   • De situatie: Hier mag je in elke richting lopen; linksom en rechtsom komen op hetzelfde neer (het is "commutatief").
   • Het resultaat: De nieuwe AI (die de regels volgt) deed het 2 tot 2,7 keer beter dan de oude AI. De oude AI raakte in de war bij lange reeksen, terwijl de nieuwe AI stabiel bleef.

2. De "Wedge of Circles" (Twee ringen die elkaar raken):

   • De situatie: Hier is de volgorde belangrijk. Als je eerst ring A en dan ring B doet, is dat iets anders dan eerst B en dan A.
   • Het resultaat: Hier was het verschil enorm (5,5 tot 10 keer beter). De oude AI verloor de draad volledig; hij wist niet meer welke ring hij moest volgen. De nieuwe AI hield de volgorde perfect bij, omdat zijn bouwplaat dat vereiste.

3. De Klein-fles (Een vreemd oppervlak):

   • De situatie: Dit is het moeilijkste. Hier gebeurt er iets raars: als je een rondje loopt, keer je je om (je "draait" de wereld om).
   • Het resultaat: Alleen de nieuwe AI die een extra "bewijsstuk" (een wiskundige 2-cel) had ingebouwd, kon dit oplossen. De andere AI's maakten een fout van 46%. Dit bewijst dat de AI niet alleen de regels moet volgen, maar ook moet begrijpen hoe die regels elkaar beïnvloeden.

Waarom is dit belangrijk?

Stel je voor dat je een robot wilt die een fabriek bestuurt.

• De oude manier: Je laat de robot duizenden voorbeelden zien van "doe A, doe B". Als je hem nu vraagt "doe C, doe D", faalt hij omdat hij dat specifieke voorbeeld niet heeft gezien.
• De nieuwe manier: Je geeft de robot de wetten van de machine. Je zegt: "Elke beweging is een som van basisbewegingen." De robot bouwt dan zijn eigen "hersenen" zo dat hij niet anders kan dan de wetten te volgen.

Conclusie in één zin

De auteurs hebben bewezen dat je AI's niet kunt laten "leren" om goed samen te stellen door ze meer data te geven; je moet ze architectonisch dwingen om de regels van samenstellen te volgen, net zoals een LEGO-set die alleen maar op één manier kan worden samengebouwd.

Ze hebben zelfs hun theorie bewezen met een computerprogramma (Cubical Agda), zodat we 100% zeker weten dat hun nieuwe AI-ontwerp wiskundig foutloos is, voordat we hem ook maar één keer trainen.

Technische samenvatting

Probleemstelling: Het falen van compositional generalisatie

Neurale netwerken falen systematisch bij compositional generalisatie: het vermogen om correcte outputs te genereren voor nieuwe combinaties van bekende onderdelen (bijvoorbeeld het optellen van 5-cijferige getallen na het leren van 2-cijferige getallen, of het navigeren rond twee obstakels na het leren van één).

• De oorzaak: De auteur betoogt dat dit een architectonisch probleem is, geen beperking in capaciteit of trainingsdata.
• De kern: Compositional generalisatie is wiskundig equivalent aan functorialiteit van de decoder. Een decoder moet een monoidale functor zijn die de algebraïsche structuur van de invoer (woorden/sequentie) behoudt in de uitvoer.
• De beperking van Attention: Het paper stelt dat softmax self-attention (de basis van moderne transformers) fundamenteel niet-functorieel is voor niet-triviale compositional taken, omdat het token-afhankelijke routing gebruikt in plaats van structurele concatenatie. Dit zorgt ervoor dat de output afhankelijk is van de specifieke volgorde van tokens, zelfs als ze dezelfde algebraïsche betekenis hebben.

Methodologie: Van Higher Inductive Types (HIT) naar Neurale Architecturen

De auteur introduceert een compilatieproces dat topologische specificaties vertaalt naar neurale netwerken, waarbij de algebraïsche structuur van de taak de architectuur bepaalt.

1. Theoretisch Kader:

   • Gebruikmakend van Homotopy Type Theory (HoTT) en Higher Inductive Types (HIT) om ruimten te specificeren via generators (punten, lussen) en relaties (2-cellen/homotopieën).
   • De taak wordt gemodelleerd als een groep $G = \pi_1(X)$ (fundamentele groep van een ruimte $X$).
   • Een decoder wordt gedefinieerd als een functor $D: BG \to \mathcal{C}$, waarbij $BG$ de categorie van de groep is en $\mathcal{C}$ een categorie van parametrische kaarten (neurale netwerken).

2. De Compilatiefunctor (Construction 3.2):
   Het paper presenteert een automatische compilatie van HIT-specificaties naar neurale architecturen:

   • Generators: Elke generator van de groep wordt een onafhankelijk neuraal netwerk (generator network) dat een parametrische lus genereert.
   • Samenstelling (Composition): Woorden worden samengesteld door structurele concatenatie (lijst-append) van de output van deze onafhankelijke netwerken. Dit garandeert dat $D(w_1 \cdot w_2) = D(w_1) \oplus D(w_2)$.
   • 2-cellen (Relaties): Voor groepen met relaties (zoals $ab = ba$ of $bab^{-1} = a^{-1}$) wordt een geleerde homotopie (een extra MLP) toegevoegd die de continuïteit tussen verschillende paden voor dezelfde groepselementen waarborgt.

3. Type-A vs. Type-B Architecturen:

   • Type-B (Functorieel): Architecturen die structureel concateneren van onafhankelijk gegenereerde segmenten. Ze zijn per constructie monoidale functors.
   • Type-A (Niet-functorieel): Architecturen die cross-segment informatie stroming toestaan (zoals attention of RNNs). Deze breken de monoidale factorisatie.

4. Formalisatie:
   De belangrijkste stellingen (dat transport-decoders functorieel zijn en attention niet) zijn formeel bewezen in Cubical Agda, een bewijshulpmiddel voor homotopietype-theorie. Dit biedt "verified machine learning": de architectuur garandeert de eigenschappen voor alle parameterwaarden, niet alleen voor getrainde weights.

Belangrijkste Bijdragen

1. Compilatiefunctor: Een methode om HIT-specificaties direct te vertalen naar neurale architecturen met gegarandeerde compositional correctheid.
2. Onmogelijkheidsresultaat: Een formeel bewijs (Theorem 4.1) dat softmax attention nooit een monoidale functor kan zijn voor niet-triviale groepen, ongeacht de parameters.
3. Verified ML Pipeline: Een workflow van "Specificatie $\to$ Verificatie (Agda) $\to$ Compilatie $\to$ Training", waarbij de topologische garanties vastzitten in de architectuur en niet kunnen worden verbroken door training.
4. Type-A/B Distinctie: Een scherp theoretisch en empirisch onderscheid tussen architecturen die compositionaliteit leren (vaak falend) en architecturen die compositionaliteit garanderen (door constructie).

Resultaten: Experimenten op Drie Ruimtes

De auteurs testten hun theorie op drie topologische ruimtes met toenemende complexiteit:

1. Torus ($T^2$, $\pi_1 = \mathbb{Z}^2$, Abels):

   • Resultaat: Type-B decoders (Transport) presteerden 2–2.7x beter dan Type-A decoders (Transformer, Cover) bij extrapolatie naar langere woorden (lengte 10).
   • Observatie: Zelfs met meer parameters faalde de Transformer door cross-segment mixing.

2. Wedge of Circles ($S^1 \vee S^1$, $\pi_1 = F_2$, Niet-abels, Vrij):

   • Resultaat: Het prestatieverschil explodeerde tot 5.5–10x.
   • Observatie: De Transformer kon de niet-abelse structuur niet behouden; de volgorde van letters ($ab$ vs $ba$) werd genegeerd, wat leidde tot topologisch zinloze outputs. De Transport-decoder behield 100% nauwkeurigheid.

3. Klein Bottle ($K$, $\pi_1 = \mathbb{Z} \rtimes \mathbb{Z}$, Niet-abels met relatie):

   • Resultaat: Dit testte het niveau van de geleerde 2-cel (bewijsstap).
   • Observatie: Voor woorden die de groeprelatie $bab^{-1} = a^{-1}$ gebruiken, sloot de "Homotopy" decoder (Type-B met geleerde 2-cel) een 46% foutenmarge in vergelijking met de standaard Transport-decoder. Dit bewijst dat het leren van de homotopie (de "bewijsstap") essentieel is voor complexe relaties.

Algemene Trend: Type-B decoders vertonen een constante fout per segment naarmate de woordlengte toeneemt ($O(1)$), terwijl Type-A decoders degradatie vertonen ($\Omega(1)$) door out-of-distribution patronen in attention.

Betekenis en Conclusie

Dit paper biedt een fundamentele verschuiving in hoe we neurale architecturen voor compositional taken ontwerpen:

• Van "Leren" naar "Garanderen": In plaats van te hopen dat een netwerk de samenstellingsregels leert, worden deze regels ingebouwd in de architectuur via type-theoretische specificaties.
• Attention als Beperking: Het paper levert een sterk theoretisch argument waarom attention-mechanismen inherent ongeschikt zijn voor strikte compositional generalisatie in niet-triviale algebraïsche structuren.
• Toepasbaarheid: De aanpak is direct toepasbaar op domeinen met modulaire structuur, zoals robotica (obstakelplanning), programmeertalen en moleculaire systemen.
• Verified AI: Het is een van de eerste voorbeelden waarbij machine-geverifieerde bewijzen (via Cubical Agda) worden gebruikt om gegarandeerde generalisatie-eigenschappen voor neurale netwerken te bieden.

Kortom, de auteurs tonen aan dat compositional generalisatie geen kwestie is van meer data of grotere modellen, maar van de juiste functoriële architectuur, die automatisch kan worden gegenereerd uit de wiskundige specificatie van de taak.