💻 computer science

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Cet article présente Continuous-Eris, une logique de séparation d'ordre supérieur implémentée dans l'assistant de preuve Rocq, pour vérifier formellement l'exactitude des algorithmes d'échantillonnage exact pour des distributions continues telles que les distributions gaussienne et de Laplace, en palliant les limitations de sécurité et de précision des approximations en virgule flottante.

Auteurs originaux : Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti

Publié 2026-05-14

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayiez de faire un gâteau, mais au lieu d'utiliser une tasse à mesurer standard, vous devez mesurer chaque ingrédient en versant de l'eau d'un seau dans une toute petite tasse, une goutte à la fois. Si vous vous arrêtez après 100 gouttes, vous avez une approximation de la quantité. Si vous vous arrêtez après 1 000, c'est plus proche. Mais si vous vous arrêtez à n'importe quel moment, vous avez techniquement commis une petite erreur car vous n'avez pas obtenu la quantité exacte.

Dans le monde de l'informatique, c'est exactement ce qui se produit lorsque les ordinateurs gèrent des nombres réels (comme 3,14159...). Ils utilisent des « nombres à virgule flottante », qui sont comme ces approximations de 100 gouttes. Pour la plupart des choses, cela suffit. Mais pour des tâches sensibles — comme la protection des données privées dans les études médicales ou les registres financiers — ces petites « erreurs d'arrondi » peuvent s'additionner pour créer de grandes failles de sécurité.

Ce papier présente une nouvelle façon de résoudre ce problème. Les auteurs ont créé un outil appelé Continuous-Eris qui aide les programmeurs à prouver que leur code effectue un échantillonnage exact à partir de distributions continues (comme choisir un nombre parfaitement aléatoire entre 0 et 1) sans jamais commettre d'erreur d'arrondi.

Voici comment ils ont procédé, en utilisant quelques analogies créatives :

1. Le Problème : Le Chef « Paresseux »

Habituellement, pour obtenir un nombre aléatoire entre 0 et 1, un ordinateur pourrait essayer de générer toute la séquence infinie de chiffres (0,101101...) d'un coup. Mais c'est impossible ; on ne peut pas écrire une liste infinie.

Au lieu de cela, les auteurs utilisent une approche « paresseuse ». Imaginez un chef qui épluche un oignon couche par couche, mais seulement lorsque vous le lui demandez.

Le Code : Le programme U (Uniforme) ne génère pas tout le nombre immédiatement. Il crée simplement une liste vide.
La Demande : Lorsque vous demandez les premiers chiffres (en utilisant une fonction appelée GetBits), le programme épluche une couche (génère un bit aléatoire, 0 ou 1).
La Magie : Si vous demandez plus de chiffres plus tard, il épluche une autre couche. Il construit le nombre bit par bit, aussi vite que vous en avez besoin. Cela garantit que vous n'avez jamais à gérer une liste infinie, mais vous pouvez obtenir une réponse aussi précise que vous le souhaitez.

2. Le Défi : Prouver que le Chef est Honnête

La partie difficile n'est pas d'écrire le code ; c'est de prouver que le chef paresseux choisit réellement les nombres de manière équitable.

Si le chef épluche une couche, est-ce vraiment aléatoire ?
Si vous demandez 10 couches, le nombre résultant est-il vraiment réparti sur toute la plage ?
Comment le prouver lorsque le chef n'a même pas encore fini d'éplucher l'oignon ?

Les outils précédents ne pouvaient prouver cela que pour des choses simples et discrètes (comme lancer un dé). Ils ne pouvaient pas gérer l'« oignon infini » des nombres continus, surtout lorsque le code était complexe, utilisait de la mémoire et modifiait des valeurs à la volée.

3. La Solution : Le « Ruban Infini » et les « Reçus de Temps »

Pour résoudre ce problème, les auteurs ont inventé un nouveau système logique (un ensemble de règles pour prouver la correction du code) qui combine trois astuces ingénieuses :

A. Le « Ruban Pré-dessiné » (Pré-échantillonnage)

Imaginez que vous êtes un magicien. Pour prouver que votre tour fonctionne, vous écrivez secrètement toute la séquence de cartes que vous allez tirer du paquet avant même de commencer le spectacle.
Dans leur logique, ils utilisent un « ruban » qui agit comme cette liste pré-écrite. Même si l'ordinateur génère les bits un par un, la preuve suppose que toute la séquence infinie de bits est déjà écrite sur un ruban magique. Cela permet au mathématicien de raisonner sur le « nombre entier » même si le programme ne voit que « un bit à la fois ».

B. Le « Reçu de Temps » (Le Budget)

Voici la partie délicate : un ruban ne peut pas réellement être infini dans une preuve informatique.
Ainsi, ils utilisent un concept appelé Reçus de Temps. Considérez cela comme un « budget d'étapes ».

La logique dit : « Nous allons seulement observer l'exécution du programme pendant 100 étapes ».
Parce que le programme ne prend qu'une étape pour générer un bit, si nous n'observons que 100 étapes, nous n'avons besoin de connaître que les 100 premiers bits sur notre ruban magique.
Le « Reçu de Temps » est un jeton qui dit : « Il me reste 100 étapes ». Chaque fois que le programme effectue une étape, vous dépensez un reçu.
Cela leur permet de faire semblant que le ruban est infini, car pour n'importe quel moment spécifique dans la preuve, ils n'ont besoin que d'un nombre fini de bits, et ils ont un « reçu » pour les payer.

C. Le « Crédit d'Erreur » (Le Filet de Sécurité)

Enfin, ils utilisent des Crédits d'Erreur. Imaginez que vous avez un budget de « erreurs » que vous êtes autorisé à commettre.

Si vous voulez prouver que le programme est correct à 99,9 %, vous dépensez 0,1 % de votre crédit.
Les auteurs ont mis au point un moyen de « dépenser » ces crédits pour prouver que la probabilité que le programme se comporte incorrectement est négligeable.
Ils ont trouvé comment transformer ces « budgets d'erreurs » discrets en un outil mathématique continu et lisse (en utilisant des intégrales) afin de prouver que le code fonctionne pour toute la gamme des nombres réels, et pas seulement pour des points spécifiques.

4. Ce qu'ils ont réellement prouvé

En utilisant ce nouveau système, les auteurs n'ont pas seulement parlé de théorie ; ils ont construit et vérifié du code réel pour :

Distribution Uniforme : Choisir un nombre aléatoire entre 0 et 1.
Gaussienne (Courbe en Cloche) : Choisir un nombre qui se regroupe autour d'une moyenne (comme les tailles humaines).
Distribution de Laplace : Un type spécifique de bruit utilisé dans la Confidentialité Différentielle (une méthode pour partager des données sans révéler les secrets individuels).

Ils ont prouvé que leur code pour ces distributions est mathématiquement exact. Si vous utilisez leur code, vous n'obtenez pas un nombre à virgule flottante « assez proche » ; vous obtenez un nombre garanti pour suivre les règles mathématiques parfaites, bit par bit.

L'Essentiel

Le papier présente un nouveau « code de règles » (Continuous-Eris) qui permet aux programmeurs d'écrire du code complexe, paresseux et d'échantillonnage exact, et de prouver qu'il est correct à 100 %. Ils ont fait cela en combinant un « ruban pré-écrit magique » avec un système de « budget d'étapes », leur permettant de raisonner sur des possibilités infinies en utilisant des étapes finies et gérables. C'est une avancée majeure pour garantir que les algorithmes de préservation de la vie privée et d'autres systèmes critiques ne comportent pas de bugs mathématiques cachés causés par des erreurs d'arrondi.

Résumé technique : Vérification des échantillonneurs exacts pour les distributions continues avec une logique de programme discrète

Énoncé du problème

La plupart des implémentations d'algorithmes d'échantillonnage pour les distributions de probabilité continues reposent sur l'arithmétique à virgule flottante. Bien que cela soit acceptable pour de nombreuses applications, les opérations à virgule flottante introduisent des erreurs d'arrondi difficiles à analyser et pouvant conduire à des vulnérabilités de sécurité critiques, en particulier dans le cadre de la confidentialité différentielle où les algorithmes sont souvent développés formellement en supposant une arithmétique exacte.

Une alternative consiste à utiliser des algorithmes d'échantillonnage exacts basés sur les réels calculables, capables de générer paresseusement les chiffres d'un échantillon continu avec une précision arbitraire. Cependant, ces algorithmes sont complexes. Ils nécessitent une combinaison de fonctionnalités linguistiques sémantiquement difficiles, notamment le choix probabiliste, les fonctions d'ordre supérieur et l'état mutable alloué dynamiquement. Les logiques de programme existantes pour la vérification probabiliste sont insuffisantes pour cette tâche : les travaux antérieurs restreignent soit le raisonnement aux distributions discrètes, soit supposent l'existence de primitives pour l'échantillonnage à partir de distributions continues (reposant souvent sur une arithmétique réelle non calculable). Par conséquent, il manque de techniques formelles pour vérifier la correction des échantillonneurs exacts calculables pour les distributions continues opérant au sein d'un modèle de programmation discret et mutable.

Méthodologie

Les auteurs présentent Continuous-Eris, une logique de séparation d'ordre supérieur conçue pour vérifier la correction des algorithmes d'échantillonnage exacts pour les distributions calculables. Continuous-Eris étend Eris (une logique pour vérifier la correction approximative des programmes probabilistes discrets) et est construite sur le cadre de logique de séparation Iris.

La méthodologie centrale repose sur le comblement du fossé entre le raisonnement discret et continu grâce à trois ingrédients logiques clés :

Crédits d'erreur : Empruntés à Eris, ce sont des ressources de logique de séparation $E(r)$ représentant une borne supérieure sur la probabilité d'échec d'une spécification. Ils permettent un raisonnement modulaire sur les programmes probabilistes en « dépensant » des crédits pour exclure des événements d'erreur de faible probabilité.
Reçus de temps : Adaptés de Mével et al., ils servent à internaliser la correction partielle de la logique. En suivant le nombre d'étapes d'exécution restantes ($StepsLeft(k)$), la logique peut raisonner sur des préfixes finis d'exécutions potentiellement infinies. Ceci est crucial car les échantillonneurs exacts impliquent souvent une évaluation paresseuse où une séquence infinie de bits n'est jamais entièrement générée.
Rubans de pré-échantillonnage : Adaptés de Clutch, ils permettent à la preuve de déterminer à l'avance les résultats des futures commandes d'échantillonnage aléatoire. Alors que les rubans standards sont finis, les auteurs les combinent avec des reçus de temps pour simuler des rubans de pré-échantillonnage infinis. Ce mécanisme permet à la logique de conditionner les crédits d'erreur à un nombre réel spécifique $r$ (représenté par une chaîne de bits infinie), même si le programme ne génère qu'un nombre fini de bits lors de toute exécution finie.

Fondement théorique

La logique généralise la spécification de correction discrète de Marionneau et al. au cadre continu. Au lieu de caractériser un échantillonneur par une fonction de masse de probabilité discrète, Continuous-Eris le caractérise par une intégrale de Riemann sur une fonction de densité de probabilité.

Le motif de spécification central pour un échantillonneur $U$ générant un réel uniforme dans $[0, 1]$ est :
$\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 \}$
Ici, $F$ est une fonction bornée et continue par morceaux. La logique permet de conditionner les crédits à la valeur échantillonnée $r$ comme si elle était tirée uniformément, à condition que la valeur attendue des crédits soit préservée. La validité de cette approche repose sur le fait qu'une somme de Riemann (dérivée d'un pré-échantillonnage fini) peut approximer l'intégrale arbitrairement près, l'erreur de discrétisation étant payée par des crédits d'erreur « tirés de nulle part ».

Contributions clés

Logique Continuous-Eris : Une logique de programme novatrice combinant crédits d'erreur, reçus de temps et rubans de pré-échantillonnage pour vérifier les algorithmes d'échantillonnage continu calculables. Elle prend en charge les fonctions d'ordre supérieur, l'état mutable et l'allocation dynamique.
Vérification formelle d'échantillonneurs exacts : Les auteurs fournissent des implémentations formellement vérifiées d'échantillonneurs exacts pour :
- La distribution Uniforme sur $[0, 1]$ .
- La distribution Gaussienne (Normale).
- La distribution Laplace.
  Ces implémentations sont basées sur des algorithmes de Karney et utilisent des représentations paresseuses de listes de bits.
Arithmétique réelle constructive vérifiée : Une bibliothèque pour l'arithmétique réelle exacte (une adaptation de CReal) vérifiée dans Continuous-Eris. Cette bibliothèque prend en charge les opérations (addition, négation, mise à l'échelle, comparaison) sur les nombres réels paresseux, permettant la construction de distributions complexes à partir de distributions plus simples.
Borne de précision pour la confidentialité différentielle : Une preuve formelle que l'échantillonneur Laplace vérifié satisfait une borne de précision spécifique utilisée dans la littérature sur la confidentialité différentielle. Cela démontre que la sortie de l'échantillonneur adhère aux garanties théoriques requises pour les mécanismes de préservation de la confidentialité, sans recourir à des approximations à virgule flottante.
Mécanisation : Tous les résultats sont mécanisés dans l'assistant de preuve Rocq (anciennement Coq), s'appuyant sur le cadre Iris et la bibliothèque d'analyse réelle Coquelicot.

Résultats

L'article démontre l'utilité de Continuous-Eris à travers la vérification du programme MaxU2 (calculant le maximum de deux échantillons uniformes) et de l'échantillonneur Gaussien de Karney complet.

MaxU2 : Les auteurs prouvent que le programme retourne une valeur distribuée avec une densité de probabilité $\mu_{max}(x) = 2x$ . La preuve implique des intégrales itérées et l'induction de Löb pour gérer les comparaisons récursives de bits.
Échantillonneur Gaussien : La vérification suit une structure modulaire, vérifiant des sous-routines pour les essais de Bernoulli, les parties entières et les boucles d'échantillonnage par rejet. La preuve établit que l'échantillonneur génère des valeurs avec la densité gaussienne correcte.
Échantillonneur Laplace : Les auteurs vérifient un échantillonneur pour la distribution Laplace et dérivent la borne de queue $P[|L_{\epsilon, \mu} - \mu| > \frac{\log(1/\beta)}{\epsilon}] \leq \beta$ directement de la logique, sans l'ajouter comme un axiome primitif.

Importance et affirmations

L'article prétend combler une lacune critique dans la vérification formelle en fournissant la première technique capable de vérifier des échantillonneurs exacts et calculables pour les distributions continues qui utilisent un état mutable et des fonctions d'ordre supérieur.

Correction sans approximation : Contrairement aux travaux antérieurs qui supposent des primitives continues ou utilisent l'arithmétique à virgule flottante, Continuous-Eris vérifie des algorithmes générant des échantillons exacts (avec une précision arbitraire) en utilisant uniquement des primitives discrètes (essais de Bernoulli).
Gestion de la complexité : La logique gère avec succès les défis sémantiques de la combinaison du hasard, de l'état mutable et des fonctions d'ordre supérieur, qui sont généralement difficiles à raisonner de manière dénotationnelle.
Pertinence pratique : En vérifiant l'échantillonneur Laplace et ses bornes de précision, ce travail fournit une base pour construire des systèmes à confidentialité différentielle avec des garanties rigoureuses contre les erreurs à virgule flottante.
Modestie : Les auteurs reconnaissent les limites. L'approche actuelle repose sur l'intégration de Riemann, exigeant que les fonctions de distribution de crédits soient continues par morceaux. Cela empêche le raisonnement sur des distributions avec des discontinuités non dénombrables (par exemple, éviter tous les points rationnels). De plus, l'article se concentre sur la correction partielle ; prouver la terminaison presque sûre pour ces échantillonneurs est laissé à de futurs travaux ou à d'autres logiques comme Total Eris.

En résumé, Continuous-Eris offre un cadre rigoureux et mécanisé pour vérifier que des programmes complexes et mutables implémentent correctement l'échantillonnage exact à partir de distributions continues, comblant le fossé entre l'analyse calculable théorique et la vérification pratique des programmes.