🤖 AI

A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus

Diese Arbeit präsentiert die erste maschinell geprüfte Formalisierung von Topos-kausalen Modellen in Cubical Agda, welche Kernkonzepte wie Intervention als charakteristische Abbildungen und Sheaf-Gluing verifiziert, während sie eine Lücke in den Lawvere-Tierney-Axiomen identifiziert und behebt, um die Stabilität von Pearls Regeln zu etablieren, sowie eine Kontextualitäts-Obstruktion innerhalb eines sicheren, axiomenfreien Rahmens demonstriert.

Ursprüngliche Autoren: Karen Sargsyan

Veröffentlicht 2026-07-20

📖 7 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Karen Sargsyan

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

Das Dilemma des Detektivs: Warum Kausalität eine neue Landkarte braucht

Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, ein Rätsel zu lösen. Sie haben eine Liste von Hinweisen: „Es hat geregnet“, „Das Gras ist nass“ und „Die Sprinkleranlage war an“. In der Vergangenheit behandelten Wissenschaftler diese Hinweise wie eine einfache Liste von Fakten. Wenn das Gras nass ist, könnten sie vermuten, dass es geregnet hat. Aber das echte Leben ist chaotischer. Was, wenn Sie das Gras nass gemacht haben, indem Sie die Sprinkleranlage eingeschaltet haben? Ändert das die Tatsache, dass es geregnet hat? Dies ist das Herz der kausalen Inferenz: herauszufinden, nicht nur, was zusammen auftritt, sondern was was verursacht, besonders wenn wir intervenieren und die Regeln des Spiels ändern.

Seit Jahrzehnten nutzen Experten Diagramme und Mathematik, um diese Ursache-Wirkungs-Ketten nachzuverfolgen. Doch vor kurzem entstand eine neue Idee: Was wäre, wenn wir die gesamte Welt der Ursachen nicht als statisches Bild betrachten, sondern als eine sich verschiebende Landschaft, die sich ändert, je nachdem, von wo aus man sie betrachtet? Dies ist der Bereich der Topos-Theorie, ein Zweig der Mathematik, der untersucht, wie Formen und Strukturen zusammenpassen. Denken Sie an eine universelle Sprache zum „Verkleben“ von Informationsteilen. Wenn Sie ein Puzzle haben, bei dem die Teile in Ihren Händen perfekt passen, aber kein vollständiges Bild ergeben, wenn Sie versuchen, sie auf den Tisch zu legen, dann ist das ein Problem, das diese neue Mathematik lösen will. Die große Frage lautet: Können wir diese hochkomplexe Mathematik nutzen, um ein unfehlbares System zum Verständnis von Ursache und Wirkung aufzubauen, selbst wenn wir die Welt durch Tests verändern?

Die Reise der Arbeit: Den Bau eines kausalen Lego-Sets

Diese Arbeit ist ein massives, computergeprüftes Konstruktionsprojekt. Die Autoren, unter der Leitung von Karen Sargsyan, nahmen eine kühne neue Theorie namens „Topos Causal Models“ und bauten sie von Grund auf in einem Computerprogramm namens *Cubical Agda neu auf. Betrachten Sie dieses Programm als einen superstrengen Lego-Meister, der sich weigert, zwei Steine zusammenzustecken, es sei denn, die Verbindung ist mathematisch perfekt. Das Ziel war es, eine Theorie zu verifizieren, die von einem Forscher namens Mahadevan vorgeschlagen wurde und besagt, dass wir das gesamte Universum von Ursache und Wirkung unter den Regeln eines „Topos“ (eines mathematischen Universums) beschreiben können.

Die Autoren haben die Theorie nicht einfach kopiert; sie haben sie getestet, korrigiert und Dinge gefunden, die der ursprüngliche Autor übersehen hatte. Hier ist, was sie entdeckt haben, erklärt durch die Linse ihrer digitalen Baustelle.

1. Der „Do-Button“ und der Wahrheitsfilter

In der ursprünglichen Theorie wird eine Intervention (wie das Erzwingen eines bestimmten Wertes für eine Variable, geschrieben als do(X = x)) als eine spezielle „charakteristische Abbildung“ beschrieben. Stellen Sie sich vor, Sie haben eine riesige Stadtkarte (die kausale Welt). Wenn Sie eine bestimmte Straße sperren wollen, löschen Sie nicht einfach die Straße; Sie zeichnen einen speziellen „Wahrheitsfilter“ über die Karte. Dieser Filter hebt genau die Stelle hervor, an der die Straße gesperrt ist, und sonst nirgendwo sonst.

Die Autoren bauten diesen Filter in ihren Computercode ein. Sie bewiesen, dass dieser Filter genau so funktioniert, wie versprochen: Er identifiziert perfekt die „gesperrte Straße“ und nichts anderes. Sie zeigten, dass dies nicht nur ein cleverer Trick ist, sondern eine fundamentale Regel dieses mathematischen Universums. Wenn man versucht, einen Wert zu erzwingen, der nicht zum natürlichen Fluss der Karte passt, lehnt das System dies ab. Dies bestätigt, dass der „Do-Button“ ein solides, zuverlässiges Werkzeug in diesem neuen Rahmen ist.

2. Der Kleber, der manchmal versagt

Eines der spannendsten Versprechen der ursprünglichen Theorie war das Sheaf Gluing (Schicht-Verklebung). Stellen Sie sich vor, drei verschiedene Detektive betrachten einen Tatort aus drei verschiedenen Blickwinkeln. Wenn Detektiv A mit Detektiv B übereinstimmt und Detektiv B mit Detektiv C übereinstimmt, könnte man annehmen, dass sie sich alle auf das Gesamtbild einigen. In dieser Mathematik bedeutet „Verkleben“, diese lokalen Ansichten zu nehmen und sie zu einer einzigen, globalen Wahrheit zusammenzusetzen.

Die Autoren bewiesen, dass dies für zwei Detektive immer funktioniert. Wenn ihre Ansichten sich überschneiden und übereinstimmen, können sie perfekt zusammengeklebt werden. Sie fanden jedoch einen Fehler, wenn drei oder mehr Detektive involviert sind. Sie konstruierten ein Szenario (ein „Specker-Dreieck“), bei dem jedes Paar von Detektiven perfekt übereinstimmt, aber wenn man versucht, alle drei zu kombinieren, bricht das Bild auseinander. Es gibt keine einzige globale Geschichte, die zu allen lokalen Hinweisen passt. Dies ist eine „Kontextualitäts-Obstruktion“. Es ist, als hätte man drei Puzzleteile, die paarweise zusammenpassen, aber wenn man versucht, sie alle auf den Tisch zu legen, entsteht in der Mitte ein Loch. Die Autoren bewiesen, dass dies kein Bug in ihrem Code ist, sondern ein echliches Merkmal der Mathematik. Es bedeutet, dass in komplexen kausalen Systemen die Tatsache, dass lokale Teile übereinstimmen, nicht bedeutet, dass eine globale Lösung existiert. Man benötigt eine globale Prüfung, nicht nur lokale.

3. Das Reparieren der „Magischen Modalität“

Die Theorie verwendet ein spezielles Werkzeug namens Lawvere-Tierney-Topologie (nennen wir es eine „Magische Modalität“), um zu entscheiden, welche kausalen Fakten in verschiedenen Situationen „stabil“ oder „wahr“ sind. Das Originalpapier listete drei Regeln für dieses magische Werkzeug auf. Die Autoren rechneten die Zahlen durch und fanden ein Problem: Diese drei Regeln waren nicht ausreichend! Sie fanden eine seltsame, dreistufige Leiter, bei der das Werkzeug zwar allen drei Regeln folgte, aber dennoch die Logik brach (es war nicht „inflationär“, was bedeutet, dass es die Dinge nicht immer gleich oder größer hielt).

Sie behoben dies, indem sie eine vierte Regel hinzufügten. Mit dieser neuen Regel funktioniert das magische Werkzeug korrekt. Sie zeigten dann, dass dieses Werkzeug das „Do-Calculus“ (die Regeln zur Berechnung von Ursache und Wirkung) stabil macht. Egal, wie man die Welt zerschneidet oder die Perspektive ändert, die Kernregeln der Kausalität bleiben bestehen. Sie zeigten sogar ein spezifisches Beispiel dieser „Magie“ in Aktion: die „Doppel-Negations-Topologie“, die wie ein Filter wirkt, der unscharfe, unsichere Wahrheiten in klare, klassische Fakten verwandelt.

4. Wahrheit über Welten hinweg transportieren

Schließlich befassten sich die Autoren mit der Transportierbarkeit: Kann eine Regel, die wir in einer Welt lernen (wie in einem Krankenhaus in Tokio), in einer anderen vertraut werden (in einer Klinik in New York)? In ihrem Rahmen ist das Verschieben eines kausalen Faktes von einem Ort zum anderen dasselbe wie die Prüfung, ob er unter der Magischen Modalität „stabil“ ist. Wenn ein Fakt stabil ist, reist er sicher. Wenn er nicht stabil ist, könnte er kaputtgehen, wenn man ihn bewegt. Sie bewiesen, dass für bestimmte Arten von Fakten (wie jene, die Interventionen betreffen) diese Stabilität garantiert ist. Sie merkten jedoch an, dass die Mathematik für komplexere, realweltliche Szenarien, in denen Fakten ihre Werte zwischen Welten ändern könnten, schwieriger wird und weitere Arbeit erfordert, um sie vollständig zu lösen.

Das Fazendatum

Diese Arbeit ist ein Triumph der Verifizierung. Sie sagte nicht nur: „Diese Theorie sieht cool aus.“ Sie baute die Theorie in einem Computer auf, zwang sie, strengen logischen Regeln zu folgen, und fand heraus, dass:

Der „Do-Button“ perfekt als Wahrheitsfilter funktioniert.
Lokale Übereinstimmungen manchmal daran scheitern, eine globale Wahrheit zu schaffen (das „Drei-Detektive-Problem“).
Die ursprünglichen Regeln für die „Magische Modalität“ unvollständig waren und eine vierte Regel benötigten, um zu funktionieren.
Sobald dies korrigiert ist, beweist das System, dass kausale Regeln stabil sind und über verschiedene Umgebungen hinweg transportiert werden können.

Die Autoren sind sich über diese Ergebnisse sehr sicher, weil sie maschinengeprüft sind. Jeder einzelne Schritt wurde vom Computer verifiziert, ohne Annahmen oder „Vielleicht“-Momente. Sie haben dies nicht nur simuliert; sie haben es mathematisch bewiesen. Sie sind jedoch vorsichtig zu betonen, dass dies nur die „1-Topos“-Version ist (eine spezifische, einfachere Art des mathematischen Universums). Sie haben noch nicht das gesamte Problem der Kausalität gelöst, insbesondere die Teile, die gerichtete Pfeile betreffen (wo A nach B verursacht, aber B nicht nach A). Aber für den Teil, den sie angegangen sind, haben sie ein felsenfester Fundament gebaut und bewiesen, dass die Mathematik hinter kausalen Modellen nicht nur eine schöne Idee, sondern eine verifizierte, funktionierende Realität ist.

Technische Zusammenfassung: Eine kubische Formalisierung von Topos-Kausalen Modellen

Problem und Motivation
Die Arbeit adressiert die Verifizierung von „Topos Causal Models“ (TCMs), einem Rahmenwerk, das von Mahadevan [Mah25c, Mah25b, Mah25a] vorgeschlagen wurde und die kausale Inferenz innerhalb der Kategorie eines Topos neu formuliert. In diesem Rahmenwerk ist eine kausale Welt ein Präpräš (Presheaf), Interventionen sind charakteristische Abbildungen in den Subobjektklassifikator $\Omega$ , und das Schließen erfolgt in der intuitionistischen internen Sprache. Während das Quellmaterial eine konzeptionelle Umformulierung liefert, in der die Standard-Kausalanlagen (Intervention, Mechanismus-Assemblierung, Kontrafaktualität) den topos-theoretischen universellen Eigenschaften entsprechen, handelt es sich dabei um eine rein papierbasierte Entwicklung. Zentrale Behauptungen im Quellmaterial werden ohne Beweis aufgestellt, und einige Axiome bleiben abstrakt oder potenziell unvollständig. Das Problem besteht darin, eine maschinell überprüfte Verifizierung dieses 1-Topos-Kerns bereitzustellen, um die logische Konsistenz des Rahmenwerks sicherzustellen und etwaige Lücken in der ursprünglichen axiomatischen Präsentation zu identifizieren.

Methodik
Die Autoren implementieren die Formalisierung in Cubical Agda, einem Proof Assistant, der auf kubischer Typentheorie basiert. Die Entwicklung ist eine direkte Fortsetzung einer Begleitarbeit [Sar26], welche ein Wahrscheinlichkeitsmonad und die Regeln des Pearlschen do-Calculus verifiziert hat.

Fundamente: Die Arbeit operiert über dem Präpräš-Topos $\mathbf{PSh}(\mathcal{C}) = \mathbf{Set}^{\mathcal{C}^{op}}$ über einer abstrakten Basiskategorie $\mathcal{C}$ von Kontexten.
Sicherheit und Axiome: Die gesamte Entwicklung lässt sich unter dem Agda-Flag --safe typisieren, was bedeutet, dass sie keine Postulate, Löcher oder unsicheren Merkmale enthält. Das zugrunde liegende geordnete Körperfeld wird konkret als die rationalen Zahlen $\mathbb{Q}$ instanziiert, wodurch abstrakte Postulate vermieden werden.
Struktur: Die Formalisierung baut den Subobjektklassifikator $\Omega$ als einen Präpräš von Sieben (Sieves) auf, definiert die interne Sprache via Kripke-Joyal-Forcing und konstruiert eine Lawvere-Tierney-Topologie, um die $j$ -do-calculus-Modalität zu modellieren.

Zentrale Beiträge und Ergebnisse

Der Interventionsklassifikator (Abschnitt 3):
Die Autoren konstruieren $\Omega$ als den Präpräš von Sieben und realisieren die Intervention $do(X := x_0)$ als eine charakteristische Abbildung $\chi: X \to \Omega$ . Sie beweisen den Klassifikationstheorem in beide Richtungen: $\chi_c(b) = \top \iff b = x_0^c$ . Entscheidend ist, dass sie etablieren, dass für die Konstruktion topos-intern zu sein, der feste Wert $x_0$ ein natürliches globales Element (ein in den Kontext natürlicher Wert) sein muss, nicht bloß eine kontextindexierte Familie. Dies beweist, dass $\Omega$ der Subobjektklassifikator ist und das universelle Eigentum erfüllt, dass jedes restriktionsgeschlossene Sub-Präpräš durch eine eindeutige Abbildung nach $\Omega$ klassifiziert wird.
Sheaf-Gluing unabhängiger Mechanismen (Abschnitt 4):
Das Quellmaterial behauptet, dass lokale Mechanismen, die auf Überlappungen übereinstimmen, zu einem eindeutigen globalen Mechanismus „zusammengefügt“ werden können, liefert jedoch keinen Beweis. Die Autoren beweisen dies als Pullback-Limit im Präpräš-Topos. Sie zeigen, dass für zwei Mechanismen $p: X \to Z$ und $q: Y \to Z$ der Pullback $X \times_Z Y$ kontextweise existiert, und dass jeder Kegel übereinstimmender Mechanismen eindeutig durch diesen Pullback faktorisiert. Dies bestätigt die „Gluing“-Eigenschaft, ohne eine Grothendieck-Topologie oder Sheafifizierung zu erfordern, da dies für alle Präpräš gilt.
Die interne Sprache (Abschnitt 5):
Das Paper definiert das Kripke-Joyal-Forcing für die interne Logik und überprüft maschinell die Klauseln für alle Konnektive ( $\top, \bot, \land, \lor, \Rightarrow$ ) und Quantoren ( $\forall, \exists$ ). Sie verifizieren die Lokalitäts-Eigenschaft (Monotonie) und stellen sicher, dass das Forcing unter Restriktion stabil bleibt, was das definierende Merkmal der Kripke-Semantik ist.
Korrektur der Lawvere-Tierney-Axiome (Abschnitt 6):
Eine bedeutende Erkenntnis ist eine Lücke in der Standarddefinition der Lawvere-Tierney-Topologie, die im Quellmaterial angegeben wurde. Die drei Standardaxiome (Bewahrung von $\top$ , Bewahrung von $\land$ und Idempotenz) implizieren nicht zwangsläufig die Inflativität ( $S \leq j(S)$ ). Die Autoren liefern ein Gegenmodell (eine dreigliedrige Kette), das die drei Axiome erfüllt, bei dem die Inflativität jedoch fehlschlägt, was bedeutet, dass der Operator nicht notwendigerweise ein Abschlussoperator ist. Sie fügen die Inflativität als viertes Axiom hinzu, um sicherzustellen, dass $j$ ein Abschlussoperator (Nukleus) ist.
- Konkretes Beispiel: Sie führen die Doppelte Negation ( $\neg\neg$ ) als ein nicht-degeneriertes konkretes Beispiel auf.
- Stabilität: Sie beweisen, dass Interventionen und Pearls drei do-calculus-Regeln $j$ -geschlossen (stabil) sind für jede Topologie. Sie merken jedoch an, dass dies trivial für Regeln ist, deren Schlussfolgerungen bewiesene Gleichheiten (Wahrheitswert $\top$ ) sind. Das substantielle Ergebnis betrifft kontingente Behauptungen (z. B. bedingte Unabhängigkeiten, die in einigen Regimen gelten, aber in anderen nicht), und zeigt, dass deren Wahrheitswerte unter der Doppel-Negations-Topologie $j$ -geschlossen sind.
Kontextualitäts-Obstruktion (Abschnitt 7):
Die Autoren führen ein Phänomen ein, das im ursprünglichen Programm nicht berücksichtigt wurde: eine kohomologische Obstruktion gegen das Gluing. Während zwei Mechanismen immer zusammengefügt werden können, können drei Kontexte scheitern, ein globales Modell zuzulassen, selbst wenn sie paarweise konsistent sind. Sie maschinell überprüfen Speckers Dreieck (drei Boole’sche Observablen mit paarweiser Antikorrelation) als minimales Zeugnis.
- Sie formalisieren die Obstruktion als eine nicht-verschwindende Klasse in der ersten Čech-Kohomologie ( $H^1$ ) des Covers mit $\mathbb{Z}_2$ -Koeffizienten.
- Sie beweisen, dass eine globale Sektion existiert, wenn und nur wenn die Holonomie des Zyklus trivial ist. Speckers Dreieck besitzt eine nicht-triviale Holonomie, was das Fehlen eines globalen Modells bestätigt.
Transportierbarkeit als Invarianz (Abschnitt 8):
Das Paper identifiziert die Transportierbarkeit eines Kontrafaktuals über ein Cover von Regimen als $j$ -Stabilität (Invarianz). Ein Kontrafaktual gilt global (ist transportierbar), wenn und nur wenn sein interner Wahrheitswert $j$ -geschlossen ist. Sie beweisen die Korrektheit: Wenn ein Kontrafaktual $j$ -stabil ist und in einer $j$ -dichten Umgebung gilt, dann gilt es global.

Bedeutung und Ansprüche
Das Paper beansprucht Bedeutung in zwei primären Bereichen:

Gewährleistung: Die zentralen Behauptungen des TCM-Rahmenwerks sind nun zertifiziert statt lediglich behauptet. Dies ist entscheidend für die Automatisierung, da ein verifizierter Kern notwendig ist, um maschinell generierte kausale Modelle zu prüfen.
Praktische Erkenntnisse: Die Mechanisierung offenbarte zwei praktische Einsichten:
- Die Garantien der modalen Schicht hängen davon ab, dass $j$ ein Abschlussoperator ist; die ursprünglichen Axiome waren unzureichend.
- Die modulare Assemblierung kausaler Mechanismen (Map-Reduce-Stil) ist nicht allein durch paarweise Übereinstimmung garantiert; eine globale Konsistenzprüfung ist erforderlich, um kohomologische Obstruktionen (Kontextualität) zu detektieren.

Geltungsbereich und Limitationen
Die Autoren begrenzen den Umfang explizit auf das 1-Topos (Präpräš)-Fragment.

Sie formalisieren keine Typ-Ebene der Sheafifizierung (den assoziierten-Sheaf-Reflektor auf dem gesamten Topos).
Sie befassen sich nicht mit dem gerichteten oder $\infty$ -kategorialen Lift des Rahmenwerks, welcher eine gerichtete Typentheorie erfordern würde, um die Asymmetrie der Kausalität zu modellieren (kausale Pfeile sind im aktuellen Präpräš-Modell symmetrisch).
Das Resultat zur Transportierbarkeit wird als Äquivalenz mit Invarianz unter einer spezifischen Dichtehypothese etabliert, wobei die Vollständigkeitsäquivalenz mit dem graphischen $s$ -hedge-Kriterium zukünftige Arbeit bleibt.

Die Entwicklung ist frei verfügbar und stellt die erste maschinell überprüfte Darstellung des 1-Topos-Kerns von Topos-kausalen Modellen dar, welche die modalen Axiome korrigiert sowie bisher unverifizierte Gluing- und Obstruktions-Eigenschaften bewiesen hat.