A homotopy-type-theoretic generalization of neurosymbolic inference

Sintesi Tecnica: Una Generalizzazione della Inferenza Neurosimbolica tramite la Teoria dei Tipi Omotopici

Enunciato del Problema
Gli attuali sistemi neurosimbolici (NeSy) si basano ampiamente su un funzionale unificato definito come una somma pesata di credenze di una quantità logica su uno spazio di $\sigma$-strutture (assegnazioni di valori a simboli logici). Questo funzionale, spesso istanziato come conteggio di modelli pesati (WMC), logica probabilistica o logica fuzzy, opera su insiemi. Gli autori sostengono che gli insiemi siano oggetti "deliberatamente dimenticosi" che scartano due informazioni critiche essenziali per la NeSy strutturata:

1. Simmetria: Non distinguono tra $\sigma$-strutture che sono identiche rispetto a una simmetria della teoria (ad esempio, scambiare individui intercambiabili). Di conseguenza, il funzionale standard sovraconta le strutture simmetriche.
2. Molteplicità di Dimostrazione: Collassano molteplici derivazioni distinte che testimoniano una query in un singolo numero, ignorando il "quante modi" un fatto sia provato.

Questa decategorizzazione porta a un modello di fallimento specifico noto come scorciatoie di ragionamento (reasoning shortcuts). Quando un modello viene addestrato solo su output logici, può convergere verso una percezione che assegna un significato errato ai concetti latenti (una "scorciatoia") pur preservando l'output. I metodi standard faticano a identificare il corretto posteriore "consapevole della scorciatoia" (una distribuzione uniforme sul set di confusione di concetti equivalenti) senza ricorrere a complessi ensemble o alla stima della densità.

Metodologia
Il paper propone di sostituire gli insiemi sottostanti della inferenza NeSy con i tipi della Teoria dei Tipi Omotopici (HoTT). In questo framework, un tipo ricorda non solo i suoi elementi, ma anche i modi in cui gli elementi possono essere identificati (isomorfismi).

Gli autori "elevano" i quattro ingredienti del funzionale NeS classico (Eq. 1) di un livello superiore:

1. Spazio delle Strutture ($\Omega$): Sostituito da un tipo in cui i tipi di identità registrano le simmetrie (rinomine degli individui). Il classico insieme delle strutture è il caso 0-troncato.
2. Funzione Logica ($\ell$): Sostituita da una famiglia di prove $P: \Omega \to \mathcal{U}$. Il livello di troncamento di $P$ è un parametro di design: una proposizione (livello -1) verifica la soddisfazione; un insieme (livello 0) conta le derivazioni; un groupoide (livello 1) identifica le derivazioni simmetriche.
3. Inferenza: Sostituita dalla cardinalità omotipica pesata dalle credenze. Invece di una semplice somma, il valore di inferenza è calcolato come:
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   Questo conta ogni elemento pesato dal reciproco della dimensione del suo gruppo di simmetria ($1/|Aut(x)|$), assicurando che le strutture simmetriche contribuiscano meno di quelle asimmetriche.
4. Valutazione: La scelta del semianello commutativo (ad es., $(+, \times)$ per la probabilità, $(\max, +)$ per il tropicale) determina quale invariante numerico viene letto dalla cardinalità omotipica.

Contributi Chiave

1. Framework Teorico: Gli autori formalizzano l'inferenza NeSy come una cardinalità omotipica pesata dalle credenze. Questo framework introduce due parametri espliciti assenti nelle formulazioni classiche: un parametro di simmetria (che definisce il gruppo di rinomine consentite) e un livello di troncamento (che definisce la granularità del tracciamento delle prove).
2. Teorema di Conservatività: Un teorema verificato meccanicamente (tramite Lean 4) dimostra che quando le simmetrie sono triviali (il gruppo è l'identità) o il semianello è idempotente, la cardinalità omotipica collassa esattamente nel funzionale classico basato sugli insiemi. Ciò garantisce che il nuovo framework sia una generalizzazione fedele.
3. Scorciatoie di Ragionamento come Orbite: Il paper identifica il "set di confusione" (l'insieme di assegnazioni di concetti che producono lo stesso output) come un'orbita sotto il gruppo di simmetia della teoria.
   • Il posteriore del concetto "consapevole della scorciatoia" è identificato come l'unico punto invariante per simmetria: la distribuzione uniforme sull'orbita.
   • Ciò porta all'Orbit-Averaging (media delle orbite), un metodo a forma chiusa per calcolare questo posteriore:
     $$\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$$
   • Questo metodo simmetrizza un singolo modello base sulla base del gruppo di output-preservazione $G$ senza richiedere un ensemble o la stima della densità.
4. Funzioni Generatrici: Per i modelli scambiabili, il framework produce naturalmente funzioni generatrici esponenziali (tramite la cardinalità omotipica) anziché funzioni generatrici ordinarie, allineandosi con la teoria delle specie combinatorie.

Risultati Sperimentali
Gli autori hanno valutato il metodo di orbit-averaging su benchmark di scorciatoie di ragionamento MNIST (specificamente compiti con gruppi di simmetria noti e ground truth per l'identificabilità del concetto).

• Setup: Una singola rete neurale è stata addestrata per predire etichette fuse. Il compito consisteva nel distinguere tra cifre identificabili (dimensione orbita 1) e cifre confondibili (dimensione orbita > 1).
• Confronto: Un singolo modello con wrapper di orbit-averaging è stato confrontato con un modello base e un ensemble di 5 modelli addestrati per la diversità (Bears).
• Risultati:
  • Il modello base era eccessivamente sicuro sulle cifre confondibili (alto Expected Calibration Error, ECE).
  • L'orbit-averaging ha ridotto l'ECE sulle cifre confondibili da 0.614 a 0.010, preservando l'accuratezza delle etichette e la calibrazione dei concetti identificabili.
  • L'ensemble addestrato per la diversità ha raggiunto miglioramenti simili nella calibrazione solo sacrificando l'accuratezza delle etichette o miscalibrando i concetti identificabili, evidenziando un compromesso che l'orbit-averaging del singolo modello evita.

Significatività e Rivendicazioni
Il paper sostiene che leggere l'inferenza NeSy attraverso la lente della HoTT fornisca un "guadagno concreto" esponendo la struttura di simmetria responsabile delle scorciatoie di ragionamento.

• Unificazione Teorica: Unifica varie approcci NeSy (probabilistici, fuzzy, provenienza) sotto una visione decategorizzata di un oggetto più ricco e strutturato.
• Efficienza Pratica: Dimostra che il posteriore "consapevole della scorciatoia", precedentemente ritenuto richiedere un costoso ensembling, può essere calcolato in forma chiusa mediando un singolo modello sul gruppo di simmetria.
• Calibrazione: Il metodo migliora la calibrazione sui concetti non identificabili senza degradare le prestazioni su quelli identificabili, risolvendo un fallimento specifico dell'apprendimento NeSy.
• Limitazioni: Gli autori notano che l'attuale framework si basa su tipi finiti ($\pi$-finiteness). Estendere la cardinalità omotipica a domini continui tramite la "coesione" rimane un problema aperto.

Il lavoro è presentato come un cambiamento fondamentale dai ragionamenti basati su insiemi a quelli basati su tipi, dove la "dimenticanza" degli insiemi è sostituita dalla memoria strutturale dei tipi, affrontando direttamente le cause profonde delle scorciatoie di ragionamento.