🤖 AI

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

Cet article présente la première formalisation vérifiée par machine dans Cubical Agda des modèles causaux de type topos, vérifiant des concepts fondamentaux tels que l'intervention en tant que cartes caractéristiques et le collage de faisceaux, tout en identifiant et en réparant une lacune dans les axiomes de Lawvere-Tierney pour établir la stabilité des règles de Pearl et en démontrant une obstruction de contextualité au sein d'un cadre sûr et sans axiome.

Auteurs originaux : Karen Sargsyan

Publié 2026-07-20

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Karen Sargsyan

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le dilemme du détective : Pourquoi la causalité nécessite une nouvelle carte

Imaginez que vous êtes un détective essayant de résoudre un mystère. Vous avez une liste d'indices : « Il a plu », « L'herbe est mouillée » et « L'arroseur était allumé ». Par le passé, les scientifiques traitaient ces indices comme une simple liste de faits. Si l'herbe est mouillée, ils pourraient supposer qu'il a plu. Mais la vie réelle est plus complexe. Et si c'était vous qui aviez mouillé l'herbe en allumant l'arroseur ? Cela change-t-il le fait qu'il a plu ? C'est le cœur de l'inférence causale : comprendre non seulement ce qui arrive ensemble, mais ce qui cause quoi, surtout lorsque nous intervenons et que nous changeons les règles du jeu.

Pendant des décennies, les experts ont utilisé des diagrammes et des mathématiques pour suivre ces chaînes de cause à effet. Mais récemment, une nouvelle idée est apparue : et si nous considérions le monde entier des causes non pas comme une image statique, mais comme un paysage changeant qui varie selon l'endroit où l'on regarde ? C'est le domaine de la Théorie des Topos, une branche des mathématiques qui étudie comment les formes et les structures s'emboîtent. Voyez cela comme un langage universel pour « coller » des morceaux d'information. Si vous avez un puzzle dont les pièces s'emboîtent parfaitement dans vos mains mais ne forment pas une image complète quand vous essayez de les poser sur la table, c'est un problème que ces nouvelles mathématiques tentent de résoudre. La grande question est la suivante : pouvons-nous utiliser ces mathématiques de haut niveau pour construire un système infaillible pour comprendre la cause et l'effet, même lorsque nous changeons le monde en faisant des tests ?

Le voyage du papier : Construire un kit Lego causal

Ce document est un projet de construction massif, vérifié par ordinateur. Les auteurs, dirigés par Karen Sargsyan, ont pris une théorie audacieuse appelée « Modèles causaux de Topos » et l'ont reconstruite de fond en comble à l'intérieur d'un programme informatique appelé Cubical Agda. Voyez ce programme comme un maître Lego super strict qui refuse de vous laisser emboîter deux briques à moins que la connexion ne soit mathématiquement parfaite. L'objectif était de vérifier une théorie proposée par un chercheur nommé Mahadevan, qui suggère que nous pouvons décrire l'univers entier de la cause à effet en utilisant les règles d'un « Topos » (un univers mathématique).

Les auteurs n'ont pas simplement copié la théorie ; ils l'ont testée, corrigée et ont trouvé des choses que l'auteur original avait manquées. Voici ce qu'ils ont découvert, expliqué à travers le prisme de leur chantier de construction numérique.

1. Le « Bouton Do » et le filtre de vérité

Dans la théorie originale, une intervention (comme forcer une variable à prendre une valeur spécifique, écrite sous la forme do(X = x)) est décrite comme une « application caractéristique » spéciale. Imaginez que vous avez une carte géante d'une ville (le monde causal). Si vous voulez forcer la fermeture d'une rue spécifique, vous ne vous contentez pas d'effacer la rue ; vous dessinez un « filtre de vérité » spécial sur la carte. Ce filtre met en évidence précisément là où la rue est fermée et nulle part ailleurs.

Les auteurs ont construit ce filtre dans leur code informatique. Ils ont prouvé que ce filtre fonctionne exactement comme promis : il identifie parfaitement la « rue fermée » et rien d'autre. Ils ont montré qu'il ne s'agit pas seulement d'une astuce ingénieuse, mais d'une règle fondamentale de cet univers mathématique. Si vous essayez de forcer une valeur qui ne correspond pas au flux naturel de la carte, le système la rejette. Cela confirme que le « Bouton Do » est un outil solide et fiable dans ce nouveau cadre.

2. La colle qui échoue parfois

L'une des promesses les plus excitantes de la théorie originale était le Collage de Faisceaux (Sheaf Gluing). Imaginez trois détectives différents observant une scène de crime sous trois angles différents. Si le Détective A est d'accord avec le Détective B, et que le Détective B est d'accord avec le Détective C, vous pourriez supposer qu'ils sont tous d'accord sur l'image globale. Dans ces mathématiques, le « collage » signifie prendre ces vues locales et les emboîter pour former une vérité globale géante.

Les auteurs ont prouvé que pour deux détectives, cela fonctionne toujours. Si leurs points de vue se chevauchent et concordent, ils peuvent être collés parfaitement. Cependant, ils ont découvert un dysfonctionnement lorsqu'il y a trois détectives ou plus. Ils ont construit un scénario (un « triangle de Specker ») où chaque paire de détectives est parfaitement d'accord, mais lorsqu'on tente de combiner les trois, l'image s'effondre. Il n'existe pas de récit global unique qui s'adapte à tous les indices locaux. C'est une « obstruction de contextualité ». C'est comme avoir trois pièces de puzzle qui s'emboîtent par paires, mais quand on essaie de les poser toutes sur la table, elles forment un trou au milieu. Les auteurs ont prouvé que ce n'est pas un bug dans leur code, mais une véritable caractéristique des mathématiques. Cela signifie que dans les systèmes causaux complexes, le fait que les parties locales soient d'accord ne garantit pas l'existence d'une solution globale. Il faut un contrôle global, pas seulement des contrôles locaux.

3. Réparer la « Modalité Magique »

La théorie utilise un outil spécial appelé topologie de Lawvere-Tierney (appelons-le une « Modalité Magique ») pour décider quels faits causaux sont « stables » ou « vrais » à travers différentes situations. Le papier original énumérait trois règles pour cet outil magique. Les auteurs ont passé les chiffres en revue et ont trouvé un problème : ces trois règles ne suffisaient pas ! Ils ont découvert une étrange échelle à trois marches où l'outil suivait les trois règles mais brisait la logique (il n'était pas « inflationnaire », ce qui signifie qu'il ne maintenait pas toujours les choses identiques ou plus grandes).

Ils ont réparé cela en ajoutant une quatrième règle. Avec cette nouvelle règle, l'outil magique fonctionne correctement. Ils ont ensuite montré que cet outil rend le « calcul Do » (les règles pour calculer la cause et l'effet) stable. Peu importe la façon dont vous découpez le monde ou changez de perspective, les règles fondamentales de la causalité restent fermes. Ils ont même montré un exemple spécifique de cette « magie » en action : la topologie de la « double négation », qui agit comme un filtre transformant les vérités floues et incertaines en faits classiques clairs.

4. Transporter la vérité à travers les mondes

Enfin, les auteurs se sont attaqués à la Transposabilité : une règle apprise dans un monde (comme un hôpital à Tokyo) peut-elle être fiable dans un autre (une clinique à New York) ? Dans leur cadre, déplacer un fait causal d'un endroit à un autre revient à vérifier s'il est « stable » sous la Modalité Magique. Si un fait est stable, il voyage en toute sécurité. S'il n'est pas stable, il pourrait se briser lors du déplacement. Ils ont prouvé que pour certains types de faits (impliquant des interventions), cette stabilité est garantie. Cependant, ils ont noté que pour des scénarios réels plus complexes où les faits pourraient changer de valeur entre les mondes, les mathématiques deviennent plus délicates et nécessitent plus de travail pour être pleinement résolues.

L'essentiel

Ce papier est un triomphe de la vérification. Il n'a pas seulement dit : « Cette théorie a l'air cool ». Il a construit la théorie dans un ordinateur, l'a forcée à suivre des règles logiques strictes et a découvert que :

Le « Bouton Do » fonctionne parfaitement comme un filtre de vérité.
Les accords locaux peuvent parfois échouer à créer une vérité globale (le problème des « trois détectives »).
Les règles originales de la « Modalité Magique » étaient incomplètes et nécessitaient une quatrième règle pour fonctionner.
Une fois corrigé, le système prouve que les règles causales sont stables et peuvent être transportées d'un environnement à un autre.

Les auteurs sont très sûrs de ces résultats car ils sont vérifiés par machine. Chaque étape a été vérifiée par l'ordinateur, sans suppositions ni moments de « peut-être ». Ils n'ont pas seulement simulé cela ; ils l'ont prouvé mathématiquement. Cependant, ils précisent avec prudence qu'il s'agit seulement de la version « 1-topos » (un type spécifique et plus simple d'univers mathématique). Ils n'ont pas encore résolu l'intégralité du problème de la causalité, en particulier les parties impliquant des flèches dirigées (où A cause B, mais B ne cause pas A) de manière totalement asymétrique. Mais pour la partie qu'ils ont abordée, ils ont construit une base solide, prouvant que les mathématiques derrière les modèles causaux ne sont pas seulement une belle idée, mais une réalité fonctionnelle et vérifiée.

Résumé Technique : Une Formalisation Cubique des Modèles Causaux de Topos

Problème et Motivation
L'article traite de la vérification des « Modèles Causaux de Topos » (MCT), un cadre proposé par Mahadevan [Mah25c, Mah25b, Mah25a] qui reformule l'inférence causale au sein de la catégorie d'un topos. Dans ce cadre, un monde causal est un préfaisceau, les interventions sont des applications caractéristiques vers le classificateur de sous-objets $\Omega$ , et le raisonnement s'opère dans le langage interne intuitionniste. Bien que le matériel source fournisse une reformulation conceptuelle où la machinerie causale standard (intervention, assemblage de mécanismes, contre-factuels) correspond aux propriétés universelles de la théorie des topos, il s'agit d'un développement basé sur du texte papier. Les affirmations centrales clés dans la source sont énoncées sans preuve, et certains axiomes sont laissés abstraits ou potentiellement incomplets. Le problème est de fournir une vérification par machine du cœur 1-topos, assurant la cohérence logique du cadre et identifiant les lacunes dans la présentation axiomatique originale.

Méthodologie
Les auteurs implémentent la formalisation dans Cubical Agda, un assistant de preuve basé sur la théorie des types cubiques. Le développement est la suite directe d'un article compagnon [Sar26] qui a vérifié un monaide de probabilité et les règles du $do$-calculus de Pearl.

Fondations : Le travail opère sur le topos de préfaisceaux $\mathbf{PSh}(\mathcal{C}) = \mathbf{Set}^{\mathcal{C}^{op}}$ sur une catégorie de base abstraite $\mathcal{C}$ de contextes.
Sécurité et Axiomes : L'ensemble du développement respecte le flag --safe d'Agda, ce qui signifie qu'il ne contient aucun postulat, trou ou caractéristique non sécurisée. Le corps de l'ordre est concrètement instancié comme les nombres rationnels $\mathbb{Q}$ , évitant ainsi les postulats abstraits.
Structure : La formalisation construit le classificateur de sous-objets $\Omega$ comme un préfaisceau de cribles (sieves), définit le langage interne via la forcing de Kripke-Joyal, et construit une topologie de Lawvere-Tierney pour modéliser la modalité du $j$ -$do$-calculus.

Contributions Clés et Résultats

Le Classificateur d'Intervention (Section 3) :
Les auteurs construisent $\Omega$ comme le préfaisceau de cribles et réalisent l'intervention $do(X := x_0)$ comme une application caractéristique $\chi: X \to \Omega$ . Ils prouvent le théorème de classification dans les deux sens : $\chi_c(b) = \top \iff b = x_0^c$ . Crucialement, ils établissent que pour que la construction soit interne au topos, la valeur fixée $x_0$ doit être un élément global naturel (une valeur naturelle dans le contexte), et non simplement une famille indexée par le contexte. Cela prouve que $\Omega$ est le classificateur de sous-objets, satisfaisant la propriété universelle selon laquelle tout sous-préfaisceau fermé par restriction est classifié de manière unique par une application vers $\Omega$ .
Collage de Mécanismes Indépendants par Faisceau (Section 4) :
Le matériel source affirme que des mécanismes locaux s'accordant sur les recouvrements peuvent être « collés » en un mécanisme global unique, mais ne fournit aucune preuve. Les auteurs prouvent cela comme un limite de produit tiré dans le topos de préfaisceaux. Ils démontent que pour deux mécanismes $p: X \to Z$ et $q: Y \to Z$ , le produit tiré $X \times_Z Y$ existe par contexte, et tout cône de mécanismes concordants se factorise de manière unique à travers ce produit tiré. Cela confirme la propriété de « collage » sans nécessiter de topologie de Grothendieck ou de faisceautisation, car elle est vraie pour tous les préfaisceaux.
Le Langage Interne (Section 5) :
Le papier définit la forcing de Kripke-Joyal pour la logique interne et vérifie par machine les clauses pour tous les connecteurs ( $\top, \bot, \land, \lor, \Rightarrow$ ) et quantificateurs ( $\forall, \exists$ ). Ils vérifient la propriété de localité (monotonicité), garantissant que la forcing est stable sous restriction, ce qui est la caractéristique définissante de la sémantique de Kiel.
Correction des Axiomes de Lawvere-Tierney (Section 6) :
Une découverte significative est une lacune dans la définition standard d'une topologie de Lawvere-Tierney fournie dans la source. Les trois axiomes standards (préservation de $\top$ , préservation de $\land$ , et idempotence) n'impliquent pas l'inflationnité ( $S \leq j(S)$ ). Les auteurs fournissent un contre-modèle (une chaîne de trois éléments) satisfaisant les trois axiomes où l'inflationnité échoue, signifiant que l'opérateur n'est pas nécessairement un opérateur de clôture. Ils ajoutent l'inflationnité comme un quatrième axiome pour garantir que $j$ est un opérateur de clôture (noyau).
- Instance Concrète : Ils exhibent la topologie de la double négation ( $\neg\neg$ ) comme une instance concrète non dégénérée.
- Stabilité : Ils prouvent que les interventions et les trois règles du $do$-calculus de Pearl sont $j$ -fermées (stables) pour chaque topologie. Cependant, ils notent que cela est trivial pour les règles dont les conclusions sont des égalités prouvées (valeur de vérité $\top$ ). Le résultat substantiel concerne les affirmations contingentes (par exemple, les indépendances conditionnelles qui tiennent dans certains régimes mais pas d'autres), montrant que leurs valeurs de vérité sont $j$ -fermées sous la topologie de la double négation.
Obstruction de Contextualité (Section 7) :
Les auteurs introduisent un phénomène non considéré dans le programme original : une obstruction cohomologique au collage. Bien que deux mécanismes se collent toujours, trois contextes peuvent échouer à admettre un modèle global même s'ils sont pairwise cohérents. Ils vérifient par machine le triangle de Specker (trois observables booléennes avec des anti-corrélations par paires) comme témoin minimal.
- Ils formalisent l'obstruction comme une classe non nulle dans la première cohomologie de Čech ( $H^1$ ) du recouvrement avec des coefficients $\mathbb{Z}_2$ .
- Ils prouvent qu'une section globale existe si et seulement si l'holonomie du cocycle est triviale. Le triangle de Specker possède une holonomie non triviale, confirmant l'absence de modèle global.
La Transportabilité comme Invariance (Section 8) :
Le papier identifie la transportabilité d'un contre-factuel à travers un recouvrement de régimes avec la $j$ -stabilité (invariance). Un contre-factuel tient globalement (est transportable) si et seulement si sa valeur de vérité interne est $j$ -fermée. Ils prouvent la correction : si un contre-factuel est $j$ -stable et tient dans un environnement $j$ -dense, il tient globalement.

Signification et Revendications
Le papier revendique une importance dans deux domaines principaux :

Assurance : Les affirmations centrales du cadre TCM sont désormais certifiées plutôt qu'affirmées. Cela est critique pour l'automatisation, car un cœur vérifié est nécessaire pour vérifier les modèles causaux générés par machine.
Résultats Pratiques : La mécanisation a révélé deux intuitions pratiques :
- Les garanties de la couche modale dépendent du fait que $j$ soit un opérateur de clôture ; les axiomes originaux étaient insuffisants.
- L'assemblage modulaire de mécanismes causaux (style map-reduce) n'est pas garanti par la seule cohérence par paires ; une vérification de cohérence globale est requise pour détecter les obstructions cohomologiques (contextualité).

Portée et Limites
Les auteurs limitent explicitement la portée au fragment 1-topos (préfaisceau).

Ils ne formalisent pas la faisceautisation de type-niveau (le réflecteur de faisceau associé sur l'ensemble du topos).
Ils ne traitent pas le levé directed ou $\infty$ -catégorique du cadre, qui nécessiterait une théorie des types dirigée pour modéliser l'asymétrie de la causalité (les flèches causales sont symétriques dans le modèle de préfaisceau actuel).
Le résultat de transportabilité est établi comme une équivalence avec l'invariance sous une hypothèse de densité spécifique, mais l'équivalence de complétude avec le critère du $s$ -hedge graphique reste un travail futur.

Le développement est disponible en accès libre et représente le premier compte vérifié par machine du cœur 1-topos des modèles causaux de topos, corrigeant les axiomes modaux et prouvant les propriétés de collage et d'obstruction précédemment non vérifiées.