同伦类型论视角下的神经符号推理：从集合到对称性不变量

背景

神经符号（Neurosymbolic, NeSy）人工智能系统旨在结合深度学习的感知能力与符号逻辑的推理能力。当前，广泛使用的 NeSy 系统通常计算一个特定的函数：在 $\sigma$-结构（$\sigma$-structures）空间上，对某个逻辑量进行信念加权求和。加权模型计数（Weighted Model Counting）、模糊逻辑（Fuzzy Logic）和概率逻辑（Probabilistic Logic）均为此函数的特例。

然而，现有的 NeSy 框架建立在经典集合论（Sets）基础之上。集合论在处理 NeSy 任务时，有意或无意地忽略了两个关键信息：

1. 对称性：当两个 $\sigma$-结构在理论对称性下被视为相同时，集合论无法区分这种“等价”与“同一”。
2. 证明的多样性：集合论不记录有多少个不同的证明（proofs）可以支持同一个查询（query）。

这种信息的丢失导致模型在处理具有对称性的逻辑结构时，无法准确反映其内在的不确定性，进而可能产生推理捷径（reasoning shortcuts），即模型利用数据中的非因果相关性而非真正的逻辑规则进行预测。

核心内容

本文提出了一种基于同伦类型论（Homotopy Type Theory, HoTT）的神经符号推理泛化框架。该框架的核心思想是用“类型”（Types）替代传统的“集合”（Sets），从而保留结构中的对称性和证明信息。

1. 从集合到类型：保留对称性信息

在经典集合论中，两个元素要么相同，要么不同。但在同伦类型论中，类型不仅包含元素，还包含元素之间的“路径”或“等价关系”。当我们将底层结构从集合替换为类型时，系统能够感知到两个 $\sigma$-结构是否通过理论的对称性相互关联。

2. 信念加权同伦基数（Belief-Weighted Homotopy Cardinality）

随着底层结构的改变，NeSy 系统的核心计算函数也随之演变。新的函数不再是简单的加权求和，而是转化为信念加权同伦基数。

• 定义：同伦基数是一种度量集合（或类型）大小的概念。它通过对每个对象进行加权来计算总数，其中权重与该对象的对称性数量成反比。
• 直观理解：如果一个对象具有高度的对称性（即存在多个自同构将其映射到自身），它在同伦基数中的贡献会被稀释。这反映了这样一个事实：对称性高的对象在逻辑空间中提供的“独特信息量”较少。

3. 保守性定理与推理捷径

作者从基础出发构建了适用于 NeSy 系统的框架，并证明了以下关键性质：

• 保守性定理（Conservativity Theorem）：当对称性平凡（即没有非平凡的自同构）时，新的同伦基数框架退化为经典的信念加权求和函数。这意味着新框架是经典框架的自然推广，而非完全颠覆。
• 对称性与推理捷径的关系：框架所暴露出的对称性，正是导致传统 NeSy 系统出现“推理捷径”的根本原因。传统模型往往因为忽略了结构的对称性，而错误地将对称等价的状态视为独立证据，从而高估了某些假设的可信度。

4. 具体应用：对称性感知的概念后验

该框架的实际收益是具体的。在近期的研究中，通过集成学习（Ensembling）或高表达能力密度估计（Expressive Density Estimation）得到的“对称性感知的概念后验”（Shortcut-aware concept posterior），被证明是混淆集单纯形（Confusion-set simplex）中唯一的对称性不变点。

• 计算方法：这一后验分布可以通过对单个模型在对称群（Symmetry Group）上进行平均，以封闭形式（Closed Form）计算得出。
• 实验结果：在 MNIST 推理捷径基准测试中，这种基于单模型的封装方法（Single-model wrapper）在校准度（Calibration）上优于经过多样性训练的集成模型，同时保持了标签准确率（Label Accuracy）和可识别概念（Identifiable Concepts）不受影响。

关键要点

• 理论革新：利用同伦类型论（HoTT）中的“类型”概念替代经典集合论，解决了 NeSy 系统中对称性和证明多样性信息丢失的问题。
• 新计算范式：将传统的信念加权逻辑量求和泛化为“信念加权同伦基数”，该基数通过逆比例于对称性数量来计数对象，从而更准确地反映逻辑空间的度量。
• 解释捷径根源：证明了传统 NeSy 系统中的推理捷径本质上源于对结构对称性的忽视；同伦框架显式地建模了这种对称性。
• 计算效率与性能：
  • 无需复杂的集成学习或高密度估计，仅通过对单个模型在对称群上取平均，即可计算出对称性感知的概念后验。
  • 在 MNIST 基准测试中，该方法在保持准确率和概念可解释性的同时，显著提升了模型的校准度，优于多样性集成模型。
• 理论完备性：通过保守性定理证明，当对称性不存在时，新框架等价于经典方法，确保了理论的一致性。

意义与影响

这项工作在神经符号人工智能的理论基础和应用实践上均具有重要意义：

1. 统一了逻辑与几何视角：通过引入同伦类型论，文章在逻辑推理中引入了几何直观（如对称性、路径等价），为理解逻辑结构提供了更丰富的数学工具。
2. 提升了模型的可靠性：推理捷径是 NeSy 系统面临的主要挑战之一，它导致模型在分布外（OOD）数据上表现不佳。通过显式建模对称性，该方法提高了模型校准度，使模型输出更符合其真实的不确定性估计，增强了系统的可信度。
3. 简化了工程实现：以往为了消除推理捷径，研究者往往需要设计复杂的集成方案或密度估计模型。本文证明，通过对称群平均，单模型即可达到类似甚至更好的效果，降低了计算复杂度和工程实现难度。
4. 开源贡献：代码的公开（Code is freely available）为后续研究提供了基准，有助于社区进一步探索同伦类型论在其他 AI 领域的应用。

总之，这篇论文不仅提供了一个更严谨的 NeSy 推理框架，还通过具体的实验验证了其在解决长期存在的推理捷径问题上的有效性，为构建更鲁棒、更可解释的神经符号系统指明了新方向。