noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning

Resumen Técnico: noDice

1. El Problema

Los lenguajes de programación probabilística (PPL) son herramientas expresivas para modelar distribuciones de probabilidad complejas. Sin embargo, los motores de inferencia modernos suelen carecer de soporte para dos características críticas que a menudo aparecen juntas en la práctica:

1. No determinismo: Elecciones que no siguen una distribución de probabilidad fija (común en Procesos de Decisión de Markov - MDPs, aprendizaje por refuerzo y abstracciones de sistemas).
2. Condicionamiento (Observaciones): La capacidad de actualizar creencias basándose en evidencia observada (razonamiento bayesiano).

La combinación de no determinismo y condicionamiento es matemáticamente desafiante porque:

• Los programas ya no modelan una sola distribución, sino un conjunto de distribuciones.
• La inferencia deja de ser composicional: la probabilidad condicional máxima de un programa no puede derivarse simplemente de las probabilidades máximas de sus subprogramas.
• Los enfoques existentes a menudo fallan al manejar ambos simultáneamente o requieren la construcción directa de semánticas operativas que generan espacios de estado exponencialmente grandes, haciendo la inferencia inviable.

2. Metodología: El Marco noDice

Los autores presentan noDice, un motor de inferencia para programas probabilísticos discretos que extiende el trabajo previo del motor Dice. La metodología se basa en transformar el problema de inferencia en un problema de alcanzabilidad condicional en Procesos de Decisión de Markov (MDP), utilizando Diagramas de Decisión como estructura intermedia para comprimir el espacio de estados.

El proceso de inferencia consta de tres etapas principales:

1. Compilación Booleana (Boolean Compilation):

   • El programa noDice (sin bucles, con variables acotadas) se compila utilizando el motor de Dice.
   • Se generan dos fórmulas booleanas:
     • $\phi$: Modela el comportamiento del programa ignorando las observaciones.
     • $\gamma$: Modela exclusivamente las condiciones de las observaciones (éxito de las observaciones).
   • Se mantiene una traza anotada de las operaciones de "flip" (lanzamiento de moneda), distinguiendo entre flips probabilísticos ($flip(\theta)$) y no determinísticos ($nflip()$).

2. Construcción de Diagramas de Decisión Algebraicos (ADDs):

   • Las fórmulas booleanas se representan internamente como Diagramas de Decisión Binarios (BDDs).
   • A diferencia de Dice, noDice combina estas dos estructuras en un único Diagrama de Decisión Algebraico (ADD). Los ADDs generalizan los BDDs permitiendo salidas que no son solo booleanas, lo que permite unificar la lógica del programa y las observaciones en una sola estructura gráfica compacta.
   • Esta etapa explota la estructura del programa (independencia condicional) para eliminar redundancias y reducir drásticamente el tamaño de la representación.

3. Levantamiento a MDPs (Lifting to MDPs):

   • El ADD se "levanta" a un MDP. Cada nodo del ADD se convierte en un estado del MDP.
   • Las transiciones del MDP dependen del tipo de variable en el nodo:
     • Si es un flip probabilístico, las transiciones tienen probabilidades fijas.
     • Si es un flip no determinístico, el estado tiene múltiples acciones disponibles (no determinismo).
   • La semántica del programa original corresponde a los planificadores (schedulers) sin memoria en este MDP.
   • La inferencia se reduce a calcular la probabilidad máxima de alcanzabilidad condicional de un estado objetivo (donde el programa devuelve un valor específico) dado que se alcanza un estado de "aceptación" (donde todas las observaciones tuvieron éxito).

3. Contribuciones Clave

• Lenguaje noDice: Definición de un lenguaje funcional de primer orden, no recursivo, que soporta elecciones probabilísticas, no determinísticas y observaciones de primera clase.
• Algoritmo de Inferencia Teórico: Presentación de una base teórica sólida que demuestra cómo compilar programas con no determinismo y condicionamiento en MDPs compactos mediante ADDs. Se prueba que la probabilidad máxima de alcanzar un valor en el MDP corresponde a la máxima probabilidad condicional en la semántica del programa.
• Implementación y Evaluación: Desarrollo de un prototipo en OCaml que integra la compilación de Dice, la construcción de ADDs y el uso del verificador de modelos Storm (con un algoritmo de bisecación) para la resolución de MDPs.
• Optimizaciones:
  • Compresión de Estados Probabilísticos: Eliminación de estados intermedios con una sola acción habilitada para reducir el tamaño del MDP.
  • Reducción a Programas Booleanos: Transformación de consultas sobre valores complejos a consultas booleanas para simplificar la inferencia.

4. Resultados Empíricos

Los autores evaluaron noDice en una amplia gama de benchmarks (Redes de Runway, Colección de Cupones, Redes de Comunicación, Protocolos de Intercambio Justo y Redes Bayesianas) comparándolo con Dice (solo probabilístico) y Storm (verificador de modelos directo).

• Reducción del Espacio de Estados: noDice logra construir MDPs significativamente más pequeños que la codificación directa utilizada por Storm. En muchos casos, el tamaño del MDP de noDice es órdenes de magnitud menor gracias a la compresión mediante ADDs.
• Eficiencia de Inferencia:
  • En problemas con alta dimensionalidad (muchas variables, como en los benchmarks de Cupones o Redes Bayesianas grandes), noDice supera a Storm, que sufre por la explosión combinatoria al enumerar estados.
  • En problemas con baja dimensionalidad (pocas variables, como en el benchmark de Red), Storm puede ser más rápido porque la compilación de noDice tiene un costo fijo alto.
• Impacto del No Determinismo: El tiempo de compilación (construcción del ADD) es independiente de la cantidad de no determinismo. El tiempo de verificación (model checking) aumenta ligeramente con el no determinismo, pero sigue siendo una fracción pequeña del tiempo total.
• Rendimiento General: noDice es capaz de realizar inferencia en programas grandes donde los enfoques directos fallan o tardan demasiado, demostrando ser superior en escenarios complejos con múltiples variables y condicionamiento.

5. Significado e Impacto

Este trabajo es un avance significativo en el campo de la verificación formal y la programación probabilística:

• Cierra una brecha importante: Proporciona una solución práctica para la inferencia en programas que combinan no determinismo y condicionamiento, un área que anteriormente carecía de herramientas escalables.
• Eficiencia Escalable: Demuestra que el uso de diagramas de decisión (ADDs) como intermediario es una estrategia viable para evitar la explosión del espacio de estados en MDPs derivados de programas.
• Fundamento para Futuras Investigaciones: Establece una base para extender la inferencia exacta a programas más complejos (por ejemplo, con bucles o números no acotados) y para la síntesis de estrategias óptimas en sistemas probabilísticos.

En resumen, noDice ofrece un enfoque novedoso que traduce la complejidad de la inferencia probabilística con no determinismo en problemas de alcanzabilidad en MDPs comprimidos, logrando un rendimiento superior en escenarios de alta dimensionalidad donde las herramientas existentes fallan.