A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

技术摘要：条件独立性、贝叶斯后验与 Pearl d-分离性的立方形式化

问题陈述
本文解决了概率推理形式化验证中的一个基础性空白：自 Stone 以来，概率单子（probability-monad）形式化中通用的标准凸代数交换公理（convex-algebra interchange axiom），在证明上过于微弱，无法支持完整的贝叶斯后验（Bayesian conditioning）。虽然经典的 Coq 形式化将条件独立性（CI）视为实值概率之间的命题等价，但这些方法依赖于经典逻辑和外延性，通常需要正性假设以及对非零概率的除法运算，才能推导出诸如交集公理（intersection axiom）之类的结构性结果。此外，将递归贝叶斯后验提升为分布的高阶归纳类型（HIT）表示时，揭示了一个结构性失配：标准的交换公理假设重新排列混合物时具有单一的共享内权重，而贝叶斯后验自然产生的是通过贝叶斯公式相关联的、具有不同内权重的混合物。

方法论
作者在 Cubical Agida 中开发了一种构造性形式化，利用了 立方类型论（Cubical Type Theory） 和 高阶归纳类型（HITs）。该方法依赖于从经典方法向三个结构性转变：

1. 作为 HIT 的概率单子： 有限分布（FDist）被定义为一个由点质量（point masses）和二元加权混合操作生成的 HIT。标准的凸代数律（幂等性、斜交换性、边界情况、交换律和斜结合律）被施加为路径构造器（path constructors）。这使得分布等价性可以被视为可运行的变换（路径），而非不透明的命题等价。
2. 结构化条件独立性： CI 被定义为分布核之间的路径（kXY z ≡ kX z ⊗D kY z），而非实数之间的逐点相等。这实现了组合式推理，使得 CI 见证（witnesses）可以被传递到单子操作中。
3. 构造性权重处理： 开发过程对抽象的 Weight 签名（一个具有可判定序的有理域）具有多态性，并在有理数（$\mathbb{Q}$）处进行具体实例化。这避免了构造性实数中相等性的不可判定性，并允许显式处理正性和除法。

核心贡献与结果

• 交换失配与泛化： 核心技术发现是，标准的交换公理（中性律）不足以支持完整的贝叶斯后验。对一个 4 叶混合物进行后验处理会产生两个具有不同权重（$q_1$ 和 $q_2$）的内半部分，这两个权重通过贝叶斯公式相关联，而标准公理则要求它们必须相同（$q_1 = q_2$）。作者引入了一个广义交换公理（mix-bayes-interchange），允许不同的内权重。作者证明了标准形式是这两个权重相等的退化情形。
• 构造性交集公理： 本文通过将其归约为收缩（contraction），提供了交集公理的构造性证明。该证明并非通过贝叶斯提取（即除法），而是使用因子分解的结构性 $\Sigma$-类型见证和条件变量的填充假设。这为任何具体的正分布模型恢复了交集公项的完整内容，而无需额外公理。
• Pearl do-演算验证： 在小型结构因果模型（SCM）的核层级上验证了 Pearl do-演算的所有三条规则：
  • 规则 1 & 3： 被验证为单子律和 constBind 引理（对独立变量的干预不改变边缘分布）的推论。
  • 规则 2： 在混杂 SCM 上通过表明联合先验进行因式分解的结构性 CI 见证进行了验证。这确立了干预与条件化在独立性下的等价性。
• 递归贝叶斯后验： 在全支撑（full-support）分片的 HIT 上定义了一个用于递归贝叶斯后验的全函数。作者完成了将此函数提升到完整 HIT 所需的所有六个相干性义务。第五个相干性（交换性）必须依赖于前述的广义公理。
• 马尔可夫范畴对齐： FDist 单子被验证为 马尔可夫范畴（根据 Fritz 和 Cho–Jacobs 的定义）的一个具体实例。通过 HIT 归纳证明了非平凡的 delete-naturality 公理（总质量守恒），确认了路径构造器正确捕捉了随机归一化。
• D-分离健全性： 对于任意有限有向无环图（DAG），本文构造性地验证了 Pearl d-分离定理的健全性。这涵盖了干预形式（针对多元素集合 $X, Y, Z$）和贝叶斯形式（针对基本模式），是通过祖先因子分解而非逐路径约简推导出的。

意义与主张
本文声称提供了在这一通用程度下，完全在类型论框架内进行的关于 Pearl d-分离定理健全性方向的第一个构造性、机器检查的形式化。

• 计算内容： 与 CI 作为一种断言的经典形式化不同，立方方法产生了计算内容。CI 见证是可运行的变换；后验分布是由 Agda 标准化器计算的、可执行的项。
• 基础性修正： 本研究指出，概率单子的标准代数基础对于贝叶斯后验而言“过于微弱”。所提出的对交换公理的泛化被视为任何旨在支持完整贝叶斯推理的单子框架中必要的结构性精炼。
• 验证 Mahadevan 的堆栈： 本文验证了 Mahadevan 的拓扑因果模型（TCM）框架的“底层”。它确认了 do-演算的核形式恒等式和交换分布单子在构造性意义下成立，为构建基于层（sheaves）和强制语义（forcing semantics）的拓扑理论机制提供了经过验证的基质。
• 零公理化： 包括 d-分离健全性和贝叶斯后验在内的整个开发过程，在高于抽象有序域接口（实例化为 $\mathbb{Q}$）的情况下，是在零公理下完成验证的。这包括移除了此前使用的不安全界限，并用构造性的、受正性保护的操作取代了经典除法。

本文结论认为，条件独立性和后验的构造性内容最好不是通过经典逻辑加外延性来捕捉，而是通过立方类型论中的结构化、基于路径的推理来捕捉，其中概率的代数律是其类型的内在属性。