A homotopy-type-theoretic generalization of neurosymbolic inference

Technische Samenvatting: Een Homotopie-Type-Theoretische Generalisatie van Neurosymbolische Inferentie

Probleemstelling
Huidige neurosymbolische (NeSy) systemen vertrouwen grotendeels op een verenigde functionaal die gedefinieerd wordt als een geloofsgewogen som van een logische kwantiteit over een ruimte van $\sigma$-structuren (toewijzingen van waarden aan logische symbolen). Deze functionaal, vaak geïnstantieerd als gewogen modeltelling (WMC), probabilistische logica of fuzzy logica, opereert op verzamelingen. De auteurs stellen dat verzamelingen "bewust vergeetachtige" objecten zijn die twee cruciale stukken informatie weggooien die essentieel zijn voor gestructureerde NeSy:

1. Symmetrie: Ze maken geen onderscheid tussen $\sigma$-structuren die identiek zijn tot een symmetrie van de theorie (bijv. het verwisselen van uitwisselbare individuen). Bijgevolg telt de standaardfunctionaal symmetrische structuren over.
2. Bewijs-multipliciteit: Ze reduceren meerdere verschillende afleidingen die een query bewerkstelligen tot één enkel getal, waarbij genegeerd wordt "op hoeveel manieren" een feit bewezen is.

Deze decategorificatie leidt tot een specifieke foutmodus die bekend staat als redeneer-shortcuts (redeneringsafkortingen). Wanneer een model alleen getraind wordt op logische outputs, kan het convergeren naar een perceptie die de verkeerde betekenis toekent aan latente concepten (een "shortcut") terwijl de output behouden blijft. Standaardmethoden worstelen om de correcte "shortcut-bewuste" posterior (een uniforme distributie over de verwarringsset van equivalente concepten) te identificeren zonder terug te vallen op complexe ensembling of expressieve dichtheidschatting.

Methodologie
Het artikel stelt voor om de onderliggende verzamelingen van NeSy-inferentie te vervangen door types uit de Homotopie Type Theorie (HoTT). In dit kader onthoudt een type niet alleen zijn elementen, maar ook de manieren waarop elementen geïdentificeerd kunnen worden (isomorfismen).

De auteurs "verheffen" de vier ingrediënten van de standaard NeSy-functionaal (Vergelijking 1) één niveau omhoog:

1. Structuurruimte ($\Omega$): Vervangen door een type waarin identiteitstypes symmetrieën vastleggen (hernoemingen van individuen). De klassieke verzameling van structuren is het 0-getrunceerde geval.
2. Logische Functie ($\ell$): Vervangen door een bewijsfamilie $P: \Omega \to \mathcal{U}$. Het truncatieniveau van $P$ is een ontwerp-parameter: een propositie (niveau -1) controleert verzadiging; een verzameling (niveau 0) telt afleidingen; een groïde (niveau 1) identificeert symmetrische afleidingen.
3. Inferentie: Vervangen door geloofsgewogen homotopie-cardinaliteit. In plaats van een eenvoudige som, wordt de inferentiewaarde berekend als:
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   Dit telt elk element, gewogen door de reciproque van de grootte van zijn symmetriegroep ($1/|Aut(x)|$), wat ervoor zorgt dat symmetrische structuren minder bijdragen dan asymmetrische structuren.
4. Waardering: De keuze van de commutatieve semiring (bijv. $(+, \times)$ voor waarschijnlijkheid, $(\max, +)$ voor tropisch) bepaalt welk numeriek invariant wordt afgelezen uit de homotopie-cardinaliteit.

Belangrijkste Bijdragen

1. Theoretisch Kader: De auteurs formaliseren NeSy-inferentie als een geloofsgewogen homotopie-cardinaliteit. Dit kader introduceert twee expliciete parameters die afwezig zijn in klassieke formuleringen: een symmetrieparameter (die de groep van toegestane hernoemingen definieert) en een truncatieniveau (dat de granulariteit van bewijsregistratie definieert).
2. Conservativiteitstheorema: Een door een machine gecontroleerd theorema (geverifieerd in Lean 4) bewijst dat wanneer symmetrieën triviaal zijn (de groep is de identiteit) of de semiring idempotent is, de homotopie-cardinaliteit exact convergeert naar de klassieke verzameling-gebaseerde functionaal. Dit garandeert dat het nieuwe kader een getrouwe generalisatie is.
3. Redeneer-shortcuts als Banen: Het artikel identificeert de "verwarringsset" (de verzameling concept-toewijzingen die dezelfde output opleveren) als een baan (orbit) onder de symmetriegroep van de theorie.
   • De "shortcut-bewuste" concept-posterior wordt geïdentificeerd als het unieke symmetrie-invariante punt: de uniforme distributie over de baan.
   • Dit leidt tot baan-averaging (orbit-averaging), een gesloten vorm methode om deze posterior te berekenen:
     $$\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$$
   • Deze methode symmetriseert een enkele basismodel over de output-behoudende groep $G$ zonder dat daarvoor ensembling of dichtheidschatting nodig is.
4. Genererende Functies: Voor uitwisselbare modellen levert het kader van nature exponentiële genererende functies op (via homotopie-cardinaliteit), in plaats van gewone genererende functies, wat aansluit bij de theorie van combinatorische soorten (combinatorial species).

Experimentele Resultaten
De auteurs evalueerden de baan-averaging methode op MNIST reasoning-shortcut benchmarks (specifiek taken met bekende symmetriegroepen en grondwaarheid voor concept-identificeerbaarheid).

• Opzet: Een enkel neuraal netwerk werd getraind om samengevoegde labels te voorspellen. De taak was het onderscheiden van identificeerbare cijfers (baan grootte 1) en verwarbare cijfers (baan grootte > 1).
• Vergelijking: Een single-model baan-averaging wrapper werd vergeleken met een basismodel en een diversiteit-getrainde 5-model ensemble (Bears).
• Bevindingen:
  • Het basismodel was overmoedig op verwarbare cijfers (hoge Expected Calibration Error, ECE).
  • Baan-averaging verminderde de ECE op verwarbare cijfers van 0.614 naar 0.010 terwijl de label-accuratesse behouden bleef en de kalibratie van identificeerbare concepten intact bleef.
  • Het diversiteit-getrainde ensemble bereikte vergelijkbare kalibratieverbeteringen alleen door label-accuratesse op te offeren of de kalibratie van identificeerbare concepten te verstoren, wat de trade-off benadrukt die het single-model baan-averaging vermijdt.

Betekenis en Claims
Het artikel claimt dat het lezen van NeSy-inferentie door de lens van de HoTT een "concreet rendement" biedt door de symmetriestructuur bloot te leggen die verantwoordelijk is voor redeneer-shortcuts.

• Theoretische Unificatie: Het verenigt diverse NeSy-benaderingen (probabilistisch, fuzzy, provenance) onder een enkele decategorifieerde kijk op een rijker, gestructureerd object.
• Praktische Efficiëntie: Het demonstreert dat de "shortcut-bewuste" posterior, die voorheen werd geacht dure ensembling te vereisen, in gesloten vorm berekend kan worden door een enkel model te middelen over de symmetriegroep.
• Kalibratie: De methode verbetert de kalibratie op onidentificeerbare concepten zonder de prestaties op identificeerbare concepten te verslechteren, waarmee een specifiek faalmechanisme van NeSy-leren wordt opgelost.
• Beperkingen: De auteurs merken op dat het huidige kader steunt op eindige types ($\pi$-finiteness). Het uitbreiden van homotopie-cardinaliteit naar continue domeinen via "cohesie" blijft een openstaand probleem.

Het werk wordt gepresenteerd als een fundamentele verschuiving van verzameling-gebaseerd naar type-gebaseerd redeneren, waarbij de "vergetelheid" van verzamelingen wordt vervangen door het structurele geheugen van types, wat direct de kernoorzaken van redeneer-shortcuts aanpakt.