Alpha内测版本警告:此为早期内部构建版本,尚不完整且可能存在错误,欢迎大家提Issue反馈问题或建议。
Skip to content

番外:从理论到代码——CocDo 神经因果算子

理论告诉你因果推断是什么。代码告诉你它是怎么做成的。


推理王国的兔狲小思考:从理论到代码,我们到底在翻译什么?

上卷13章讲完了理论:因果边界、注意力机制、搜索艺术、推理极限。现在的问题是:这些理论如何变成可运行的代码?

这看起来是个工程问题,但它在第一行代码之前就有一个根本障碍:数学结构和计算结构之间的翻译会丢失什么?

线性注意力是个绝佳的例子。它的代数核心是 Monoid(幺半群)——前缀和结合律允许 O(logT) 并行扫描,轻松甩掉 O(T2) 的复杂度诅咒。这是数学结构直接给出计算红利。

但 Monoid 没有逆元。一旦 ktvt 被加进状态矩阵 S,它就和其他所有历史贡献永久混叠,无法单独取出。而 Pearl 的 do 算子要求:切断变量 X 的所有入边,其他边不动。 翻译到状态矩阵的语言就是:从 S 里减去某个特定 token 的外积贡献。这在 Monoid 里根本无法表达——不是实现困难,是代数结构上缺少"撤销"操作。

这是数学结构和因果语义之间的根本错位:Monoid 的优雅来自结合律,因果推断的精确来自可逆性。两者在代数层面不相容。

于是你面临选择:保留 Monoid 的复杂度优势,放弃 do 算子的完整语义;或者放弃 Monoid,保留 do 算子,承担 O(n2) 的存储代价。

Spartacus 模型选了第一条路,在 Monoid 内部把记忆机制做到极致:向量衰减门让不同维度有独立的记忆寿命,快衰减维负责局部句法,慢衰减维负责长程实体记忆。它证明了即使不升级到 Group,向量化的衰减结构已经能逼近"可寻址记忆"的行为。

CocDo 选了第二条路:放弃压缩历史,保留完整的因果邻接矩阵 A,让每条边有名字、有地址、可以被单独切断。代价是 O(n2) 的图存储;换来的是 do 算子的完整语义。

这两条路的分叉点,正是 Monoid 有没有逆元。

但这不是故事的终点。从理论到代码的翻译还会暴露其他错位:类型系统如何排除循环?β-归约如何对应结构方程传播?梯度下降如何成为 do 算子的逆?注意力机制和因果发现是什么关系?

这些问题的答案不在理论里,在代码里。这一章展示 CocDo——一个把 Pearl 因果演算和 COC 类型论融合的神经因果模型库。它不是玩具实现,而是一个可以在真实数据上训练、干预、规划的完整系统。

翻译的过程会丢失一些优雅,会引入一些妥协,但也会暴露出理论里看不见的结构——比如"注意力矩阵就是软因果邻接矩阵",比如"梯度规划是搜索的微积分版本",比如"系统可以用自身做知识图谱"。

理论告诉你因果推断是什么。代码告诉你它是怎么做成的——以及为什么有些事,在现有数学结构里,根本做不成。


上卷走过了13章:从熵增与预测(第1章),到符号系统的天花板(第2章),再到因果的边界(第6章)、注意力机制(第9章)、搜索的艺术(第10章),最后在推理的边界前停下(第13章)。

这些理论如何变成可运行的代码?

这一章展示 CocDo——一个把 Pearl 因果演算和 COC 类型论融合的神经因果模型库。它不是玩具实现,而是一个可以在真实数据上训练、干预、规划的完整系统。

从理论到代码的翻译过程,会暴露一些在纯数学里看不见的问题:类型系统如何在结构层面排除循环?β-归约和矩阵传播是什么关系?梯度下降如何成为 do 算子的逆?注意力机制和因果发现是什么关系?


23.1 类型系统排除循环

第6章说因果图必须无环——因果不能成圈,否则时间上就出现了悖论。但"无环"在代码里怎么保证?

传统做法是运行时检查:构造完图之后,跑一遍拓扑排序或 DFS,发现环就报错。问题是,这个错误发生在你已经花了很多时间构造图、训练模型之后。

CocDo 用类型系统在编译时排除循环。核心思想只有一句话:

每条因果边 XY 被编码为依赖 Pi 类型 Π(X:Typei).Typej,要求 i<j

什么是依赖类型论(CoC)?

构造演算(Calculus of Constructions,CoC) 是类型论的一种,类型本身也可以依赖值。

关键概念:

  • Sort(宇宙)Sort(i) 表示第 i 层的类型宇宙,Sort(0) 是最基础的类型层
  • Pi 类型Π(x:A).B 是依赖函数类型——"对于类型 A 的任意 x,返回类型 B"
  • 层级约束:CoC 要求类型宇宙严格分层,Sort(i) 的类型是 Sort(i+1),防止自指悖论

CocDo 借用这个结构:每个因果节点被分配一个层级 i,Pi 类型的层级约束 i<j 自动等价于"因果图无环"。

ij 是拓扑序中的层级——根节点是 Type0,它的子节点是 Type1,以此类推。要求 i<j 意味着:一条边只能从低层指向高层

循环图意味着什么?意味着存在一条路径 XX,使得 X 的层级既要小于某个中间节点,又要大于它。这在类型系统里是矛盾的——不是运行时错误,而是类型检查失败:

python
from cocdo.kernel.terms import Sort, Pi, Var
from cocdo.kernel.typing import type_of, Context

# 合法的边:X(层级0) → Y(层级1)
ctx: Context = {"X": Sort(0), "Y": Sort(1)}
edge = Pi("X", Sort(0), Sort(1))   # ✓ 0 < 1

# 非法的边:Y(层级1) → X(层级0),构成循环
bad_edge = Pi("Y", Sort(1), Sort(0))  # type_of 会拒绝这个

这个设计的意义不只是工程上的防御。它说的是:因果图的无环性不是一个运行时检查,而是一个类型不变量。一个带循环的因果模型,在 CocDo 里根本无法被构造出来——就像在强类型语言里,你无法把字符串赋值给整数变量。

类型系统把约束从"运行时崩溃"提升到"编译时拒绝"。这不是技术细节,这是认识论的一步:你不是在检查模型是否合法,你是在让非法模型无法被表达。第14章说形式系统的价值是消除歧义;这里的价值是消除一整类错误的可能性。


23.2 do() 的实现:λ 演算的项替换

第6章定义了 do 算子——"把 X 的结构方程替换为常数 X=v,删除所有入边,沿后代传播效应"。这个定义是数学的,但在代码里怎么实现?

在 λ 演算里,这个操作有一个精确的名字:捕获避免替换(capture-avoiding substitution),记作 [v/X]M——把项 M 里所有自由出现的变量 X 替换为 v

β-归约和捕获避免替换:λ-演算的两个核心操作

**β-归约(Beta Reduction)**是 λ-演算的核心计算规则:

(λx.M)N[N/x]M

读作:把函数 (λx.M) 应用到参数 N,等于把 M 里所有的 x 替换为 N。这是"运行一个函数"的最基本步骤。

捕获避免替换 [N/x]M:在 M 里把自由变量 x 替换为 N,但需要小心:如果 M 里有 λx.(另一个绑定了同名变量 x 的函数),不能进入那个内层替换——否则会把本来属于外层的 x 和内层的 x 混淆,产生语义错误。"捕获避免"就是指避免这种意外绑定。

在 CocDo 里的意义do(X=v) 的语义恰好就是"把因果图里 X 的结构方程替换为常数 v"——这正是捕获避免替换。替换之后运行 beta_reduce,就是"沿拓扑序把效应传播到后代节点"。Pearl 的数学定义和 λ-演算的计算语义,在这里完美对应。

CocDo 的实现:

python
def subst(term, var: str, replacement):
    """把 term 里所有自由出现的 var 替换为 replacement。"""
    if isinstance(term, Var):
        return replacement if term.name == var else term
    elif isinstance(term, Lam):
        if term.var == var:          # 绑定变量遮蔽,停止替换
            return term
        return Lam(term.var, term.domain, subst(term.body, var, replacement))
    elif isinstance(term, App):
        return App(subst(term.func, var, replacement),
                   subst(term.arg,  var, replacement))
    return term  # Const, Sort 不含自由变量

"捕获避免"处理的是一个微妙的情况:如果 M 里有一个 λ 绑定了和 X 同名的变量,替换不应该进入那个绑定的作用域——否则会把本来指向外部的 X 错误地替换掉。代码里的 if term.var == var: return term 就是这个检查。

替换之后,需要 β-归约 把结果化简到正常形式:

python
def beta_reduce(term, steps=100):
    """按值调用归约到不动点。"""
    for _ in range(steps):
        reduced = _step(term)
        if reduced is term:   # 不动点:无法继续归约
            break
        term = reduced
    return term

_step 的核心规则是 β-规约:(λx.M)N[N/x]M——把函数应用化简为替换。当 Add/Mul 的两个操作数都是带值的 Const 时,归约器直接计算:

App(App(Mul, Const(w=0.9)), Const(v=3.0))  →  Const(2.7)

这意味着结构方程 Ej=iAijEi+Uj 的传播,发生在项语言内部,不是一次独立的矩阵乘法。do 算子的语义和计算语义是同一件事。

Pearl 的操作λ 演算操作
X 的方程替换为 X=vsubst(mechanism, "X", Const(v))
删除 X 的所有入边替换后父节点项消失,不再出现在归约路径上
沿后代传播效应beta_reduce 按拓扑序归约到不动点
循环图非法Pi 类型要求层级严格递增,循环是 TypeError

23.3 NOTEARS:从数据学习因果结构

第6章说"观测数据永远不够"——因为相关性不等于因果性。但我们还是要从数据学习因果结构,这就是因果发现问题。

传统方法(PC 算法、FCI)是组合搜索——在所有可能的 DAG 里找最符合数据的那个。节点数 n 时,DAG 的数量是超指数的,搜索代价极高。

2018 年,Zheng 等人提出了 NOTEARS,把"是否是 DAG"这个离散约束转化为一个连续可微的等式约束

h(A)=tr(eAA)n=0A 是 DAG

其中 AA 是逐元素平方,eM 是矩阵指数。这个等式成立当且仅当 A 是有向无环图。

NOTEARS:用矩阵指数把"是否无环"变成连续优化(前人工作:Zheng et al., 2018)

因果发现的传统困难:要在所有可能的 DAG(有向无环图)里找最符合数据的那个。n 个节点的 DAG 数量是超指数级的——暴力搜索完全不可行。

NOTEARS 的关键思想:把"是 DAG"这个离散约束,转化成一个光滑的连续等式:

h(A)=tr(eAA)n=0
  • A 是边权重矩阵,A[i,j] 表示边 ij 的权重
  • AA 是逐元素平方(让负值也变正)
  • eM(矩阵指数)的迹 tr(eM)n,等号成立当且仅当矩阵无环

有了这个连续约束,因果发现变成了梯度优化问题——可以用 Adam 等标准优化器直接求解,不需要组合搜索。这是让因果结构学习在神经网络框架里变得可行的关键一步。

CocDo 对稀疏图用 AF2 近似,避免矩阵指数数值溢出。

有了这个约束,因果发现变成了带等式约束的连续优化:

minALrecon(A)+λh(A)+ρ2h(A)2
重建损失 Lrecon 是什么?

重建损失衡量学到的因果权重矩阵 A 对数据的解释能力。

在线性结构方程模型(SEM)假设下,每个变量是其父节点的线性组合加噪声:X=XA+ϵ。因此,如果 A 是真实因果图的权重矩阵,XA 应该近似重建 X 本身:

Lrecon(A)=1NXXAF2

这是一个最小二乘目标——让因果图"解释"数据的程度最大化。单独最小化它会让 A 退化为全连接图(完美解释但不是 DAG),所以必须配合无环约束 h(A)=0 联合优化。

增广拉格朗日法(Augmented Lagrangian)

标准拉格朗日法处理等式约束 h(A)=0

L(A,λ)=f(A)+λh(A)

但纯拉格朗日法数值不稳定,乘子 λ 很难收敛。增广拉格朗日法加入一个二次惩罚项:

L(A,λ,ρ)=f(A)+λh(A)+ρ2h(A)2

算法交替进行两步:

  1. 固定 λ,ρ,对 A 做梯度下降(内层优化)
  2. 更新乘子:λλ+ρh(A);如果约束收敛太慢,增大 ρ

ρ 越大,无环约束的惩罚越强,A 被迫向 DAG 靠近。代码里每50步检查一次 h(A) 是否充分下降,不够就把 ρ 乘以10。

用增广拉格朗日法求解,每隔若干步收紧乘子 λ 和惩罚系数 ρ。下面是 CocDo 在合成数据上的完整训练循环(来自 examples/demo_gcastle.py):

python
# 用 gCastle 生成 5 节点线性高斯 DAG,1000 个样本
from castle.datasets import DAG, IIDSimulation
true_dag = DAG.erdos_renyi(n_nodes=5, n_edges=6, seed=42)
dataset  = IIDSimulation(W=true_dag, n=1000, method="linear", sem_type="gauss")
X = dataset.X  # (1000, 5)

# 训练 CausalFFNN 学习因果权重矩阵 A
ffnn = CausalFFNN(d_embed=32, hidden=128)
rho, lam = 1.0, 0.0

for epoch in range(500):
    A, _ = ffnn(E_raw)
    recon = ((X @ A - X) ** 2).mean()
    h = acyclicity_loss(A)  # ≈ tr(e^{A∘A}) - n
    loss = recon + lam * h + (rho / 2) * h ** 2
    loss.backward(); optim.step()
    
    # 每 50 步收紧约束
    if (epoch + 1) % 50 == 0:
        lam += rho * h.item()
        if h > 0.25 * h_prev:
            rho = min(rho * 10, 1e6)

训练完成后,A 就是学到的因果权重矩阵。CocDo 会自动从 A 提取拓扑序(Kahn 算法),构造 NeuralSCM

注意力即因果发现。 CausalFFNN 用低秩双线性打分:

score(ij)=(Wqhi)(Wkhj)r

这和 Transformer 注意力在数学上完全相同。区别只有两点:用 sigmoid 而非 softmax(边独立竞争),以及对角线强制为零(变量不能是自身的原因)。

Transformer 的注意力头在计算"token i 对 token j 的影响权重"——这正是因果权重矩阵 A[i,j] 的定义。区别在于 Transformer 没有施加无环约束,也没有用 do-calculus 解释这些权重。CocDo 把这两件事补上了。

抽象代数插曲:为什么线性注意力天生无法做 do 算子(没错,又是兔狲的研究)

标准注意力每步要访问完整的 KV 缓存,代价是 O(T) 的存储。线性注意力的出发点是把整个因果历史压缩进一个固定大小的状态矩阵 St

St=diag(αt)St1+ktvt,ot=qtSt

这个递推式背后有一个代数结构。定义二元算子:

(α,S)(β,X)=(αβ,diag(β)S+X)

这个算子满足结合律,单位元是 (1,0)。满足结合律 + 单位元,这就是 Monoid

结合律带来的工程红利是直接的:训练时可以做 O(logT) 深度的并行前缀扫描,推理时每步只做 O(1) 的状态更新。线性注意力能跑起来,Monoid 是代数层面的根本原因。

但 Monoid 没有逆元。

Group(群)= Monoid + 逆元。矩阵加法群里,S+(S)=0,你可以"撤销"一次更新。Monoid 里没有这个操作——一旦 ktvt 被加进 St,它和之前所有 token 的贡献就永久混在一起,无法单独取出,无法单独切断。

Pearl 的 do 算子要求:切断变量 X 的所有入边,其他边不动。 翻译到状态矩阵的语言就是:从 St 里减去某个特定 token 的外积贡献 kjvj。这在 Monoid 里根本无法表达——不是实现困难,是代数结构上的缺失。

Spartacus 在这个框架里走得更远:它用向量衰减替代标量衰减,αt(0,1)d 让每个特征维度有独立的记忆寿命——快衰减维负责局部句法,慢衰减维负责长程实体记忆。衰减门用 sigmoid 激活,偏置初始化为 3.0(使 σ(3)0.95),模型从"几乎全记住"开始训练。填充位置(PAD)被设计为 Monoid 的单位元:α=1,k=v=0,状态矩阵原封不动地穿过,批处理时的不等长序列对递推完全透明。

这是在 Monoid 结构内部把记忆机制做到极致的一次尝试。它没有解决 do 算子的问题——因为 Monoid 本身不允许解决。但它证明了:即使不升级到 Group,向量化的衰减结构已经能让不同维度分别承担不同的时间尺度,逼近"可寻址记忆"的行为,而不需要真正寻址。

CocDo 选择了另一条路:放弃压缩历史,保留完整的因果邻接矩阵 A,让每条边有名字、有地址、可以被单独切断。代价是 O(n2) 的图存储;换来的是 do 算子的完整语义。

两条路的分叉点,正是 Monoid 有没有逆元。

Spartacus 的完整实现与模型权重见 NoesisLab/Spartacus-1B-Instruct


23.4 梯度规划:搜索的微积分版本

第10章讲搜索的艺术——在巨大的推理空间中导航。传统搜索是采样:试很多次,记住哪次好。梯度规划是微积分:沿梯度方向走。

do 算子是正向的:给定干预值 v,计算结果 Y。实践中更常见的问题是反向的:给定目标 Y=y,找到最优干预值 v

v=argminvj(Enext[j]yj)2

其中 Enext 是 do 算子传播后的嵌入状态,用 L2 范数而非全向量比较,消除方向对齐问题。

CausalPlanner 的核心是一个可微的单步传播:

python
# do-calculus 在嵌入空间的实现:
A_do  = A * (1 - col_mask)      # 把干预节点的入边列清零
E_do  = (1 - row_mask) * E + row_mask * interv_E   # 注入干预值
E_next = A_do.T @ E_do + U      # 结构方程传播

然后对干预值 a 求梯度,用 Adam 优化:

python
a = torch.tensor([0.0], requires_grad=True)
opt = torch.optim.Adam([a], lr=0.05)
for _ in range(200):
    E_next = planner._step(a, interv_nodes, E_init)
    energy = ((E_next[target_idx].norm(dim=-1) - scalar_targets) ** 2).sum()
    energy.backward(); opt.step()

整个计算图从目标一路反传到干预值,不需要采样,不需要强化学习。

强化学习把规划变成采样问题:试很多次,记住哪次好。梯度规划把规划变成微积分问题:沿梯度方向走。后者需要可微的世界模型——这正是神经 SCM 提供的。代价是世界必须可微,或者至少可以被可微模型近似。这个假设不总成立,但在嵌入空间里通常足够好。


23.5 CausalSearch:系统用自身做知识图谱

第13章讲推理的边界,提到系统开始推理关于自身——这是自指的开始。CausalSearch 是一个具体的自指应用:用推理王国的章节作为因果知识图谱

前四节处理的是"变量"——标量或向量,有明确的数值含义。但知识也可以是因果结构的节点:一个段落依赖另一个段落,一个概念建立在另一个概念之上。

demo_causal_search.py 把推理王国的全部章节(22章,约1800段)用 BGE 嵌入,训练 CausalFFNN 学习段落间的因果权重矩阵 A,然后用 Pearl 三步法做检索:

第一步:溯因(Abduction)——找到与查询最近邻的段落 j

第二步:行动(Action)——do(j=query_emb):注入查询向量,清零 j 的入边。

第三步:预测(Prediction)——Enext=AdoEdo+U;按 ΔEnext 排序所有节点。

Δ = 下游激活(查询触发的知识链);负 Δ = 上游前提(理解查询所需的概念)。

查询:"Transformer 注意力与贝叶斯推断的关系"

[向量检索 RAG]
  1. ch9·Transformer 的成功触发了...  cos=0.763
  2. ch9·注意力作为因果性...          cos=0.682

[CausalSearch · Pearl 三步]
  溯因锚点 → ch9·Transformer 的成功...

  + 下游激活:
    ch17·贝叶斯更新与 ch14 的比较...  Δ=+2.69e-02
    ch20·PAC 与贝叶斯:ch17 的延续... Δ=+2.34e-02

  * CausalSearch 独有(RAG 遗漏):
    ch17 贝叶斯推断 ×4,ch1 生成模型层,ch19 证明...

向量检索找的是"表面相似";CausalSearch 找的是"因果相关"——沿学到的因果边传播,而不是在嵌入空间里量距离。

RAG 是第一层阶梯:关联。CausalSearch 是第二层:干预。你问的不是"哪些段落和这个查询相似",而是"如果我把这个查询注入知识图谱,哪些节点会被激活"。这是两个完全不同的问题,只是碰巧都叫"检索"。


23.6 回顾:从理论到代码的映射

上卷走到这里,可以画一条完整的线:

上卷章节核心问题在 CocDo 里的对应
第6章 因果的边界观测数据推不出因果NOTEARS: 从数据学习 DAG 结构
第6章 do 算子干预 vs 观测subst + beta_reduce = do 算子的实现
第9章 Transformer注意力机制的数学结构CausalFFNN: 低秩双线性打分
第9章番外 注意力即因果注意力矩阵是软因果邻接矩阵sigmoid 边权重,对角线强制为零
第10章 搜索的艺术在推理空间中导航CausalPlanner: 梯度规划,不是采样
第13章 推理的边界系统推理关于自身CausalSearch: 用自身章节做知识图谱

这不是巧合。上卷的每一章都在问:推理是什么,它的边界在哪里,它如何在现实约束下工作? CocDo 是这些问题的一个可运行的回答——不完整,但诚实。

形式化的价值不只是数学上的严格,还在于它可以被实现。COC 类型系统让循环成为类型错误,NOTEARS 让离散搜索变成梯度优化,这些都是形式化带来的工程红利。


思考题

★ 热身

  1. 在 CocDo 里,为什么用 sigmoid 而不是 softmax 计算边权重 A[i,j]?这个选择对因果图的稀疏性有什么影响?
  2. subst 函数里的"捕获避免"处理的是什么情况?举一个如果不做这个检查会出错的例子。

★★ 推导

考虑三节点图 XYZ,结构方程为:

EY=wXYEX+UY,EZ=wYZEY+UZ
  1. 手动计算 do(X=v)EZ 的值(用 wXY,wYZ,v,UY,UZ 表示)。
  2. 用 CocDo 的 step 方法验证你的计算,设 rollout_steps=2。为什么需要 rollout_steps=2 而不是 1?
  3. 如果只用 rollout_steps=1EZ 的值会是什么?这对应 Pearl 阶梯的哪一层?

★★★ 挑战

NOTEARS 的无环约束 h(A)=tr(eAA)n=0 是一个充要条件。CocDo 用 AF2 作为近似。

  1. 证明:AF2=0A=0(平凡 DAG)。这说明近似在什么情况下是精确的?
  2. 构造一个非零的 DAG(至少有一条边),使得 h(A)=0AF2>0。这说明近似在什么情况下会失效?
  3. 在实际训练中,重建损失 Lrecon 会推动 A 解释数据,而 AF2 会推动 A 趋向零。这两个力的平衡点是什么?它和 L1 正则化有什么关系?