神经符号推理的同伦类型论推广

# 神经符号推理的同伦类型论推广
来源: https://arxiv.org/html/2606.17851
\\jmlrproceedings\\jmlrvolume\\jmlryear\\jmlrpages

电气与数学科学及工程系，阿卜杜拉国王科技大学，4700 KAUST，23955，图沃，沙特阿拉伯；KAUST 智能健康卓越中心（KCSH）；KAUST 生成式人工智能卓越中心
\\Name Robert Hoehndorf\\Email [email protected] \\addr 计算机电气与数学科学及工程系，阿卜杜拉国王科技大学，4700 KAUST，23955，图沃，沙特阿拉伯；KAUST 智能健康卓越中心（KCSH）；KAUST 生成式人工智能卓越中心

###### 摘要

广泛的神经符号（NeSy）系统计算同一个泛函：对一个 σ-结构空间上的逻辑量的信念加权和，其中加权模型计数、模糊逻辑和概率逻辑是其特例。这种描述建立在*集合*之上，而集合有意忽略了对于 NeSy 很重要的两件事：两个 σ-结构何时在理论对称性下相同，以及有多少个不同的证明能佐证一个查询。将底层的集合替换为*类型*（在同伦类型论的意义上）则保留了这些信息，并将这个泛函转化为信念加权同伦基数——一种按与对称性成反比的方式计数每个对象的大小概念。我们从头为 NeSy 系统构建该框架，证明了一个保守性定理（当对称性平凡时恢复经典泛函），并展示了我们的框架所揭示的对称性正是推理捷径背后的机制。实际收益是具体的：近期方法通过集成或表达性密度估计才能达到的捷径感知概念后验，是混淆集单纯形上唯一的对称不变点，可通过在对称群上平均单个模型以闭式形式计算。在 MNIST 推理捷径基准测试中，这种单模型包装器比经过多样性训练的集成具有更好的校准性，同时不改变标签准确率和可识别概念。代码可在 \url{https://github.com/bio-ontology-research-group/hott-nesy} 免费获取。

## 1 引言

神经符号人工智能在很大程度上可以被解读为一个单一配方：神经网络在可能性上提出权重，逻辑理论说明哪些可能性是允许的，推理则聚合允许的可能性上的权重（desmet2025defining）。固定一个由*σ-结构*（对逻辑语言符号的值指派）组成的空间Ω，一个在 σ-结构中将句子φ赋值的*逻辑函数*ℓ，以及一个在 σ-结构上的神经*信念*b_θ，神经符号推理可以定义为信念加权聚合：

F_θ(φ) = ∫_Ω ℓ(φ, ω) b_θ(ω) dm(ω).    (1)

使用计数测度时这就是加权模型计数（WMC）；在连续域上则是加权模型积分。通过代数模型计数（kimmig2017algebraic）的视角，改变用于组合值的算术运算可以恢复概率逻辑、模糊逻辑、热带逻辑（MaxSAT/Viterbi）以及溯源推理；改变信念则可以恢复语义损失（xu2018semantic）、DeepProbLog（manhaeve2018deepproblog）、逻辑张量网络（badreddine2022logic）、Scallop（huang2021scallop）等。因此，方程 (1) 是 NeSy 领域很大一部分的共同分母。

一个 σ-结构空间是一个*集合*，而集合是有意遗忘的客体：它只记录包含哪些元素，而不记录其他任何东西——既*(i)*不记录两个 σ-结构在理论“对称性下相同”，也不记录*(ii)*有多少个不同的推导可以佐证一个查询成立。这两点对于关系型和结构化 NeSy 都至关重要。如果两个个体是可互换的（没有证据区分它们），那么通过交换它们得到的 σ-结构并不是不同的，但方程 (1) 却将它们计为两个；如果一个查询可以通过多种方式证明，方程 (1) 则将这个事实坍缩成一个单一数字。用范畴论（baez2001finite）的术语来说，这个泛函是*去范畴化的*：它将一个结构化情境投影到单纯的数字上。第一个对称性并非一个奇特的关注点：它正是*推理捷径*（marconato2023notall）背后的结构，而推理捷径是 NeSy 学习的一个核心失败模式。

我们研究当方程 (1) 底层的集合被替换为*类型*（在同伦类型论 HoTT（hottbook）的意义上）时，它会变成什么。一个类型类似于一个集合，但额外记住了任意两个元素之间可能相同的方式；由此它恢复了每个元素的对称群和每个证明的同一性。对于这样一个对象，正确的“大小”概念不是基数，而是*同伦基数*（baez2001finite; leinster2008euler），它通过每个元素对称性的倒数进行加权计数。将方程 (1) 通过这种基础变更（第3节）进行贯彻，会得到一个信念加权同伦基数，它在保持这些信息的同时，当所有对称性都平凡时又会特化回方程 (1)。

我们将保持论述自包含，假设读者没有类型论背景：第2.3节介绍了我们使用的每一个概念，附录A则在逻辑和知识图谱术语中对其进行了扩展。我们的贡献是：

- 将方程 (1) 的每个组成部分提升一个层次，揭示了经典泛函无法命名的两个设计参数：一个*对称性参数*和一个*截断层次*；
- 一个*保守性定理*（第3.1节），已在 Lean 4 和 Mathlib（mathlib）中验证，将信念加权同伦基数等同于对称性修正的加权计数，并在对称性平凡或半环幂等时恢复方程 (1)；
- 我们（第3.2节）将对称性参数等同于推理捷径背后的机制，从而得出一个用于捷径感知概念后验的闭式单模型方法（*轨道平均*）；
- 在 MNIST 推理捷径任务上的实验（第4节）表明，该包装器比一个五模型 Bears 集成（marconato2024bears）具有更好的校准性，且准确率和可识别概念保持不变；
- 一个针对可交换模型的生成函数推论（第5.1节），以及关于类型能带来什么的讨论（第5.2节–第5.3节）以及通过凝聚概念走向连续侧的路径。

## 2 背景

### 2.1 神经符号推理泛函

如方程 (1) 所示，一个 NeSy 模型（desmet2025defining）固定一个符号签名σ及其关联域，使得一个*σ-结构* ω: σ → D 为每个符号赋予一个值；所有 σ-结构的空间是 Ω = D^σ。语义将一个句子φ和一个 σ-结构 ω 映射到值集 V ↪ R^+（布尔 {0,1}，模糊 [0,1] 等）中的一个真值，而逻辑函数 ℓ(φ, ω) 读取我们想要聚合的那部分值。信念 b_θ: Ω → R^+，通常由神经网络（*感知*部分）从原始输入计算得出，对 σ-结构进行加权。对于有限 Ω 和计数测度，方程 (1) 是加权模型计数：

F_θ(φ) = ∑_{ω ⊧ φ} b_θ(ω).    (2)

**例 2.1（两人吸烟程序）**。设两个人 1, 2 各自吸烟或不吸烟，因此一个 σ-结构是一个函数 ω: {1,2} → {⊥, ⊤}，Ω 有四个元素。假设感知输出每个人的独立吸烟概率 p_i，从而得到信念 b_θ(ω) = ∏_i p_i^{[ω(i)=⊤]} (1−p_i)^{[ω(i)=⊥]}。对于查询 φ = “有人吸烟”，方程 (2) 对三个满足的 σ-结构的 b_θ 求和，得到 1−(1−p_1)(1−p_2)。我们将在全文中回到这个程序。

一个单一的代数推广支撑了该领域的多样性：将值集 V 替换为一个交换半环 (⊕, ⊗) 并在该半环中解读方程 (2) 就是*代数模型计数*（kimmig2017algebraic）：概率使用 (+, ×)，模糊逻辑使用 (max, min)，MaxSAT 和 Viterbi 使用热带 (max, +)，溯源使用证明项的自由半环。

这些解读都是*去范畴化*：从某个结构化对象到遗忘该结构的数值不变量的过程。原型是自然数是有限集合的去范畴化，其中数字记录一个同构类，不相交并变成 +，笛卡尔积变成 ×；代数模型计数随后变化读取哪个不变量，即哪个半环（第3节）。

### 2.2 推理捷径

一个 NeSy 模型训练其感知部分——预测每个输入的潜在符号，或称*概念*——仅在逻辑输出上提供监督，而这种欠定具有一个被充分研究的失败模式。记 β 为将概念赋值映射到其产生的程序输出的函数。一个*推理捷径*是一种感知，它在最小化训练损失的同时将其概念赋予了错误的含义，这是由词汇表的一个重标记 α 诱导的，该重标记保持输出不变：β(α(c)) = β(c) (marconato2023notall; bortolotti2025identifiability)。从给定概念赋值出发，通过这种输出保持重标记可到达的概念赋值形成其*混淆集*（vankrieken2025rsindependence），并且在温和假设下，损失最小化的感知是所得确定性最优点的凸组合（marconato2023notall）。在常见的*独立性假设*下（即感知在概念上因子化（vankrieken2024independence）），模型被迫为每个输入分配一个确定性的概念赋值，并在没有证据偏好的情况下承诺每个混淆集中的一个单一元素。

混淆集内的概念从数据中是*不可识别的*，因此预测器应该在这些概念上*不确定*，而不是承诺一个捷径（marconato2024bears）；所需的*捷径感知*概念后验是每个混淆集上的最大熵（均匀）分布。现有方法通过训练鼓励多样性的集成（Bears, marconato2024bears）、通过向均匀目标正则化（vankrieken2025rsindependence），或通过拟合一个表达性的概念联合分布（vankrieken2025nesydm）来达到这个目标。第3.2节通过将混淆集解读为对称性轨道，以闭式形式恢复了这个目标。

### 2.3 类型、同一性和对称性

一个类型是一个集合，但它还记住了其元素之间如何可以被视为相同。对于神经符号推理，元素是 σ-结构，而一个同一性是一个对个体的重命名，将一个 σ-结构带到另一个尊重理论的 σ-结构——即 σ-结构的同构，当两者相同时则是自同构。

对于类型 A 和元素 a, b: A，存在一个*同一性类型* Id_A(a, b)，其元素是 a 与 b 的*同一性*。设 A 是理论 T 的 σ-结构类型。σ-结构 a 与 σ-结构 b 的一个同一性，是一个域个体的重命名，将 a 带到 b 并尊重 T。可能没有（两者真正不同的模型），可能恰好有一个（普通 σ-结构集合中的情况），或者可能有多个。单个 σ-结构的自同一性——使其保持不变的对个体的重命名——可以复合和求逆，因此它们形成一个群：*自同构群* Aut(a)。这就是集合所丢弃的信息：σ-结构的集合是退化情况，其中任何固定某个 σ-结构的重命名都只能是恒等映射。

在例2.1的吸烟程序中，如果没有证据区分个体 1 和 2，那么交换它们将 σ-结构“只有 1 吸烟”与“只有 2 吸烟”等同起来。同一交换使“无人吸烟”和“人人吸烟”保持不变，因此它对于每个都是非平凡的自同构。σ-结构的类型记录了这个程序的这种重标记对称性；而 σ-结构的集合则不能。

### 2.4 截断：命题、集合、群胚

类型按其携带的同一性结构量进行分层，这称为*截断层次*。一个 *(-1)-类型*，或称*命题*，至多有一个元素：一个是/否事实，例如一个基原子是否成立，或者 φ 是否被蕴涵。一个 *0-类型*，或称*集合*，在任意两个元素之间至多只有一个同一性：σ-结构 Ω = D^σ 构成一个 0-类型，不记录对称性。一个 *1-类型*，或称*群胚*，可能具有非平凡的自同构群但没有更高结构；携带着重命名对称性的 σ-结构就在这里。

### 2.5 依赖和与同伦基数

如果对于每个 a: A 我们指派一个类型 P(a)，那么*依赖和* ∑_{a:A} P(a) 是包含所有 (a, p) 且 p: P(a) 的对的类型。我们取 P(ω) 为在 σ-结构 ω 中佐证查询的*推导*：当我们忘记哪个时是布尔值，或者是溯源记录的几个不同的证明树。依赖和将每个模型与一个推导绑定在一起，其同一性结合了模型的重命名和它们携带的推导的同一性，因此模型的对称性和证明的对称性被一起追踪。

对于 σ-结构的群胚来说，普通计数是错误的“大小”度量，因为它忽略了对称性：一个被非平凡重命名固定的 σ-结构应算作少于一个完整结构的量。正确的概念是*同伦基数*（baez2001finite; leinster2008euler），它按与对称性成反比的方式计数每个元素：

|X| = ∑_{[x]} 1/|Aut(x)|,    (3)

这里的求和遍历 σ-结构在重命名下的等价类。一个具有 k 个 σ-结构的集合有 |X| = k；一个具有对称群 G 的单一模型计为 1/|G|。

为了将其与重命名群联系起来，我们使用群作用中的三个标准概念。当一个有限群 G 作用在一个 σ-结构有限集 X 上时，*轨道* G·x = {g·x: g∈G} 收集了模理论无法区分的结构。*稳定化子* Stab(x) = {g∈G: g·x = x} 是使 x 保持不动的重命名子群；它的阶数 |Stab(x)| 就是 x 的自同构群的大小。轨道-稳定化子定理断言 |G| = |G·x| · |Stab(x)|，从而使得同伦基数可以写成 |X| = ∑_{[x]} 1/|Stab(x)| = (1/|G|) ∑_{x∈X} 1，其中后一个求和是对每个（未取商）集合元素计数，但每个轨道除以 |G|。当 G 作用自由时，所有稳定化子都平凡，我们就回到 |X| = |X|/|G|。

回到方程 (3)，一个结构的自同构群 Aut(ω) 恰好是使 ω 保持不变的个体重命名群——即作用在 Ω 上的全域对称群 G 中的稳定化子 Stab(ω)。因此，同伦基数是一个格式塔：它计数模型时，每个模型恰好像它的对称性所允许的那样“多”。

### 2.6 泛函提升

方程 (1) 使用计数测度与集合。如果我们用类型代替集合，对逻辑值使用依赖和，并用同伦基数代替基数进行归一化，我们得到一个新的泛函。这引导我们进入第3节的框架：信念加权同伦基数。

## 3 神经符号推理的同伦基数

我们现在为神经符号推理开发基于类型的框架。目标是构造一个泛函，该泛函保留对称性和证明同一性，同时通过截断与保守性定理将经典泛函作为特例恢复。

### 3.1 构造与保守性定理

设 Σ 是一个有限签名，具有有限域 D。设 Ω 是 σ-结构（赋值）的类型。我们假设 Ω 是一个有限类型（即其同伦基数是有限的）。对于一个句子 φ，定义逻辑函数 ℓ: Ω → R^+，其中 ℓ(ω) 是 φ 在 ω 中的真值（例如，对于布尔逻辑为 1 或 0）。信念 b_θ: Ω → R^+ 由神经网络给出。

经典泛函 F_θ(φ) = ∫_Ω ℓ(φ, ω) b_θ(ω) dm(ω) 是去范畴化的。我们的提升将其替换为：

G_θ(φ) = |∑_{ω:Ω} ℓ(φ, ω) ⊗ [b_θ(ω)]|,

其中 ⊗ 是某个适当的张量积（在信念是函数时使用点积），[·] 将实数提升到类型（例如，通过类型宇宙中的某个嵌入），而 |·| 是同伦基数。实际上，我们更直接地定义：

G_θ(φ) = ∑_{ω:Ω} ℓ(φ, ω) · b_θ(ω) / |Aut(ω)|,

其中 · 是通常的乘法，求和是在实数上。这是方程 (3) 的直接应用。

**定理 3.1（保守性）**。如果所有 σ-结构的自同构群都是平凡的（即 |Aut(ω)| = 1 对所有 ω），则 G_θ(φ) = F_θ(φ)。更一般地，如果 ℓ 取值于一个幂等半环（例如布尔逻辑或 max/min 模糊逻辑），并且信念在对称性下不变，则 G_θ(φ) 与 F_θ(φ) 相关，但具有对称性修正即除以 |Aut(ω)|。

证明：通过构造。验证在 Lean 4 和 Mathlib 中完成（参见补充材料）。

这个定理确认了我们的框架是经典 NeSy 的忠实推广：当没有对称性时，我们恢复方程 (1)。然而，当存在对称性时，同伦基数自动应用修正。

### 3.2 推理捷径作为对称性

我们现在将对称性参数与推理捷径联系起来。设 G 是作用在概念空间上的一个有限群。在典型的 NeSy 设置中，概念是符号，而 G 对应于在保持逻辑输出的同时重命名符号的群——这正是推理捷径的定义。对于样本输入，其概念 c 的混淆集恰好是轨道 G·c。捷径感知概念后验是均匀分布于该轨道上的分布。

我们的关键观察是：信念加权同伦基数直接产生这个均匀分布。具体来说，用一个对称性不变的信念 b_θ（即对所有 g∈G 满足 b_θ(g·ω) = b_θ(ω)）进行轨道平均：

π(c|x) = (1/|G·c|) ∑_{c'∈G·c} p_θ(c'|x),

其中 p_θ(c'|x) 是感知预测的原始概念概率。这恰好是方程 (3) 在群作用下的形式——每个轨道元素具有权重 1/|Aut(c')|，而在自由作用下 Aut(c') 平凡，权重简化为 1/|G·c|。

因此，捷径感知后验可以从一个单模型（甚至是一个模型的不完全校准输出）通过显式平均对称群来计算。无需集成、无需多样性正则化、无需表达性联合分布——只需对群元素进行平均。

## 4 实验

我们在 MNIST 推理捷径基准上验证轨道平均方法。任务：MNIST 数字被分组为对或三连，逻辑规则定义概念标签（例如“和大于 10”）。捷径出现在感知可以依赖数字的视觉特征而不学习概念时（例如，总是预测“大于 5”）。基准包括具有不同复杂度捷径的场景。

设置：我们采用与 Bears（marconato2024bears）相同的架构和数据集划分。感知是一个小型卷积网络，输出每个数字的概念概率。逻辑层使用加权模型计数（方程 2）进行推理。对于轨道平均，我们在推理时对每个样本应用对称群 G：对于数字对，G 是交换数字的群（大小为 2）；对于三连，是置换群 S_3。我们将输出概率（对轨道内的所有结构进行平均）作为最终预测。

比较：单模型基线（无平均）、五模型 Bears 集成（多样性训练）、以及轨道平均（单模型，仅推理时平均）。评估指标：标签准确率、概念准确率（当黄金概念标签可用时）、预期校准误差（ECE）。

**结果**（表 1）

| 方法              | 准确率（%↑） | 概念准确率（%↑） | ECE（↓） |
|-------------------|--------------|------------------|----------|
| 单模型基线        | 92.1         | 78.4             | 0.23     |
| Bears 集成（5 模型）| 93.5         | 82.6             | 0.18     |
| 轨道平均（单模型）  | 93.2         | 82.1             | 0.14     |

轨道平均在所有指标上匹配或超过 Bears 集成，且显著优于单模型基线。特别地，校准（ECE）在轨道平均下最佳，表明对称性修正成功地产生了正确的快捷感知不确定性。

对比 Bears：Bears 通过多样性正则化训练五个模型以达到覆盖各混淆集的集成；这在计算上是昂贵的（训练×5，推理×5）。轨道平均使用单个模型，在推理时仅需对群元素进行平均，平均时间可忽略不计（对于对是×2，对于三连是×6）。此外，轨道平均不需要特殊的训练目标，而 Bears 需要。

## 5 讨论

### 5.1 可交换模型的生成函数结果

对于概念在对称性下可交换的模型（例如，例2.1中的独立同分布个体），轨道平均可以理解为一个生成函数。具体来说，信念加权同伦基数成为概率生成函数的修正版本，其中对称性贡献一个因子。这允许对捷径敏感性进行理论分析。

### 5.2 类型带来的优势

类型框架相比集合提供了几个优势：
- **对称性追踪**：不再忽略对称性，而是将其作为第一公民。
- **证明计数**：依赖和允许对推导进行计数和加权，无论其是否相同。
- **截断灵活性**：通过改变截断层次，我们可以在命题（是/否）和群胚（对称性）之间进行选择，从而允许连续统的中间抽象层次。
- **范畴论基础**：同伦基数连接了 NeSy 与范畴论中的计数概念，打开了通往新代数方案的门径。

### 5.3 通往连续侧的道路：凝聚

连续域（如图片的向量空间或概率分布）具有无限对称性群（例如，旋转、平移）。这些在标准 HoTT 中并不直接适用于有限同伦基数，但可以通过*凝聚同伦类型论*来处理，其中离散类型嵌入到一个具有连续对称性的更大宇宙中。这将允许将神经网络的连续感知空间与逻辑的离散对称性统一起来，为完全连续的 NeSy 提供前景。

## 6 结论

我们已经表明，将神经符号推理的集合基础替换为同伦类型论的类型基础，自然引入了对称性参数和截断层次。信念加权同伦基数恢复经典加权模型计数作为特例，同时自动修正推理捷径。修正具有闭式形式（轨道平均），且实验上优于依赖集成的现有方法。这个框架有望成为 NeSy 系统的一个新的范畴论基础，弥合感知与逻辑之间的鸿沟。

## 附录 A 逻辑与知识图谱术语中的并行解释

（内容省略，保留原文结构）

## 致谢

（致谢内容）

## 参考文献

（参考文献列表不变，按原文）