A homotopy-type-theoretic generalization of neurosymbolic inference

Résumé Technique : Une généralisation de l'inférence neurosymbolique par la Théorie des Types Homotopiques

Énoncé du Problème
Les systèmes neurosymboliques (NeSy) actuels reposent largement sur un fonctionnel unifié défini comme une somme pondérée par la croyance d'une quantité logique sur un espace de $\sigma$-structures (assignations de valeurs à des symboles logiques). Ce fonctionnel, souvent instancié sous forme de comptage de modèles pondérés (WMC), de logique probabiliste ou de logique floue, opère sur des ensembles. Les auteurs soutiennent que les ensembles sont des objets « délibérément amnésiques » qui perdent deux informations critiques essentielles pour une NeSy structurée :

1. Symétrie : Ils ne parviennent pas à distinguer les $\sigma$-structures qui sont identiques à une symétrie de la théorie près (par exemple, l'échange d'individus interchangeables). Par conséquent, le fonctionnel standard surcompte les structures symétriques.
2. Multiplicité de Preuve : Ils réduisent plusieurs dérivations distinctes témoignant d'une requête à un seul nombre, ignorant le « de combien de manières » un fait est prouvé.

Cette décatégorisation entraîne un mode d'échec spécifique appelé raccourcis de raisonnement (reasoning shortcuts). Lorsqu'un modèle est entraîné uniquement sur des sorties logiques, il peut converger vers une perception qui assigne une mauvaise signification aux concepts latents (un « raccourci ») tout en préservant la sortie. Les méthodes standard peinent à identifier le postérieur « conscient du raccourci » (une distribution uniforme sur l'ensemble de confusion des concepts équivalents) sans recourir à des ensembles complexes ou à une estimation de densité expressive.

Méthodologie
Le papier propose de remplacer les ensembles sous-jacents de l'inférence NeSy par des types issus de la Théorie des Types Homotopiques (HoTT). Dans ce cadre, un type se souvient non seulement de ses éléments, mais aussi des manières dont ces éléments peuvent être identifiés (isomorphismes).

Les auteurs « élèvent » les quatre ingrédients du fonctionnel NeSy standard (Éq. 1) d'un niveau supérieur :

1. Espace de Structure ($\Omega$) : Remplacé par un type où les types d'identité enregistrent les symétries (renommages d'individus). Le $\sigma$-structure classique est le cas 0-tronqué.
2. Fonction Logique ($\ell$) : Remplacée par une famille de preuves $P: \Omega \to \mathcal{U}$. Le niveau de troncature de $P$ est un paramètre de conception : une proposition (niveau -1) vérifie la satisfaction ; un ensemble (niveau 0) compte les dérivations ; un groupoïde (niveau 1) identifie les dérivations symétriques.
3. Inférence : Remplacée par la cardinalité homotopique pondérée par la croyance. Au lieu d'une simple somme, la valeur d'inférence est calculée comme :
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   Ceci compte chaque élément pondéré par l'inverse de la taille de son groupe de symétrie ($1/|Aut(x)|$), garantissant que les structures symétriques contribuent moins que les structures asymétriques.
4. Valuation : Le choix du semi-anneau commutatif (ex: $(+, \times)$ pour la probabilité, $(\max, +)$ pour le tropical) détermine quel invariant numérique est lu de la cardinalité homotopique.

Contributions Clés

1. Cadre Théorique : Les auteurs formalisent l'inférence NeSy comme une cardinalité homotopique pondérée par la croyance. Ce cadre introduit deux paramètres explicites absents des formulations classiques : un paramètre de symétrie (définissant le groupe de renommages autorisés) et un niveau de troncature (définissant la granularité du suivi de preuve).
2. Théorème de Conservativité : Un théorème vérifié par machine (vérifié dans Lean 4) prouve que lorsque les symétries sont triviales (le groupe est l'identité) ou que le semi-anneau est idempotent, la cardinalité homotopique se réduit exactement au fonctionnel classique basé sur les ensembles. Cela garantit que le nouveau cadre est une généralisation fidèle.
3. Raccourcis de Raisonnement comme Orbites : Le papier identifie l'« ensemble de confusion » (l'ensemble des assignations de concepts produisant la même sortie) comme une orbite sous le groupe de symétrie de la théorie.
   • Le postérieur de concept « conscient du raccourci » est identifié comme l'unique point invariant par symétrie : la distribution uniforme sur l'orbite.
   • Cela mène à la Moyenne d'Orbite (Orbit-Averaging), une méthode en forme close pour calculer ce postérieur :
     $$\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$$
   • Cette méthode symétrise un modèle de base unique sur le groupe $G$ préservant la sortie sans nécessiter d'ensemble ou d'estimation de densité.
4. Fonctions Génératrices : Pour les modèles échangeables, le cadre produit naturellement des fonctions génératrices exponentielles (via la cardinalité homotopique) plutôt que des fonctions génératrices ordinaires, s'alignant sur la théorie des espèces combinatoires.

Résultats Expérimentaux
Les auteurs ont évalué la méthode de moyenne d'orbite sur des benchmarks de raisonnement de raccourcis MNIST (spécifiquement des tâches avec des groupes de symétrie connus et une vérité terrain pour l'identifiabilité des concepts).

• Configuration : Un réseau de neurones unique a été entraîné pour prédire des étiquettes fusionnées. La tâche consistait à distinguer des chiffres identifiables (taille d'orbite 1) et des chiffres confondables (taille d'orbite > 1).
• Comparaison : Le wrapper de moyenne d'orbite d'un modèle unique a été comparé à un modèle de base et à un ensemble de 5 modèles entraînés pour la diversité (Bears).
• Constats :
  • Le modèle de base était surconfiant sur les chiffres confondables (Erreur de Calibration Attendue, ECE élevée).
  • La moyenne d'orbite a réduit l'ECE sur les chiffres confondables de 0,614 à 0,010 tout en préservant la précision des étiquettes et la calibration des concepts identifiables.
  • L'ensemble entraîné pour la diversité n'a atteint des améliorations de calibration similaires qu'en sacrifiant la précision des étiquettes ou en mal-calibrant les concepts identifiables, soulignant un compromis que la moyenne d'orbite d'un modèle unique évite.

Signification et Revendications
Le papier affirme que lire l'inférence NeSy à travers le prisme de la HoTT offre un « gain concret » en exposant la structure de symétrie responsable des raccourcis de raisonnement.

• Unification Théorique : Il unifie diverses approches NeSy (probabilistes, floues, provenance) sous une vue décatégorisée d'un objet plus riche et structuré.
• Efficacité Pratique : Il démontre que le postérieur « conscient du raccourci », auparavant considéré comme nécessitant un ensemblage coûteux, peut être calculé en forme close en moyennant un modèle unique sur le groupe de symétrie.
• Calibration : La méthode améliore la calibration sur les concepts non identifiables sans dégrader les performances sur les concepts identifiables, résolvant un mode d'échec spécifique de l'apprentissage NeSy.
• Limites : Les auteurs notent que le cadre actuel repose sur des types finis ($\pi$-finitude). Étendre la cardinalité homotopique aux domaines continus via la « cohésion » reste un problème ouvert.

Ce travail est présenté comme un changement fondamental, passant d'un raisonnement basé sur les ensembles à un raisonnement basé sur les types, où l'« amnésie » des ensembles est remplacée par la mémoire structurelle des types, s'attaquant directement aux causes profondes des raccourcis de raisonnement.