A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus
This work by Karen Sargsyan, submitted to arXiv in the cs.AI and cs.LO categories, presents a formalization of topos causal models within Cubical Agda. The core contribution is a machine-checked, foundational account of causal inference as envisioned in topos theory, where causal worlds are treated as presheaves. This addresses a gap in the field by providing rigorous, verifiable implementations of theoretical causal frameworks. The research is primarily for software engineers and researchers in AI, causality, and formal methods who are interested in building provably correct causal reasoning systems.
A key technical idea is the realization of interventions, specifically $\mathrm{do}(X := x_0)$, as characteristic maps into the subobject classifier of a topos. This provides a formal, categorical interpretation of the action of intervening in a causal model. Another significant contribution is the machine-checked proof of the sheaf gluing of independent mechanisms. This addresses a previously asserted but unproven property, crucial for composing complex causal systems from independent components. The paper also details the machine-checking of the Kripke-Joyal forcing clauses, which are fundamental for reasoning within the internal language of the topos. A notable finding and correction involves a gap in the standard Lawvere-Tierney axioms, where the absence of a specific axiom is shown to prevent the formation of a closure operator necessary for modal reasoning. Restoring this axiom leads to the identification of the double-negation topology as a concrete instance and demonstrates the stability of interventions and Pearl's causal rules under such topologies.
This formalization enables the development of robust, verifiable causal inference engines. By providing machine-checked proofs and implementations, it paves the way for increased trust and reliability in AI systems that rely on causal reasoning, particularly in safety-critical domains. The work’s emphasis on intuitionistic logic and topos theory may influence the development of new paradigms for representing and reasoning about causality, potentially leading to more sophisticated counterfactual reasoning and transportability across different causal regimes. The inclusion of a machine-checked contextuality obstruction also highlights the potential for formal methods to uncover subtle limitations in data and models, a phenomenon not previously considered in the topos causal model program. The current scope is limited to the presheaf (1-topos) fragment, with type-level sheafification and directed lifts left as future work. This abstract only describes the work.