A wide range of neurosymbolic (NeSy) systems compute one functional: a belief-weighted sum of a logical quantity over a space of $σ$-structures, of which weighted model counting, fuzzy logic, and probabilistic logic are special cases. This account is built on sets, and a set deliberately forgets two things that are important for NeSy: when two $σ$-structures are the same up to a symmetry of the theory, and how many distinct proofs witness a query. Replacing the underlying sets by types, in the sense of homotopy type theory, preserves this information, and turns this functional into a belief-weighted homotopy cardinality, a notion of size that counts each object in inverse proportion to its symmetries. We develop the framework from scratch for NeSy systems, prove a conservativity theorem that recovers the classical functional when symmetries are trivial, and show that the symmetry our framework exposes is exactly the one behind reasoning shortcuts. The payoff is concrete: the shortcut-aware concept posterior that recent methods reach by ensembling or expressive density estimation is the only symmetry-invariant point of the confusion-set simplex, computable in closed form by averaging a single model over the symmetry group. On MNIST reasoning-shortcut benchmarks this single-model wrapper is better calibrated than a diversity-trained ensemble, while leaving label accuracy and identifiable concepts untouched. Code is freely available at https://github.com/bio-ontology-research-group/hott-nesy.

翻译：广泛的神经符号系统计算一种泛函：在σ-结构空间上对逻辑量进行置信加权求和，其中加权模型计数、模糊逻辑和概率逻辑均为特例。这种表示建立在集合论基础上，但集合有意忽略了神经符号系统中两个重要方面：两个σ-结构何时在理论对称性下等价，以及有多少个不同证明可验证一个查询。将底层集合替换为同伦类型论意义上的类型，能保留这些信息，并将该泛函转化为置信加权同伦基数——一种按对象对称性倒数计数的规模度量。我们从头构建了面向神经符号系统的理论框架，证明了当对称性平凡时恢复经典泛函的保守性定理，并揭示了该框架所暴露的对称性正是推理捷径背后的核心机制。其实际价值在于：最新方法通过集成或表达性密度估计实现的捷径感知概念后验，恰好是混淆集单纯形上唯一的对称不变点，可通过在对称群上取单个模型平均以闭式计算得到。在MNIST推理捷径基准测试中，这种单模型包装器相比多样性训练集成具有更好的校准性能，同时保持标签准确率和可识别概念不变。代码开源见https://github.com/bio-ontology-research-group/hott-nesy。