Verifying Sampling Algorithms via Distributional Invariants
summary
Framework treats probabilistic programs as distribution transformers and proves that the Fast Dice Roller and Fast Loaded Dice Roller produce the intended discrete distributions, e.g. variable c is uniform on 0..n-1 despite using a single coin flip per loop. Correctness uses inductive distributional loop invariants (over-approximations of reachable distributions) shown equivalent to Markov-chain invariants, a closure that adds limit distributions, and a required almost-sure termination proof; invariants are found manually.
AI-written summary · about
related talks
15mTuning Random Generators: Property-Based Testing as Probabilistic Programming
56mUsing, Generating and Testing with Pseudo-Random Numbers
40mTesting Distributed Systems w/ Deterministic Simulation
23mRandomized Testing of Distributed Systems with Probabilistic Guarantees
38mPurely Random
27mUnderstanding Distributed Systems with Deterministic Simulation
08mUnlucky Simulation
34mSymbolic Execution for Randomized Programs