💻 computer science

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Dit artikel introduceert Continuous-Eris, een higher-order scheidingslogica geïmplementeerd in de Rocq-bewijshulp, om de correctheid van exacte steekproefalgoritmen voor continue verdelingen zoals Gaussisch en Laplace formeel te verifiëren, en zo de beveiligings- en nauwkeurigheidsbeperkingen van drijvende-kommabenaderingen aan te pakken.

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

Gepubliceerd 2026-05-14

📖 6 min leestijd🧠 Diepgaand

CC BY 4.0

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

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een taart probeert te bakken, maar in plaats van een standaard maatbeker te gebruiken, moet je elke ingrediënt meten door water uit een emmer in een klein kopje te gieten, één druppel per keer. Als je stopt na 100 druppels, heb je een benadering van de hoeveelheid. Als je stopt na 1.000, komt het dichter in de buurt. Maar als je op enig moment stopt, heb je technisch gezien een klein foutje gemaakt, omdat je niet het exacte bedrag hebt gekregen.

In de wereld van de informatica is dit precies wat er gebeurt wanneer computers reële getallen verwerken (zoals 3,14159...). Ze gebruiken "drijvende-kommagetallen", die lijken op die benaderingen van 100 druppels. Voor de meeste dingen is dit prima. Maar voor gevoelige taken—zoals het beschermen van privégegevens in medische studies of financiële dossiers—kunnen die kleine " afrondingsfouten" oplopen tot grote beveiligingslekken.

Dit artikel introduceert een nieuwe manier om dit probleem op te lossen. De auteurs hebben een tool gebouwd genaamd Continuous-Eris die programmeurs helpt om aan te tonen dat hun code exacte steekproeven trekt uit continue verdelingen (zoals het kiezen van een perfect willekeurig getal tussen 0 en 1) zonder ooit een afrondingsfout te maken.

Hier is hoe ze dit deden, met behulp van enkele creatieve analogieën:

1. Het Probleem: De "Luie" Kok

Meestal probeert een computer, om een willekeurig getal tussen 0 en 1 te krijgen, de hele oneindige reeks cijfers (0,101101...) in één keer te genereren. Maar dat is onmogelijk; je kunt geen oneindige lijst opschrijven.

In plaats daarvan gebruiken de auteurs een "luie" aanpak. Stel je een kok voor die alleen een ui laag voor laag schilt, maar alleen wanneer je erom vraagt.

De Code: Het programma U (Uniform) genereert niet direct het hele getal. Het maakt gewoon een lege lijst.
Het Verzoek: Wanneer je om de eerste paar cijfers vraagt (met een functie genaamd GetBits), schilt het programma één laag (genereert één willekeurig bit, 0 of 1).
De Magie: Als je later om meer cijfers vraagt, schilt het een andere laag. Het bouwt het getal bit voor bit op, alleen zo snel als je het nodig hebt. Dit zorgt ervoor dat je nooit met een oneindige lijst te maken hoeft te krijgen, maar je kunt wel een antwoord krijgen dat zo nauwkeurig is als je wilt.

2. De Uitdaging: Bewijzen dat de Kok Eerlijk is

Het moeilijke deel is niet het schrijven van de code; het is bewijzen dat de luie kok echt eerlijk getallen kiest.

Als de kok een laag schilt, is het dan echt willekeurig?
Als je om 10 lagen vraagt, is het resulterende getal dan echt verdeeld over het hele bereik?
Hoe bewijs je dit wanneer de kok nog niet eens klaar is met het schillen van de ui?

Eerdere hulpmiddelen konden dit alleen bewijzen voor eenvoudige, discrete dingen (zoals het rollen van een dobbelsteen). Ze konden niet omgaan met de "oneindige ui" van continue getallen, vooral niet wanneer de code complex was, geheugen gebruikte en waarden onderweg veranderde.

3. De Oplossing: De "Oneindige Tape" en "Tijdskvoten"

Om dit op te lossen, hebben de auteurs een nieuw logisch systeem (een reeks regels voor het bewijzen van codecorrectheid) bedacht dat drie slimme trucs combineert:

A. De "Voorgetekende Tape" (Vooraf steekproeven)

Stel je voor dat je een goochelaar bent. Om te bewijzen dat je truc werkt, schrijf je in het geheim de hele reeks kaarten die je zult trekken uit het deck, voordat je zelfs maar de show begint.
In hun logica gebruiken ze een "tape" die fungeert als deze vooraf geschreven lijst. Hoewel de computer bits één voor één genereert, gaat de bewijsvoering ervan uit dat de hele oneindige reeks bits al is opgeschreven op een magische tape. Dit stelt de wiskundige in staat om te redeneren over het "hele getal", zelfs al ziet het programma slechts "één bit per keer".

B. De "Tijdskvot" (Het Budget)

Hier komt het lastige deel: een tape kan in een computerbewijs eigenlijk niet oneindig zijn.
Daarom gebruiken ze een concept genaamd Tijdskvoten. Denk hierbij aan een "stappenbudget".

De logica zegt: "We gaan het programma slechts 100 stappen lang observeren."
Omdat het programma slechts één stap nodig heeft om één bit te genereren, hoeven we, als we slechts 100 stappen observeren, alleen de eerste 100 bits op onze magische tape te kennen.
De "Tijdskvot" is een token dat zegt: "Ik heb nog 100 stappen over." Elke keer dat het programma een stap zet, geef je een kwot uit.
Dit stelt hen in staat om te doen alsof de tape oneindig is, omdat ze voor elk specifiek moment in het bewijs slechts een eindig aantal bits nodig hebben, en ze een "kwot" hebben om die te betalen.

C. De "Foutkrediet" (Het Veiligheidsnet)

Tot slot gebruiken ze Foutkredieten. Stel je voor dat je een budget hebt aan "fouten" die je mag maken.

Als je wilt bewijzen dat het programma 99,9% correct is, besteed je 0,1% van je krediet.
De auteurs hebben een manier ontwikkeld om deze kredieten te "besteden" om te bewijzen dat de kans dat het programma zich onjuist gedraagt, verwaarloosbaar klein is.
Ze hebben uitgezocht hoe ze deze discrete "foutbudgetten" kunnen omzetten in een glad, continu wiskundig hulpmiddel (met behulp van integralen), zodat ze konden bewijzen dat de code werkt voor het hele bereik van reële getallen, niet alleen voor specifieke punten.

4. Wat Ze Eigenlijk Bewezen

Met behulp van dit nieuwe systeem hebben de auteurs niet alleen over theorie gesproken; ze hebben daadwerkelijke code gebouwd en geverifieerd voor:

Uniforme Verdeling: Het kiezen van een willekeurig getal tussen 0 en 1.
Gaussische (Belkromme): Het kiezen van een getal dat zich rond een gemiddelde concentreert (zoals menselijke lengtes).
Laplace-verdeling: Een specifiek type ruis dat wordt gebruikt in Differentiële Privacy (een methode om gegevens te delen zonder individuele geheimen te onthullen).

Ze bewezen dat hun code voor deze verdelingen wiskundig exact is. Als je hun code gebruikt, krijg je geen "voldoende nauwkeurig" drijvende-kommagetal; je krijgt een getal dat gegarandeerd de perfecte wiskundige regels volgt, bit voor bit.

De Conclusie

Het artikel presenteert een nieuw "reglement" (Continuous-Eris) dat programmeurs in staat stelt complexe, luie, exacte steekproefcode te schrijven en te bewijzen dat deze 100% correct is. Ze deden dit door een "magische vooraf geschreven tape" te combineren met een "stappenbudget"-systeem, waardoor ze konden redeneren over oneindige mogelijkheden met behulp van eindige, beheersbare stappen. Dit is een belangrijke stap vooruit om ervoor te zorgen dat privacy-bewarende algoritmen en andere kritieke systemen geen verborgen wiskundige bugs hebben die worden veroorzaakt door afrondingsfouten.

Technische Samenvatting: Verificatie van Exacte Steekproefnemers voor Continue Verdelingen met een Discrete Programmalogica

Probleemstelling

De meeste implementaties van steekproefalgoritmen voor continue kansverdelingen vertrouwen op drijvende-kommarekenen. Hoewel dit voor veel toepassingen aanvaardbaar is, introduceren bewerkingen met drijvende komma afrondingsfouten die moeilijk te analyseren zijn en kunnen leiden tot kritieke beveiligingskwetsbaarheden, met name in differentieel privacy waar algoritmen vaak formeel worden ontwikkeld onder de aanname van exacte rekenkunde.

Een alternatief is het gebruik van exacte steekproefalgoritmen gebaseerd op berekenbare reële getallen, die digitaal een continue steekproef willekeurig nauwkeurig kunnen genereren. Deze algoritmen zijn echter ingewikkeld. Ze vereisen een combinatie van semantisch uitdagende taalfeatures, waaronder probabilistische keuze, hogere-orde functies en dynamisch toegewezen mutabele staat. Bestaande programmalogica's voor probabilistische verificatie zijn ontoereikend voor deze taak: eerdere werken beperken redenering ofwel tot discrete verdelingen of gaan uit van het bestaan van primitieven voor het nemen van steekproeven uit continue verdelingen (vaak afhankelijk van niet-berekenbare reële rekenkunde). Bijgevolg ontbreekt het aan formele technieken om de correctheid van berekenbare, exacte steekproefnemers voor continue verdelingen te verifiëren die opereren binnen een discrete, statige programmodel.

Methodologie

De auteurs presenteren Continuous-Eris, een hogere-orde separatielogica ontworpen om de correctheid van exacte steekproefalgoritmen voor berekenbare verdelingen te verifiëren. Continuous-Eris breidt Eris uit (een logica voor het verifiëren van benaderende correctheid van discrete probabilistische programma's) en is gebouwd op het Iris-separatielogica-framework.

De kernmethodologie vertrouwt op het overbruggen van de kloof tussen discrete en continue redenering via drie belangrijke logische ingrediënten:

Foutkredieten: Geleend van Eris, zijn dit separatielogica-bronnen $E(r)$ die een bovengrens vertegenwoordigen op de waarschijnlijkheid dat een specificatie faalt. Ze maken modulaire redenering over probabilistische programma's mogelijk door kredieten te "besteden" om fouten met lage waarschijnlijkheid uit te sluiten.
Tijdsontvangsten: Aangepast van Mével et al., worden deze gebruikt om de partiële correctheid van de logica te internaliseren. Door het aantal resterende uitvoerstappen bij te houden ($StepsLeft(k)$), kan de logica redeneren over eindige prefixen van potentieel oneindige uitvoeringen. Dit is cruciaal omdat exacte steekproefnemers vaak lazy evaluatie omvatten waarbij een oneindige reeks bits nooit volledig wordt gegenereerd.
Pre-steekproefbanden: Aangepast van Clutch, stellen deze de bewijsvoering in staat om de uitkomsten van toekomstige willekeurige steekproefopdrachten vooraf te bepalen. Waar standaardbanden eindig zijn, combineren de auteurs ze met tijdsontvangsten om oneindige pre-steekproefbanden te simuleren. Dit mechanisme stelt de logica in staat foutkredieten te conditioneren op een specifiek reëel getal $r$ (vertegenwoordigd door een oneindige bitreeks), zelfs al genereert het programma tijdens enige eindige uitvoering slechts een eindig aantal bits.

Theoretische Grondslag

De logica generaliseert de discrete correctheidsspecificatie van Marionneau et al. naar de continue setting. In plaats van een steekproefnemer te karakteriseren door een discrete kansmassafunctie, karakteriseert Continuous-Eris een steekproefnemer door een Riemann-integraal over een kansdichtheidsfunctie.

Het centrale specificatiepatroon voor een steekproefnemer $U$ die een uniform reëel getal in $[0, 1]$ genereert, is:
$\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 \}$
Hierbij is $F$ een begrensd, stuksgewijs continu functie. De logica staat toe kredieten te conditioneren op de gestoken waarde $r$ alsof deze uniform wordt getrokken, op voorwaarde dat de verwachte waarde van de kredieten behouden blijft. De geldigheid van deze aanpak rust op het feit dat een Riemann-som (afgeleid van eindige pre-steekproeven) de integraal willekeurig nauwkeurig kan benaderen, waarbij de discretisatiefout wordt betaald met "thin-air" foutkredieten.

Belangrijkste Bijdragen

Continuous-Eris Logica: Een nieuwe programmalogica die foutkredieten, tijdsontvangsten en pre-steekproefbanden combineert om berekenbare continue steekproefalgoritmen te verifiëren. Het ondersteunt hogere-orde functies, mutabele staat en dynamische toewijzing.
Formele Verificatie van Exacte Steekproefnemers: De auteurs leveren formeel geverifieerde implementaties van exacte steekproefnemers voor:
- De Uniforme verdeling over $[0, 1]$ .
- De Gaussische (Normale) verdeling.
- De Laplace-verdeling.
  Deze implementaties zijn gebaseerd op algoritmen van Karney en maken gebruik van lazy bit-lijst representaties.
Geverifieerde Constructieve Reële Rekenkunde: Een bibliotheek voor exacte reële rekenkunde (een aanpassing van CReal) geverifieerd binnen Continuous-Eris. Deze bibliotheek ondersteunt bewerkingen (optellen, negatie, schalen, vergelijken) op lazy reële getallen, waardoor de constructie van complexe verdelingen uit eenvoudigere mogelijk wordt.
Nauwkeurigheidsgrens voor Differentieel Privacy: Een formeel bewijs dat de geverifieerde Laplace-steekproefnemer voldoet aan een specifieke nauwkeurigheidsgrens die wordt gebruikt in de literatuur over differentieel privacy. Dit toont aan dat de uitvoer van de steekproefnemer voldoet aan de theoretische garanties die vereist zijn voor privacy-bewarende mechanismen, zonder te vertrouwen op benaderingen met drijvende komma.
Mechanisatie: Alle resultaten zijn gemecaniseerd in de Rocq bewijshulp (voorheen Coq), gebaseerd op het Iris-framework en de Coquelicot bibliotheek voor reële analyse.

Resultaten

Het artikel demonstreert de bruikbaarheid van Continuous-Eris door de verificatie van het MaxU2-programma (het berekenen van het maximum van twee uniforme steekproeven) en de volledige Karney Gaussische steekproefnemer.

MaxU2: De auteurs bewijzen dat het programma een waarde retourneert die is verdeeld met kansdichtheid $\mu_{max}(x) = 2x$ . Het bewijs omvat geïtereerde integralen en Löb-inductie om recursieve bitvergelijkingen te behandelen.
Gaussische Steekproefnemer: De verificatie volgt een modulaire structuur, waarbij subroutines voor Bernoulli-proeven, gehele delen en afwijzingssteekproeflussen worden geverifieerd. Het bewijs stelt vast dat de steekproefnemer waarden genereert met de juiste Gaussische dichtheid.
Laplace-steekproefnemer: De auteurs verifiëren een steekproefnemer voor de Laplace-verdeling en leiden de staartgrens $P[|L_{\epsilon, \mu} - \mu| > \frac{\log(1/\beta)}{\epsilon}] \leq \beta$ direct af uit de logica, zonder deze als een primitieve axiom toe te voegen.

Betekenis en Claims

Het artikel claimt een kritieke kloof in formele verificatie te dichten door de eerste techniek te bieden die in staat is exacte, berekenbare steekproefnemers voor continue verdelingen te verifiëren die mutabele staat en hogere-orde functies gebruiken.

Correctheid zonder Benadering: In tegenstelling tot eerdere werken die continue primitieven aannemen of drijvende-kommarekenen gebruiken, verifieert Continuous-Eris algoritmen die exacte steekproeven genereren (tot willekeurige nauwkeurigheid) met uitsluitend discrete primitieven (Bernoulli-proeven).
Omgaan met Complexiteit: De logica beheert succesvol de semantische uitdagingen van het combineren van willekeur, mutabele staat en hogere-orde functies, wat doorgaans moeilijk is om denotationeel te redeneren.
Praktische Relevantie: Door de Laplace-steekproefnemer en zijn nauwkeurigheidsgrenzen te verifiëren, biedt het werk een fundament voor het bouwen van systemen met differentieel privacy met rigoureuze garanties tegen fouten met drijvende komma.
Bescheidenheid: De auteurs erkennen beperkingen. De huidige aanpak vertrouwt op Riemann-integratie, wat vereist dat kredietverdelingsfuncties stuksgewijs continu zijn. Dit verhindert redenering over verdelingen met onaftelbare discontinuïteiten (bijvoorbeeld het vermijden van alle rationale punten). Bovendien richt het artikel zich op partiële correctheid; het bewijzen van bijna-zekere terminatie voor deze steekproefnemers wordt overgelaten aan toekomstig werk of andere logica's zoals Total Eris.

Kortom, Continuous-Eris biedt een rigoureus, gemecaniseerd raamwerk om te verifiëren dat complexe, statige programma's correct exacte steekproefneming uit continue verdelingen implementeren, en overbrugt de kloof tussen theoretische berekenbare analyse en praktische programmacorrectheid.