🤖 AI

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

本文呈现了在 Cubical Agda 中对拓扑因果模型（topos causal models）进行的首次机器检查形式化，验证了诸如将干预视为特征映射以及层粘合（sheaf gluing）等核心概念，同时识别并修复了 Lawvere-Tierney 公理中的一个漏洞以确立 Pearl 规则的稳定性，并在一个安全的、无公理框架内展示了上下文相关性障碍（contextuality obstruction）。

原作者： Karen Sargsyan

发布于 2026-07-20

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Karen Sargsyan

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

侦探的困境：为什么因果关系需要一张新地图

想象你是一名正在试图破解谜团的侦探。你有一份线索清单：“下雨了”、“草地是湿的”以及“洒水器开了”。在过去，科学家们将这些线索视为简单的事实列表。如果草地是湿的，他们可能会推测下过雨。但现实生活要复杂得多。如果你通过打开洒水器让草地变湿，这会改变“下过雨”这个事实吗？这就是**因果推断（causal inference）*的核心：不仅要弄清楚发生了什么，还要弄清楚是什么导致*了什么，尤其是在我们进行干预并改变游戏规则时。

几十年来，专家们一直使用图表和数学来追踪这些因果链。但最近，出现了一个新想法：如果我们不把整个因果世界看作一个静态的图像，而是一个取决于观察位置而变化的移动景观，会怎样？这就是**拓扑斯理论（Topos Theory）**的领域，它是研究形状和结构如何相互契合的一个数学分支。你可以把它看作一种用于“粘合”信息碎片的通用语言。如果你有一个拼图，碎片在手里能完美契合，但试图拼成完整图像放在桌上时却无法完成，那么这就是这种新数学试图解决的问题。核心问题在于：我们能否利用这种高层级的数学，建立一个万无一失的系统来理解因果关系，即使在我们通过测试来改变世界的时候也是如此？

论文之旅：构建一套因果乐高集

这是一项大规模的、经过计算机检查的构建工程。由 Karen Sargsyan 领导的作者们采用了一种大胆的新理论——“拓扑斯因果模型”（Topos Causal Models），并在一个名为 Cubical Agda 的计算机程序中将其从头开始重建。你可以把这个程序想象成一个超级严苛的乐高大师，除非连接在数学上是完美的，否则它拒绝让你把两块积木拼在一起。其目标是验证研究员 Mahadevan 提出的一个理论，该理论认为我们可以使用“拓扑斯”（一个数学宇宙）的规则来描述整个因果宇宙。

作者们不仅仅是复制了该理论；他们测试了它，修正了它，并发现了原作者遗漏的东西。以下是他们发现的内容，通过他们的数字建筑工地视角来进行解释。

1. “Do按钮”与真值过滤器

在原始理论中，一次干预（例如强制变量为一个特定值，写作 do(X = x)）被描述为一个特殊的“特征映射”。想象你有一张巨大的城市地图（因果世界）。如果你想强制关闭某条特定的街道，你不仅仅是擦掉那条街；你是在地图上画了一个特殊的“真值过滤器”。这个过滤器精准地标出了街道关闭的位置，除此之外别无他处。

作者们在他们的计算机代码中构建了这个过滤器。他们证明了这个过滤器完全如承诺的那样工作：它完美地识别了“关闭的街道”且仅此而已。他们表明这不仅仅是一个聪明的技巧，而是这个数学宇宙的一条基本规则。如果你尝试强行赋予一个不符合地图自然流向的值，系统会拒绝它。这证实了“Do按钮”是这个新框架中一个坚实、可靠的工具。

2. 有时会失效的胶水

原始理论中最令人兴奋的承诺之一是层片粘合（Sheaf Gluing）。想象有三名不同的侦探从三个不同的角度观察犯罪现场。如果侦探 A 与侦探 B 一致，且侦探 B 与侦探 C 一致，你可能会假设他们对整体情况也达成了一致。在这种数学中，“粘合”意味着将这些局部视角捕捉并拼接成一个巨大的、全局的真相。

作者们证明了对于两个侦探来说，这总是奏效的。如果他们的视角有重叠且匹配，他们就可以完美地粘合在一起。然而，他们发现当涉及三个或更多侦探时，会出现一个故障。他们构建了一个场景（一个“Specker 三角形”），其中每两个侦探之间都完美一致，但当你试图将所有三个结合起来时，画面却崩塌了。不存在一个能符合所有局部线索的单一全局故事。这是一个“上下文阻碍”（contextuality obstruction）。这就像有三个拼图碎片，它们两两之间可以契合，但当你试图把它们全部放在桌上时，中间却出现了一个洞。作者们证明这并不是他们代码中的漏洞，而是数学中的一个真实特征。这意味着在复杂的因属系统中，仅仅局部部分一致并不意味着存在全局解。你需要全局性的检查，而不仅仅是局部的检查。

3. 修复“魔法模态”

该理论使用一种特殊的工具，称为 Lawvere-Tierney 拓扑（我们称之为“魔法模态”），来决定哪些因果事实在不同情境下是“稳定”或“真实”的。原论文列出了关于这个魔法工具的三条规则。作者们运行了计算并发现了一个问题：那三条规则不够！他们发现了一个奇怪的三级阶梯，其中的工具遵循了所有三条规则，但仍然破坏了逻辑（它不是“增量式”的，即它并不总是保持不变或变大）。

他们通过添加第四条规则修复了这个问题。有了这条新规则，这个魔法工具就能正确工作。随后，他们展示了这个工具如何使“Do演算”（计算因果关系的规则）保持稳定。无论你如何切割世界或改变视角，因果关系的核心规则始终稳固。他们甚至展示了这个“魔法”作用的一个具体例子：“双重否定”拓扑，它像一个过滤器，将模糊、不确定的真相转化为清晰的经典事实。

4. 在世界间传输真理

最后，作者们探讨了可迁移性（Transportability）：我们在一个世界（如东京的医院）学到的规则，能否在另一个世界（如纽约的诊所）得到信任？在他们的框架中，将一个因果事实从一个地方移动到另一个地方，等同于检查它在“魔法模态”下是否是“稳定的”。如果一个事实是稳定的，它就能安全传输。如果它不稳定，移动时就可能失效。他们证明了对于某些类型的特征（例如涉及干预的特征），这种稳定性是得到保证的。然而，他们指出，对于那些事实可能会在不同世界间发生变化的更复杂的现实场景，数学过程会变得更加棘手，需要更多的工作才能完全解决。

总结

这篇论文是验证的一次胜利。它不仅仅说“这个理论看起来很酷”，它在计算机中构建了该理论，迫使其遵循严格的逻辑规则，并发现：

“Do按钮”作为真值过滤器工作得非常完美。
局部的一致有时无法构成全局的真相（“三个侦探”问题）。
原始的“魔法模态”规则是不完整的，需要第四条规则才能生效。
修复后，该系统证明了因果规则是稳定的，并且可以跨环境进行迁移。

作者们对这些结果非常有信心，因为它们是经过机器检查的。每一步都经过了计算机的验证，没有任何假设或“也许”的时刻。他们不仅仅是在模拟，他们是在进行数学证明。然而，他们也谨慎地指出，这只是“1-层级拓扑斯”（1-topos）版本（一种特定的、较简单的数学宇宙类型）。他们还没有解决整个因果关系问题，特别是涉及有向箭头（即 A 导致 B，但 B 不导致 A）的完全非对称的部分。但在他们所处理的部分，他们已经建立了一个坚实的基石，证明了因果模型背后的数学不仅是一个漂亮的构想，更是一个经过验证的、运作中的现实。

技术摘要：托波斯因果模型的立方形式化

问题与动机
本文旨在验证“托波斯因果模型”（Topos Causal Models, TCM）的验证工作。该框架由 Mahadevan [Mah25c, Mah25b, Mah25a] 提出，将因果推断重新构建在托波斯范畴内。在该框架中，一个因果世界是一个预层（presheaf），干预是进入子对象分类器 $\Omega$ 的特征映射，而推理则在直觉主义内部语言中进行。虽然源材料提供了一个概念性的重构，将标准的因果机制（干预、机制组装、反事实）对应于托波斯理论中的普遍性质，但这仍属于基于论文的理论发展。源材料中的一些核心主张是在没有证明的情况下陈述的，且部分公理过于抽象或可能存在不完整性。本文的任务是对这一 1-托波斯核心进行机器检查验证，以确保该框架的逻辑一致性，并识别原始公理化陈述中的任何缺陷。

方法论
作者在 Cubical Agda（一种基于立方类型论的证明助手）中实现了这一形式化。该开发工作是其伴随论文 [Sar26] 的直接后续，后者验证了概率单子和 Pearl 的 do-演算规则。

基础： 本工作运行在抽象基范畴 $\mathcal{C}$ （上下文范畴）上的预层托波斯 $\mathbf{PSh}(\mathcal{C}) = \mathbf{Set}^{\mathcal{C}^{op}}$ 之上。
安全性与公理： 整个开发过程在 Agda 的 --safe 标志下通过类型检查，这意味着它不包含任何假设（postulates）、空洞（holes）或不安全特性。底层的有序域被具体实例化为有理数 $\mathbb{Q}$ ，避免了抽象公理的使用。
结构： 该形式化构建了作为筛（sieves）之预层的 $\Omega$ ，定义了通过 Kripke-Joyal 强迫（forcing）实现的内部语言，并构造了一个 Lawvere-Tierney 拓扑来模拟 $j$ -do-演算模态。

主要贡献与结果

干预分类器（第 3 节）：
作者将 $\Omega$ 构建为筛的预层，并将干预 $do(X := x_0)$ 实现为特征映射 $\chi: X \to \Omega$ 。他们证明了双向的分类定理： $\chi_c(b) = \top \iff b = x_0^c$ 。至关重要的是，他们确立了为了使该构造在托波斯内部有效， $x_0$ 必须是一个自然全局元素（在上下文中具有自然性的值），而非仅仅是一个上下文索引的族。这证明了 $\Omega$ 是子对象分类器，满足了每一个限制封闭的子预层都由唯一映射到 $\Omega$ 的普遍性质。
独立机制的层叠粘合（第 4 节）：
源材料声称，在重叠部分一致的局部机制可以被“汇集”成唯一的全局机制，但未提供证明。作者证明了这在预层托波斯中是一个拉回极限（pullback limit）。他们证明了对于两个机制 $p: X \to Z$ 和 $q: Y \to Z$ ，其拉回 $X \times_Z Y$ 在上下文层面存在，且任何一致机制的锥（cone）都唯一地通过该拉回进行分解。这证实了“粘合”性质，且无需要求 Grothendieck 拓扑或层化（sheafification），因为这对于所有预层均成立。
内部语言（第 5 节）：
论文定义了用于内部逻辑的 Kripke-Joyal 强迫，并机器检查了所有联结词（ $\top, \bot, \land, \lor, \Rightarrow$ ）及量词（ $\forall, \exists$ ）的条款。他们验证了局部性（单调性）性质，确保强迫在限制下是稳定的，这是 Kripke 语义的定义特征。
Lawvere-Tierney 公理的修正（第 6 节）：
一个重要的发现是，作者指出源材料中对 Lawvere-Tierney 拓扑的标准定义存在缺陷。三个标准公理（保持 $\top$ 、保持 $\land$ 以及幂等性）并不蕴含扩张性（inflationarity， $S \leq j(S)$ ）。作者提供了一个满足这三个公理但扩张性失效的三元素链反例，这意味着该算子不一定是闭包算子。他们增加了扩张性作为第四个公理，以确保 $j$ 是一个闭包算子（nucleus）。
- 具体实例： 他们展示了双重否定拓扑（ $\neg\neg$ ）作为一个非退化的具体实例。
- 稳定性： 他们证明了干预和 Pearl 的三个 do-演算规则对于每一个拓扑都是 $j$ -封闭（stable）的。然而，他们指出对于结论为等式（真值 $\top$ ）的规则，这在本质上是平凡的。实质性的结果在于涉及权变主张（例如在某些机制下成立但在其他机制下不成立的条件独立性），证明了这些主张的真值在双重否定拓扑下是 $j$ -封闭的。
上下文阻碍（第 7 节）：
作者引入了一个原计划中未曾考虑的现象：粘合的上同调阻碍。虽然两个机制总是可以粘合，但三个上下文即使两两一致，也可能无法构成一个全局模型。他们通过机器检查了 Specker 三角形（三个具有两两反相关的布尔可观测变量）作为最小见证。
- 他们将该阻碍形式化为带有 $\mathbb{Z}_2$ 系数的第一个 Čech 上同调（ $H^1$ ）中的非零类。
- 他们证明，当且仅当前缀（cocycle）的全纯性（holonomy）是平凡的时，存在全局截面。Specker 三角形具有非平凡的全纯性，从而证实了全局模型的缺失。
可迁移性作为不变性（第 8 节）：
论文将反事实在覆盖机制范围内的可迁移性识别为具有 $j$ -稳定性（不变性）。一个反事实在全球范围内成立（是可迁移的），当且仅当其内部真值是 $j$ -封闭的。他们证明了可靠性：如果一个反事实是 $j$ -稳定的且在 $j$ -稠密环境中成立，则它在全球范围内成立。

意义与主张
该论文声称其意义主要体现在两个方面：

保证： TCM 框架的核心主张现在得到了认证而非仅仅是断言。这对于自动化至关重要，因为经过验证的核心是检查机器生成的因果模型所必需的。
实践发现： 机械化过程揭示了两个实际见解：
- 模态层的保证取决于 $j$ 是一个闭包算子；原有的公理是不充分的。
- 因果机制的模块化组装（类 map-reduce 风格）并不能仅靠两两一致性来保证；需要进行全局一致性检查以检测上同调阻碍（上下文性）。

范围与局限性
作者明确将范围限制在 1-托波斯（预层） 片段。

他们没有实现类型层级的层化（整个托波斯的关联层反射器）。
他们没有处理该框架的定向或 $\infty$ -范畴提升，因为这需要定向类型论来建模因果的方向不对称性（当前的预层模型中因果箭头是对称的）。
可迁移性的结果被确立为与特定稠密性假设下的不变性之间的等价关系，但其与图形化 $s$ -hedge 准则的完备性等价关系仍是未来的工作。

该开发工作是公开可用的，并且代表了对托波斯因果模型 1-托波斯核心的首次机器检查记录，修正了模态公理，并证明了此前未经验证的粘合与阻碍性质。