A homotopy-type-theoretic generalization of neurosymbolic inference

技术摘要：一种基于同伦类型论的神经符号推理泛化

问题陈述
当前的神经符号（NeSy）系统主要依赖于一个统一的泛函，该泛函定义为在 $\sigma$-结构空间（逻辑符号的值赋值空间）上对逻辑量进行信念加权求和。这个泛函通常被实例化为加权模型计数（WMC）、概率逻辑或模糊逻辑，它是在集合上运行的。作者认为，集合是“刻意遗忘”的对象，它们丢弃了对于结构化 NeSy 至关重要的两个关键信息：

1. 对称性（Symmetry）： 它们无法区分在理论的对称变换下（例如交换可互换的个体）是同构的 $\sigma$-结构。因此，标准的泛函会过度计算对称结构的贡献。
2. 证明多重性（Proof Multiplicity）： 它们将多个不同的推导过程坍缩为一个单一的数值，忽略了事实被证明的“方式之多”。

这种去范畴化（decategorification）导致了一种特定的失效模式，即推理捷径（reasoning shortcuts）。当模型仅针对逻辑输出进行训练时，它可能会收敛到一种错误的感知，即为潜在概念分配了错误的含义（一种“捷径”），同时保留了输出。标准方法难以识别正确的“捷径感知型”后验（即等价概念的置信分布），除非诉诸复杂的集成学习或表达能力强的密度估计。

方法论
本文建议使用来自同伦类型论（HoTT）的类型（types）来取代 NeSy 推理中底层的集合。在这个框架下，类型不仅记录其元素，还记录了识别这些元素的方式（同构）。

作者将标准 NeSy 泛函（公式 1）的四个组成部分向上提升了一个层级：

1. 结构空间 ($\Omega$)： 被替换为一个记录了身份类型（identity types）以保存对称性（个体的重命名）的类型。经典的集合结构是其 0-截断情况。
2. 逻辑函数 ($\ell$)： 被替换为一个证明族 $P: \Omega \to \mathcal{U}$。$P$ 的截断层级是一个设计参数：命题（层级 -1）检查满足性；集合（层级 0）计数推导过程；群组（层级 1）识别对称推导。
3. 推理： 被替换为信念加权同伦基数（belief-weighted homotopy cardinality）。它不再是简单的求和，而是计算：
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   它通过每个元素的对称群大小的倒数（$1/|Aut(x)|$）进行加权计数，确保对称结构对总量的贡献小于非对称结构。
4. 赋值（Valuation）： 选择交换半环（例如用于概率的 $(+, \times)$，或用于热带几何的 $(\max, +)$）决定了从同伦基数中读取哪种数值不变量。

核心贡献

1. 理论框架： 作者将 NeSy 推理形式化为信念加权同伦基数。该框架引入了经典公式中缺失的两个显式参数：一个对称性参数（定义允许重命名的群）和一个截断层级（定义追踪证明的粒度）。
2. 保守性定理： 一个经由 Lean 4 验证的机器检查定理证明，当对称性是平凡的（群为恒等映射）或半环是幂等的时，同伦基数会精确地坍缩为经典的基于集合的泛函。这确保了新框架是一个忠实的泛化。
3. 推理捷径即轨道（Orbits）： 本文将“混淆集”（产生相同输出的概念赋值集合）识别为理论对称群下的一个轨道。
   • “捷径感知型”的概念后验被识别为唯一的对称不变点：即轨道上的均匀分布。
   • 这引出了轨道平均法（Orbit-Averaging），这是一种计算该后验的闭式方法：
     $$\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$$
   • 该方法通过对单个基模型在输出保持群 $G$ 上进行对称化，实现了无需集成或密度估计的目标。
4. 生成函数： 对于可交换模型，该框架自然地产生指数生成函数（通过同伦基数），而非普通生成函数，这与组合物种（combinatorial species）理论相一致。

实验结果
作者在 MNIST 推理捷径基准测试（特别是具有已知对称群和地面真值概念可识别性的任务）上评估了轨道平均法。

• 设置： 单个神经网络被训练用于预测合并标签。任务旨在区分可识别数字（轨道大小为 1）和易混淆数字（轨道大小 > 1）。
• 对比： 将单模型轨道平均包装器与基模型以及一个多样性训练的 5 模型集成（Bears）进行了比较。
• 发现：
  • 基模型在易混淆数字上表现出过度自信（高期望校准误差，ECE）。
  • 轨道平均法在保持标签准确率和可识别概念校准的同时，将易混淆数字上的 ECE 从 0.614 降低到了 0.010。
  • 多样性训练的集成模型只有在牺牲标签准确率或导致可识别概念失准的情况下，才能达到类似的校准改善效果，这凸显了轨道平均法所避免的权衡问题。

意义与主张
本文声称，通过同伦类型论（HoTT）的角度来审视 NeSy 推理，可以获得“具体的收益”，因为它揭示了导致推理捷径的对称结构。

• 理论统一： 它将各种 NeSy 方法（概率、模糊、溯源）统一在一种更丰富的、结构化对象的去范畴化视角之下。
• 实际效率： 它证明了此前被认为需要昂贵集成才能实现的“捷径感知型”后验，可以通过在对称群上对单个模型进行平均来以闭式形式计算。
• 校准： 该方法在不降低可识别概念性能的前提下，改善了不可识别概念的校准。
• 局限性： 作者指出，目前的框架依赖于有限类型（$\pi$-finiteness）。通过“凝聚”（cohesion）将同伦基数扩展到连续域仍是一个开放性问题。

这项工作被呈现为从基于集合的推理向基于类型的推理的基础性转变，其中集合的“遗忘性”被类型所具备的结构化记忆所取代，直接解决了推理捷径的根源问题。