摘要
广泛的神经符号（NeSy）系统计算一个功能：在 $\sigma$-结构空间上的逻辑量的信念加权和，其中加权模型计数、模糊逻辑和概率逻辑是特殊情况。该描述基于集合，而集合故意忽略了对 NeSy 重要的两个方面：两个 $\sigma$-结构在理论对称性下是相同的，以及有多少个不同的证明见证一个查询。
通过将基础集合替换为类型，借助同伦类型理论的意义，保留了这些信息，并将这个功能转变为信念加权的同伦基数，这是一种大小的概念，按对称性反比计数每个对象。
我们为 NeSy 系统从头开发了该框架，证明了一个保守性定理，当对称性为平凡时恢复经典功能，并展示了我们框架所揭示的对称性正是推理捷径背后的原因。
其具体收益是：通过集成或表达密度估计所达到的捷径感知概念后验是混淆集单纯形中唯一的对称不变点，能够通过对对称群的单一模型平均计算出封闭形式。在 MNIST 推理捷径基准测试中，这个单一模型包装的校准效果优于多样性训练的集成，同时保持了标签准确性和可识别概念不变。
代码可在 GitHub 免费获取。
博主点评： 本文通过引入同伦类型理论为神经符号推理提供了新的视角，强调了对称性的重要性。该框架不仅理论上严谨，还通过实证结果展示了其在实际应用中的优势，具有重要的研究和应用价值。