Resumen Técnico: Verificación de Muestreadores Exactos para Distribuciones Continuas con una Lógica de Programas Discreta

Enunciado del Problema

La mayoría de las implementaciones de algoritmos de muestreo para distribuciones de probabilidad continuas dependen de la aritmética de punto flotante. Aunque aceptable para muchas aplicaciones, las operaciones de punto flotante introducen errores de redondeo que son difíciles de analizar y pueden provocar vulnerabilidades críticas de seguridad, particularmente en la privacidad diferencial, donde los algoritmos a menudo se desarrollan formalmente bajo la suposición de aritmética exacta.

Una alternativa es utilizar algoritmos de muestreo exacto basados en reales computables, que pueden generar perezosamente dígitos de una muestra continua con precisión arbitraria. Sin embargo, estos algoritmos son intrincados. Requieren una combinación de características de lenguaje semánticamente desafiantes, incluyendo elección probabilística, funciones de orden superior y estado mutable dinámicamente asignado. Las lógicas de programas existentes para la verificación probabilística son insuficientes para esta tarea: trabajos anteriores restringen el razonamiento a distribuciones discretas o asumen la existencia de primitivas para el muestreo de distribuciones continuas (a menudo dependiendo de aritmética real no computable). En consecuencia, existe una falta de técnicas formales para verificar la corrección de muestreadores exactos y computables para distribuciones continuas que operan dentro de un modelo de programación discreto y con estado.

Metodología

Los autores presentan Continuous-Eris, una lógica de separación de orden superior diseñada para verificar la corrección de algoritmos de muestreo exacto para distribuciones computables. Continuous-Eris extiende Eris (una lógica para verificar la corrección aproximada de programas probabilísticos discretos) y se construye sobre el marco de lógica de separación Iris.

La metodología central se basa en cerrar la brecha entre el razonamiento discreto y continuo a través de tres ingredientes lógicos clave:

1. Créditos de Error: Tomados prestados de Eris, estos son recursos de lógica de separación $E(r)$ que representan una cota superior sobre la probabilidad de que falle una especificación. Permiten un razonamiento modular sobre programas probabilísticos al "gastar" créditos para excluir eventos de error de baja probabilidad.
2. Recibos de Tiempo: Adaptados de Mével et al., se utilizan para internalizar la corrección parcial de la lógica. Al rastrear el número de pasos de ejecución restantes ($StepsLeft(k)$), la lógica puede razonar sobre prefijos finitos de ejecuciones potencialmente infinitas. Esto es crucial porque los muestreadores exactos a menudo implican evaluación perezosa donde una secuencia infinita de bits nunca se genera completamente.
3. Cintas de Pre-muestreo: Adaptadas de Clutch, permiten que la prueba determine de antemano los resultados de futuros comandos de muestreo aleatorio. Mientras que las cintas estándar son finitas, los autores las combinan con recibos de tiempo para simular cintas de pre-muestreo infinitas. Este mecanismo permite que la lógica condicione los créditos de error sobre un número real específico $r$ (representado por una cadena infinita de bits) incluso si el programa solo genera un número finito de bits durante cualquier ejecución finita.

Fundamento Teórico

La lógica generaliza la especificación de corrección discreta de Marionneau et al. al contexto continuo. En lugar de caracterizar un muestreador mediante una función de masa de probabilidad discreta, Continuous-Eris caracteriza un muestreador mediante una integral de Riemann sobre una función de densidad de probabilidad.

El patrón de especificación central para un muestreador $U$ que genera un real uniforme en $[0, 1]$ es:
$$\forall F \in PC([0, 1]), \quad \left\{ E\left(\int_0^1 F(x) dx\right) \right\} U() \{ v. \exists r. E(F(r)) * IsReal\ v\ r \}$$
Aquí, $F$ es una función acotada y continua a trozos. La lógica permite condicionar créditos sobre el valor muestreado $r$ como si fuera extraído uniformemente, siempre que se preserve el valor esperado de los créditos. La solidez de este enfoque se basa en el hecho de que una suma de Riemann (derivada del pre-muestreo finito) puede aproximar la integral arbitrariamente de cerca, con el error de discretización pagado mediante créditos de error "de la nada".

Contribuciones Clave

1. Lógica Continuous-Eris: Una lógica de programas novedosa que combina créditos de error, recibos de tiempo y cintas de pre-muestreo para verificar algoritmos de muestreo continuo computables. Soporta funciones de orden superior, estado mutable y asignación dinámica.
2. Verificación Formal de Muestreadores Exactos: Los autores proporcionan implementaciones formalmente verificadas de muestreadores exactos para:
   • La distribución Uniforme sobre $[0, 1]$.
   • La distribución Gaussiana (Normal).
   • La distribución Laplace.
     Estas implementaciones se basan en algoritmos de Karney y utilizan representaciones de listas de bits perezosas.
3. Aritmética Constructiva de Reales Verificada: Una biblioteca para aritmética real exacta (una adaptación de CReal) verificada dentro de Continuous-Eris. Esta biblioteca soporta operaciones (suma, negación, escalado, comparación) sobre números reales perezosos, permitiendo la construcción de distribuciones complejas a partir de otras más simples.
4. Límite de Precisión para Privacidad Diferencial: Una prueba formal de que el muestreador Laplace verificado satisface un límite de precisión específico utilizado en la literatura de privacidad diferencial. Esto demuestra que la salida del muestreador se adhiere a las garantías teóricas requeridas para mecanismos de preservación de la privacidad sin depender de aproximaciones de punto flotante.
5. Mecanización: Todos los resultados están mecanizados en el asistente de pruebas Rocq (anteriormente Coq), construyendo sobre el marco Iris y la biblioteca de análisis real Coquelicot.

Resultados

El artículo demuestra la utilidad de Continuous-Eris a través de la verificación del programa MaxU2 (que calcula el máximo de dos muestras uniformes) y el muestreador Gaussiano de Karney completo.

• MaxU2: Los autores prueban que el programa devuelve un valor distribuido con densidad de probabilidad $\mu_{max}(x) = 2x$. La prueba implica integrales iteradas e inducción de Löb para manejar comparaciones recursivas de bits.
• Muestreador Gaussiano: La verificación sigue una estructura modular, verificando subrutinas para ensayos de Bernoulli, partes enteras y bucles de muestreo por rechazo. La prueba establece que el muestreador genera valores con la densidad gaussiana correcta.
• Muestreador Laplace: Los autores verifican un muestreador para la distribución Laplace y derivan el límite de cola $P[|L_{\epsilon, \mu} - \mu| > \frac{\log(1/\beta)}{\epsilon}] \leq \beta$ directamente de la lógica, sin añadirlo como un axioma primitivo.

Significado y Afirmaciones

El artículo afirma llenar una brecha crítica en la verificación formal al proporcionar la primera técnica capaz de verificar muestreadores exactos y computables para distribuciones continuas que utilizan estado mutable y funciones de orden superior.

• Corrección sin Aproximación: A diferencia de trabajos anteriores que asumen primitivas continuas o utilizan aritmética de punto flotante, Continuous-Eris verifica algoritmos que generan muestras exactas (con precisión arbitraria) utilizando únicamente primitivas discretas (ensayos de Bernoulli).
• Manejo de la Complejidad: La lógica gestiona con éxito los desafíos semánticos de combinar aleatoriedad, estado mutable y funciones de orden superior, que suelen ser difíciles de razonar denotacionalmente.
• Relevancia Práctica: Al verificar el muestreador Laplace y sus límites de precisión, el trabajo proporciona una base para construir sistemas de privacidad diferencial con garantías rigurosas contra errores de punto flotante.
• Modestia: Los autores reconocen limitaciones. El enfoque actual depende de la integración de Riemann, lo que requiere que las funciones de distribución de créditos sean continuas a trozos. Esto impide razonar sobre distribuciones con discontinuidades no numerables (por ejemplo, evitando todos los puntos racionales). Además, el artículo se centra en la corrección parcial; probar la terminación casi segura para estos muestreadores queda para trabajos futuros u otras lógicas como Total Eris.

En resumen, Continuous-Eris ofrece un marco riguroso y mecanizado para verificar que programas complejos con estado implementan correctamente el muestreo exacto de distribuciones continuas, cerrando la brecha entre el análisis computable teórico y la verificación práctica de programas.