A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

Resumen Técnico: Una formalización cúbica de la independencia condicional, el condicionamiento bayesiano y la solidez de la d-separación de Pearl

Planteamiento del problema
El artículo aborda una brecha fundacional en la verificación formal del razonamiento probabilístico: el axioma de intercambio de álgebra convexa estándar, común en las formalizaciones de monadas de probabilidad desde Stone, es demostrablemente demasiado débil para soportar el condicionamiento bayesiano completo. Mientras que las formalizaciones clásicas (por ejemplo, en Coq) tratan la independencia condicional (CI) como una igualdad proposicional entre probabilidades de valores reales, estas dependen de la lógica clásica y la extensionalidad, requiriendo a menudo hipótesis de positividad y división por probabilidades no nulas para derivar resultados estructurales como el axioma de intersección. Además, elevar el condicionamiento bayesiano recursivo a una representación de tipos inductivos superiores (HIT) de distribuciones revela un desajuste estructural: el axioma de intercambio estándar asume un único peso interno compartido para las mezclas reordenadas, mientras que el condicionamiento bayesano produce naturalmente mezclas con pesos internos distintos relacionados mediante la fórmula de Bayes.

Metodología
El autor desarrolla una formalización constructiva en Cubical Agda, utilizando Teoría de Tipos Cúbicos y Tipos Inductivos Superiores (HITs). La metodología se basa en tres cambios estructurales respecto a los enfoques clásicos:

1. Monada de Probabilidad como un HIT: Las distribuciones finitas (FDist) se definen como un HIT generado por masas puntuales y una operación de mezcla ponderada binaria. Las leyes estándar del álgebra convexa (idempotencia, conmutatividad sesgada, casos límite, intercambio y sesguiamiento asociativo) se imponen como constructores de caminos (path constructors). Esto permite que las igualdades distribucionales sean tratadas como transformaciones ejecutables (caminos) en lugar de igualdades proposicionales opacas.
2. Independencia Condicional Estructural: La CI se define como un camino entre núcleos de distribución (kXY z ≡ kX z ⊗D kY z) en lugar de una igualdad punto a punto de números reales. Esto permite el razonismo composicional donde los testigos de CI pueden ser transportados a través de operaciones monádicas.
3. Manejo Constructivo de Pesos: El desarrollo es polimórfico sobre una firma de Peso abstracta (un cuerpo ordenado con orden decidible), instanciada concretamente en los racionales ($\mathbb{Q}$). Esto evita la indecidibilidad de la igualdad en los reales constructivos y permite el manejo explícito de la positividad y la división.

Contribuciones Clave y Resultados

• El Desajuste del Intercambio y su Generalización: El hallazgo técnico central es que el axioma de intercambio estándar (ley medial) es insuficiente para el condicionamiento bayesiano completo. El condicionamiento de una mezcla de 4 hojas crea dos mitades internas con pesos distintos ($q_1$ y $q_2$) relacionados por la fórmula de Bayes, mientras que el axioma estándar requiere que estos pesos coincidan ($q_1 = q_2$). El autor introduce un axioma de intercambio generalizado (mix-bayes-interchange) que permite pesos internos distintos. Se demuestra que la forma estándar es el caso degenerado donde estos pesos coinciden.
• Axioma de Intersección Constructivo: El artículo proporciona una prueba constructiva del axioma de intersección (que clásicamente requiere positividad) reduciéndolo a la contracción. En lugar de la extracción bayesiana mediante división, la prueba utiliza testigos estructurales de tipo $\Sigma$ de factorización e hipótesis de habitabilidad para las variables de condicionamiento. Esto recupera el contenido completo de la intersección para cualquier modelo de distribución positiva concreta sin postulados.
• Verificación del Cálculo Do de Pearl: Las tres reglas del cálculo do de Pearl se verifican al nivel del núcleo en modelos causales estructurales (SCM) pequeños:
  • Reglas 1 y 3: Verificadas como corolarios de las leyes de la monada y el lema constBind (la intervención en variables independientes deja las marginales sin cambios).
  • Regla 2: Verificada en SCM confundidos usando un testigo de CI estructural de que el prior conjunto se factoriza. Esto establece la equivalencia entre intervención y condicionamiento bajo independencia.
• Condicionamiento Bayesiano Recursivo: Se define una función total para el condicionamiento bayesiano recursivo en un fragmento de soporte completo del HIT. El autor resuelve las seis obligaciones de coherencia requeridas para elevar esta función al HIT completo. La quinta coherencia (intercambio) requiere el axioma generalizado mencionado anteriormente.
• Alineación con Categorías de Markov: La monada FDist se verifica como una instancia concreta de una categoría de Markov (en el sentido de Fritz y Cho–Jacobs). El axioma no trivial de delete-naturality (preservación de la masa total) se demuestra mediante inducción de HIT, confirmando que los constructores de caminos capturan correctamente la normalización estocástica.
• Solidez de la d-Separación: La solidez del teorema de d-separación de Pearl se verifica constructivamente para grafos acíclicos dirigidos (DAG) finitos arbitrarios. Esto cubre tanto las formas intervencionales (para conjuntos multi-elemento $X, Y, Z$) como las formas bayesianas (para patrones elementales), derivadas mediante factorización ancestral sin reducción por cada camino.

Significado y Reivindicaciones
El artículo afirma proporcionar la primera formalización verificada por máquina, constructiva, de la dirección de solidez del teorema de d-separación de Pearl con este nivel de generalidad, enteramente dentro de un marco de teoría de tipos.

• Contenido Computacional: A diferencia de las formalizaciones clásicas donde la CI es una aserción, el enfoque cúbico produce contenido computacional. Los testigos de CI son transformaciones ejecutables; las distribuciones posteriores son términos ejecutables computados por el normalizador de Agda.
• Corrección Fundacional: Este trabajo identifica que la base algebraica estándar para las monadas de probabilidad es "demasiado débil" para el condicionamiento bayesiano. La generalización propuesta del axioma de intercambio se presenta como un refinamiento estructural necesario para cualquier marco que pretenda soportar la inferencia bayesiana completa dentro de un entorno monádico.
• Verificación del Stack de Mahadevan: El artículo verifica la "capa inferior" del marco del Modelo Causal de Topos (TCM) de Mahadevan. Confirma que las identidades de nivel de núcleo del cálculo do y la monada de distribución conmutativa se mantienen constructivamente, sirviendo como un sustrato verificado sobre el cual se puede construir la maquinaria topos-teórica (haces, semántica de forcing).
• Cero Postulados: Todo el desarrollo, incluyendo la solidez de la d-separación y el condicionamiento bayesiano, se verifica con cero postulados por encima de la interfaz de campo ordenado abstracto (instanciada en $\mathbb{Q}$). Esto incluye la eliminación de límites anteriormente usados que eran inconsistentes y el reemplazo de la división clásica por operaciones constructivas protegidas por positividad.

El artículo concluye que el contenido constructivo de la independencia condicional y el condicionamiento se captura mejor no mediante la lógica clásica y la extensionalidad, sino mediante el razonamiento estructural basado en caminos de la teoría de tipos cúbicos, donde las leyes algebraicas de la probabilidad son intrínsecas a la definición del tipo.