A homotopy-type-theoretic generalization of neurosymbolic inference

Resumen Técnico: Una generalización de la inferencia neurosimbólica mediante la Teoría de Tipos Homotópicos

Planteamiento del problema
Los sistemas neurosimbólicos (NeSy) actuales dependen en gran medida de un funcional unificado definido como una suma ponderada por creencias de una cantidad lógica sobre un espacio de $\sigma$-estructuras (asignaciones de valores a símbolos lógicos). Este funcional, a menudo instanciado como conteo de modelos ponderados (WMC), lógica probabilística o lógica difusa, opera sobre conjuntos. Los autores argumentan que los conjuntos son objetos que "olvidan deliberadamente", ya que descartan dos piezas críticas de información esenciales para la NeSy estructurada:

1. Simetría: No logran distinguir entre $\sigma$-estructuras que son idénticas hasta una simetría de la teoría (por ejemplo, intercambiar individuos intercambiables). En consecuencia, el funcional estándar sobrecuenta las estructuras simétricas.
2. Multiplicidad de pruebas: Colapsan múltiples derivaciones distintas que dan testimonio de una consulta en un único número, ignorando "de cuántas maneras" se prueba un hecho.

Esta decategorificación produce un modo de fallo específico conocido como atajos de razonamiento (reasoning shortcuts). Cuando un modelo se entrena únicamente con salidas lógicas, puede converger a una percepción que asigna el significado erróneo a conceptos latentes (un "atajo") mientras preserva la salida. Los métodos estándar tienen dificultades para identificar el posterior "consciente del atajo" (una distribución uniforme sobre el conjunto de confusión de conceptos equivalentes) sin recurrir a complejos ensambles o estimación de densidad expresiva.

Metodología
El artículo propone reemplazar los conjuntos subyacentes de la inferencia NeSy por tipos de la Teoría de Tipos Homotópicos (HoTT). En este marco, un tipo recuerda no solo sus elementos, sino las formas en que estos pueden identificarse (isomorfismos).

Los autores "elevan" los cuatro ingredientes del funcional NeSy estándar (Ec. 1) un nivel hacia arriba:

1. Espacio de estructuras ($\Omega$): Reemplazado por un tipo donde los tipos de identidad registran simetrías (renombramientos de individuos). El conjunto clásico de estructuras es el caso de truncamiento 0.
2. Función lógica ($\ell$): Reemplazada por una familia de pruebas $P: \Omega \to \mathcal{U}$. El nivel de truncamiento de $P$ es un parámetro de diseño: una proposición (nivel -1) verifica la satisfacción; un conjunto (nivel 0) cuenta derivaciones; un grupoide (nivel 1) identifica derivaciones simétricas.
3. Inferencia: Reemplazada por la cardinalidad homotópica ponderada por creencias. En lugar de una simple suma, el valor de la inferencia se calcula como:
   $$N(P, b) = \left\| \sum_{\omega:\Omega} P(\omega) \right\|_{V,b}$$
   Esto cuenta cada elemento ponderado por el recíproco del tamaño de su grupo de simetría ($1/|Aut(x)|$), asegurando que las estructuras simétricas contribuyan menos que las asimétricas.
4. Valoración: La elección del semianillo conmutativo (por ejemplo, $(+, \times)$ para probabilidad, $(\max, +)$ para tropical) determina qué invariante numérico se lee de la cardinalidad homotópica.

Contribuciones clave

1. Marco teórico: Los autores formalizan la inferencia NeSy como una cardinalidad homotópica ponderada por creencias. Este marco introduce dos parámetros explícitos ausentes en las formulaciones clásicas: un parámetro de simetría (que define el grupo de renombramientos permitidos) y un nivel de truncamiento (que define la granularidad del seguimiento de pruebas).
2. Teorema de conservatividad: Un teorema verificado por máquina (verificado en Lean 4) demuestra que cuando las simetrías son triviales (el grupo es la identidad) o el semianillo es idempotente, la cardinalidad homotópica colapsa exactamente al funcional basado en conjuntos clásico. Esto asegura que el nuevo marco sea una generalización fiel.
3. Atajos de razonamiento como órbitas: El artículo identifica el "conjunto de confusión" (el conjunto de asignaciones de conceptos que producen la misma salida) como una órbita bajo el grupo de simetría de la teoría.
   • El posterior de conceptos "consciente del atajo" se identifica como el único punto invariante de simetría: la distribución uniforme sobre la órbita.
   • Esto conduce al promedio de órbita (Orbit-Averaging), un método de forma cerrada para calcular este posterior:
     $$\bar{p}(c | x) = \frac{1}{|G|} \sum_{g \in G} p_\theta(g^{-1} \cdot c | x)$$
   • Este método simetriza un único modelo base sobre el grupo de salida preservadora $G$ sin requerir un ensamble o estimación de densidad.
4. Funciones generatrices: Para modelos intercambiables, el marco produce naturalmente funciones generatrices exponenciales (vía cardinalidad homotópica) en lugar de funciones generatrices ordinarias, alineándose con la teoría de especies combinatorias.

Resultados experimentales
Los autores evaluaron el método de promedio de órbita en pruebas de atajos de razonamiento de MNIST (específicamente tareas con grupos de simetría conocidos y verdad de base para la identificabilidad de conceptos).

• Configuración: Se entrenó una red neuronal única para predecir etiquetas fusionadas. La tarea consistía en distinguir entre dígitos identificables (tamaño de órbita 1) y dígitos confundibles (tamaño de órbita > 1).
• Comparación: El envoltorio de promedio de órbita de un solo modelo se comparó contra un modelo base y un ensamble de 5 modelos entrenados para la diversidad (Bears).
• Hallazgos:
  • El modelo base fue excesivamente confiado en los dígitos confundibles (alto Error de Calibración Esperada, ECE).
  • El promedio de órbita redujo el ECE en los dígitos confundibles de 0.614 a 0.010 mientras preservaba la precisión de la etiqueta y la calibración de los conceptos identificables.
  • El ensamble entrenado para la diversidad logró mejoras de calibración similares solo sacrificando la precisión de la etiqueta o descalibrando los conceptos identificables, resaltando un compromiso que el promedio de órbita de un solo modelo evita.

Significancia y afirmaciones
El artículo afirma que leer la inferencia NeSy a través de la lente de la HoTT proporciona un "beneficio concreto" al exponer la estructura de simetría responsable de los atajos de razonamiento.

• Unificación teórica: Unifica varios enfoques de NeSy (probabilísticos, difusos, de procedencia) bajo una única visión decategorificada de un objeto más rico y estructurado.
• Eficiencia práctica: Demuestra que el posterior "consciente del atajo", que anteriormente se pensaba que requería ensambles costosos, puede computarse en forma cerrada promediando un único modelo sobre el grupo de simetría.
• Calibración: El método mejora la calibración en conceptos no identificables sin degradar el rendimiento en los identificables, resolviendo un modo de fallo específico del aprendizaje NeSy.
• Limitaciones: Los autores señalan que el marco actual depende de tipos finitos ($\pi$-finitud). Extender la cardinalidad homotópica a dominios continuos mediante "cohesión" sigue siendo un problema abierto.

El trabajo se presenta como un cambio fundacional de un razonamiento basado en conjuntos a uno basado en tipos, donde el "olvido" de los conjuntos es reemplazado por la memoria estructural de los tipos, abordando directamente las causas raíz de los atajos de razonamiento.