Abstract
A wide range of neurosymbolic (NeSy) systems compute one functional: a belief-weighted sum of a logical quantity over a space of $\sigma$-structures, of which weighted model counting, fuzzy logic, and probabilistic logic are special cases. This account is built on sets, which deliberately forget two important aspects for NeSy: when two $\sigma$-structures are the same up to a symmetry of the theory, and how many distinct proofs witness a query.
By replacing the underlying sets with types in the sense of homotopy type theory, this information is preserved, turning 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 GitHub.
Blogger's Review: This paper provides a fresh perspective on neurosymbolic inference by introducing homotopy type theory, highlighting the significance of symmetry. The framework is not only theoretically rigorous but also demonstrates its practical advantages through empirical results, making it valuable for both research and application.