🤖 AI

A homotopy-type-theoretic generalization of neurosymbolic inference

Dieses Paper schlägt ein Framework der Homotopietypentheorie für neurosymbolische Inferenz vor, das traditionelle mengenbasierte Ansätze verallgemeinert, um strukturelle Symmetrien und Beweismultiplizitäten zu berücksichtigen, wodurch Reasoning-Shortcuts aufgelöst und die Kalibrierung durch eine symmetrieinvariante, geschlossene Mittelungsmethode verbessert wird.

Ursprüngliche Autoren: Fernando Zhapa-Camacho, Robert Hoehndorf

Veröffentlicht 2026-06-17

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Fernando Zhapa-Camacho, Robert Hoehndorf

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie versuchen, einem Computer beizubringen, ein logisches Rätsel zu verstehen, wie etwa ein Detektiv, der ein Geheimnis löst. Der Computer hat zwei Teile: einen „neuronalen“ Teil, der Wahrscheinlichkeiten schätzt (wie „Ich glaube, der Butler war es mit 70 % Zuversicht“), und einen „symbolischen“ Teil, der die Regeln der Logik kennt (wie „Der Butler kann nur der Mörder sein, wenn er in der Bibliothek war“).

Normalerweise, wenn diese beiden Teile zusammenarbeiten, macht der Computer einen Fehler, den man eine „Reasoning Shortcut“ (Denk-Abkürzung) nennt.

Das Problem: Die „Spiegel“-Falle

Stellen Sie sich einen Raum mit zwei identischen Zwillingen vor, Alice und Bob. Der Computer wird gefragt: „Ist jemand im Raum?“

Szenario A: Alice ist da, Bob ist nicht.
Szenario B: Bob ist da, Alice ist nicht.

Nach der Logik des Computers sind dies zwei verschiedene Antworten. Aber nach den Regeln des Spiels ist dies exakt dieselbe Situation, da Alice und Bob austauschbar sind. Der Computer weiß nicht, dass sie austauschbar sind, und behandelt dies als zwei verschiedene, distinkte Möglichkeiten. Er könnte verwirrt sein und denken: „Oh, es gibt zwei Wege, wie das passieren kann, also sollte ich sehr sicher sein“, oder er wählt einen der Zwillinge willkürlich aus und ignoriert den anderen.

Dies ist die „Abkürzung“: Der Computer lernt, die richtige Antwort aus dem falschen Grund zu erraten, indem er sich an ein spezifisches Detail klammert (wie „Alice“), das eigentlich gar nicht wichtig ist, sondern nur deshalb gewählt wurde, weil er dieses Detail während des Trainings gesehen hat.

Die Lösung: Eine neue Art zu zählen

Die Autoren dieses Papers schlagen eine mathematische Aufwertung vor. Anstatt die Welt des Computers als eine einfache Liste von Objekten (eine „Menge“) zu betrachten, behandeln sie sie als eine Karte von Verbindungen (einen „Typ“ aus der Homotopietheorie).

Hier ist die Analogie:

Der alte Weg (Mengen): Stellen Sie sich vor, Sie zählen Menschen in einem Raum. Sie sehen Alice und Bob. Sie zählen „1, 2“. Es ist Ihnen egal, ob sie sich ähnlich sehen oder ob das Vertauschen von Alice und Bob die Atmosphäre im Raum verändert. Sie zählen einfach Köpfe.
Der neue Weg (Typen/Homotopie): Stellen Sie sich vor, Sie zählen Menschen, aber Sie besitzen auch ein „Symmetrie-Messgerät“. Wenn Alice und Bob identische Zwillinge sind, erkennt das Messgerät, dass das Vertauschen von ihnen keine neue Situation schafft; es ist dieselbe Situation, nur aus einem anderen Blickwinkel betrachtet.
- In dieser neuen Mathematik zählt eine Situation mit viel Symmetrie (wie die Zwillinge) weniger als eine Situation ohne Symmetrie. Es ist so, als würde man sagen: „Weil es zwei Möglichkeiten gibt, diese Zwillinge anzuordnen, zählt diese spezifische Anordnung nur als ein halber Mensch.“

Diese neue Methode wird Belief-Weighted Homotopy Cardinality genannt. Das ist eine schicke Art zu sagen: „Zähle die Möglichkeiten, aber gib einer Möglichkeit einen Rabatt, wenn sie nur ein Spiegelbild einer anderen ist.“

Der magische Trick: Orbit-Averaging

Das Paper zeigt, dass man durch die Verwendung dieser neuen Mathematik das Problem der „Reasoning Shortcut“ lösen kann, ohne eine ganze Armee von verschiedenen Computern (Ensembles) oder komplexe Dichtemodelle trainieren zu müssen.

Sie führen eine Technik namens Orbit-Averaging ein.

Die Analogie: Stellen Sie sich vor, Sie haben ein unscharfes Foto eines Gesichts. Anstatt zu versuchen zu erraten, welche spezifische Person es ist, nehmen Sie das Foto, drehen es in jeder möglichen Weise, die gleich aussieht (die Zwillinge rotierend), und bilden den Durchschnitt aus all diesen Ansichten.
Das Ergebnis: Der Computer hört auf zu raten: „Es ist Alice!“ oder „Es ist Bob!“ und sagt stattdessen: „Es ist einer der Zwillinge, und ich bin mir über beide gleichermaßen unsicher.“ Er wird kalibriert. Er weiß, wann er rät und wann er sich sicher ist.

Was sie herausgefunden haben

Die Autoren testeten dies bei einer Aufgabe, bei der der Computer Zahlen (0–9) erkennen musste, aber angewiesen wurde, sie zu gruppieren (z. B. sind 1 und 2 dieselbe Kategorie).

Der alte Computer: Bekam die Gruppe richtig, war sich aber bezüglich der spezifischen Ziffer (1 oder 2) zu sicher, obwohl er sie nicht unterscheiden konnte.
Der neue Computer (Orbit-Averaging): Bekam die Gruppe richtig, behielt die gleiche Genauigkeit bei, gab aber korrekt zu: „Ich kann 1 von 2 nicht unterscheiden, also bin ich 50/50.“

Warum das wichtig ist

Es ist ein einzelnes Modell: Sie müssen nicht fünf verschiedene Versionen der KI trainieren und kombinieren (was langsam und teuer ist). Sie können eine einzige Modell nehmen und dieses mathematische „Filter“-Verfahren anwenden, um seine Zuversicht zu korrigieren.
Es ist exakt: Die Mathematik beweist, dass diese Methode der einzige Weg ist, um perfekt fair zu sein, wenn Dinge symmetrisch sind.
Es ist allgemein gültig: Dies funktioniert für jedes Logiksystem, in dem Dinge vertauscht werden können, ohne das Ergebnis zu verändern, nicht nur für die spezifischen Beispiele mit den Ziffern, die sie getestet haben.

Kurz gesagt, das Paper sagt: „Hört auf, Möglichkeiten wie eine einfache Liste zu zählen. Fangt an, sie wie einen symmetrischen Tanz zu zählen, bei dem das Vertauschen der Partner den Tanz nicht verändert. Wenn ihr das tut, wird eure KI aufhören, euch über ihre Sicherheit zu belügen.“

Technische Zusammenfassung: Eine homotopietheoretische Verallgemeinerung der neurosymbolischen Inferenz

Problemstellung
Aktuelle neurosymbolische (NeSy) Systeme verlassen sich weitgehend auf ein vereinheitlichtes Funktional, das als glaubensgewichtete Summe einer logischen Größe über einem Raum von $\sigma$ -Strukturen (Zuweisungen von Werten zu logischen Symbolen) definiert ist. Dieses Funktional, das oft als gewichtete Modellzählung (WMC), probabilistische Logik oder Fuzzy-Logik instanziiert wird, operiert auf Mengen. Die Autoren argumentieren, dass Mengen „bewusst vergessliche“ Objekte sind, die zwei kritische Informationen verwerfen, die für strukturierte NeSy-Inferenz essenziell sind:

Symmetrie: Sie unterscheiden nicht zwischen $\sigma$ -Strukturen, die bis auf eine Symmetrie der Theorie identisch sind (z. B. das Vertauschen austauschbarer Individuen). Folglich zählt das Standardfunktional symmetrische Strukturen über.
Beweismultiplizität: Sie kollabieren mehrere distinkte Ableitungen, die eine Anfrage bezeugen, zu einer einzigen Zahl und ignorieren dabei die Information „auf wie viele Arten“ ein Faktum bewiesen wird.

Diese Dekategorisierung führt zu einem spezifischen Fehlermodus, der als Reasoning Shortcut (Abkürzungs-Schlussfolgerung) bekannt ist. Wenn ein Modell nur auf logischen Ausgaben trainiert wird, kann es zu einer Wahrnehmung konvergieren, die den falschen Sinn für latente Konzepte zuweist (einen „Shortcut“), während die Ausgabe erhalten bleibt. Standardmethoden haben Schwierigkeiten, den korrekten „Shortcut-bewussten“ Posterior (eine Gleichverteilung über die Konfusionsmenge äquivalenter Konzepte) zu identifizieren, ohne auf komplexes Ensembling oder expressive Dichteschätzung zurückzugreifen.

Methodik
Der Artikel schlägt vor, die zugrunde liegenden Mengen der NeSy-Inferenz durch Typen aus der Homotopietheorie (HoTT) zu ersetzen. In diesem Rahmen erinnert ein Typ nicht nur an seine Elemente, sondern auch an die Wege, auf denen Elemente identifiziert werden können (Isomorphismen).

Die Autoren „heben“ die vier Bestandteile des Standard-NeSy-Funktionals (Gleichung 1) um eine Ebene nach oben:

Strukturraum ( $\Omega$ ): Ersetzt durch einen Typ, in dem Identitätstypen Symmetrien (Umbenennungen von Individuen) aufzeichnen. Der klassische Satz von Strukturen ist der 0-trunkierte Fall.
Logikfunktion ( $\ell$ ): Ersetzt durch eine Beweisfamilie $P: \Omega \to \mathcal{U}$ . Das Truncation-Level von $P$ ist ein Designparameter: Eine Proposition (Level -1) prüft die Erfüllbarkeit; ein Set (Level 0) zählt Ableitungen; ein Groupoid (Level 1) identifiziert symmetrische Ableitungen.
Inferenz: Ersetzt durch glaubensgewichtete Homotopie-Kardinalität. Anstatt einer einfachen Summe wird der Inferenzwert als:
$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$
berechnet. Dies zählt jedes Element gewichtet durch den Kehrwert der Größe seiner Symmetriegruppe ($1/|Aut(x)|), wodurch sichergestellt wird, dass symmetrische Strukturen weniger stark beitragen als asymmetrische.
Bewertung: Die Wahl des kommutativen Semirings (z. B. $(+, \times)$ für Wahrscheinlichkeit, $(\max, +)$ für tropisch) bestimmt, welches numerische Invariant aus der Homotopie-Kardinalität abgelesen wird.

Kernbeiträge

Theoretischer Rahmen: Die Autoren formalisieren die NeSy-Inferenz als glaubensgewichtete Homotopie-Kardinalität. Dieser Rahmen führt zwei explizite Parameter ein, die in klassischen Formulierungen fehlen: einen Symmetrieparameter (definiert die Gruppe der erlaubten Umbenennungen) und ein Truncation-Level (definiert die Granularität der Beweisverfolgung).
Konservativitäts-Theorem: Ein maschinell verifiziertes Theorem (verifiziert in Lean 4) beweist, dass wenn Symmetrien trivial sind (die Gruppe ist die Identität) oder der Semiring idempotent ist, die Homotopie-Kardinalität exakt zum klassischen mengenbasierten Funktional kollabiert. Dies stellt sicher, dass der neue Rahmen eine treue Verallgemeinerung ist.
Reasoning Shortcuts als Orbits: Der Artikel identifiziert die „Konfusionsmenge“ (die Menge der Konzeptzuweisungen, die dieselbe Ausgabe liefern) als einen Orbit unter der Symmetriegruppe der Theorie.
- Der „Shortcut-bewusste“ Konzept-Posterior wird als der eindeutige symmetrie-invariante Punkt identifiziert: die Gleichverteilung über den Orbit.
- Dies führt zum Orbit-Averaging, einer geschlossenen Methode zur Berechnung dieses Posteriors:
  $\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$
- Diese Methode symmetrisiert ein einzelnes Basismodell über die ausgabenerhaltende Gruppe $G$ , ohne ein Ensemble oder Dichteschätzung zu erfordern.
Generierende Funktionen: Für austauschbare Modelle liefert der Rahmen natürlicherweise exponentielle erzeugende Funktionen (via Homotopie-Kardinalität) anstelle von gewöhnlichen erzeugenden Funktionen, was mit der Theorie der kombinatorischen Spezies übereinstimmt.

Experimentelle Ergebnisse
Die Autoren evaluierten die Orbit-Averaging-Methode an MNIST-Reasoning-Shortcut-Benchmarks (speziell Aufgaben mit bekannten Symmetriegruppen und Ground-Truth für Konzept-Identifizierbarkeit).

Setup: Ein einzelnes neuronales Netz wurde trainiert, um gemergte Labels vorherzusagen. Die Aufgabe bestand darin, zwischen identifizierbaren Ziffern (Orbitgröße 1) und konfusiblen Ziffern (Orbitgröße > 1) zu unterscheiden.
Vergleich: Ein einzelnes Modell mit Orbit-Averaging-Wrapper wurde mit einem Basismodell und einem Diversitäts-trainierten 5-Modell-Ensemble (Bears) verglichen.
Ergebnisse:
- Das Basismodell war bei konfusiblen Ziffern überkonfident (hoher Expected Calibration Error, ECE).
- Orbit-Averaging reduzierte den ECE bei konfusiblen Ziffern von 0,614 auf 0,010, während die Label-Genauigkeit sowie die Kalibrierung identifizierbarer Konzepte erhalten blieb.
- Das Diversitäts-trainierte Ensemble erreichte ähnliche Kalibrierungsverbesserungen nur durch das Opfern der Label-Genauigkeit oder die Fehlkalibrierung identifizierbarer Konzepte, was den Trade-off verdeutlicht, den das Einzelmodell-Orbit-Averaging vermeidet.

Bedeutung und Ansprüche
Der Artikel behauptet, dass das Lesen der NeSy-Inferenz durch die Linse der HoTT einen „konkreten Ertrag“ liefert, indem sie die Symmetriestruktur offenlegt, die für Reasoning Shortcuts verantwortlich ist.

Theoretische Vereinheitlichung: Es vereinheitlicht verschiedene NeSy-Ansätze (probabilistisch, fuzzy, Provenance) unter einer einzigen dekatigorisierten Sicht auf ein reicheres, strukturiertes Objekt.
Praktische Effizienz: Es zeigt, dass der „Shortcut-bewusste“ Posterior, der zuvor als teures Ensembling galt, in geschlossener Form durch Mittelung eines einzelnen Modells über die Symmetriegruppe berechnet werden kann.
Kalibrierung: Die Methode verbessert die Kalibrierung auf unidentifizierbaren Konzepten, ohne die Leistung bei identifizierbaren Konzepten zu verschlechtern, und löst damit einen spezifischen Fehlermodus des NeSy-Learnings.
Limitierungen: Die Autoren merken an, dass der aktuelle Rahmen auf endliche Typen ( $\pi$ -Finitheit) angewiesen ist. Die Erweiterung der Homotopie-Kardinalität auf kontinuierliche Domänen via „Kohäsion“ bleibt ein offenes Problem.

Die Arbeit präsentiert sich als fundamentaler Wechsel vom mengenbasierten zum typenbasierten Denken, wobei das „Vergessen“ von Mengen durch das strukturelle Gedächtnis von Typen ersetzt wird, was die Ursachen von Reasoning Shortcuts direkt adressiert.