Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verifying Sampling Algorithms via Distributional Invariants

Daniel Zilken, Kevin Batz, Joost-Pieter Katoen, Tobias Winkler

TL;DR

This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that is applied to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saad et al.'s Fast Loaded Dice Roller, enabling both total and partial correctness of the two algorithms.

Abstract

This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saad et al.'s Fast Loaded Dice Roller. These algorithms have previously resisted formal veri cation due to their probabilistic nature, intricate loop structure, and parametric input. Our approach complements existing proof rules based on inductive distributional invariants, enabling us to verify both total and partial correctness of the two algorithms.

Verifying Sampling Algorithms via Distributional Invariants

TL;DR

This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that is applied to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saad et al.'s Fast Loaded Dice Roller, enabling both total and partial correctness of the two algorithms.

Abstract

This paper presents a Hoare-like veri cation framework for discrete probabilistic programs that we apply to two non-trivial sampling algorithms: Lumbroso's Fast Dice Roller and Saad et al.'s Fast Loaded Dice Roller. These algorithms have previously resisted formal veri cation due to their probabilistic nature, intricate loop structure, and parametric input. Our approach complements existing proof rules based on inductive distributional invariants, enabling us to verify both total and partial correctness of the two algorithms.

Paper Structure

This paper contains 52 sections, 19 theorems, 103 equations, 20 figures.

Table of Contents

  1. Introduction
  2. Sampler Verification with Distributional Invariants: Von Neumann's Fair Coin.
  3. Efficient Discrete Uniform Sampling: A "Fast Dice Roller" DBLP:journals/corr/abs-1304-1916.
  4. Contributions.
  5. Preliminaries
  6. Probabilistic Programs.
  7. Distributions.
  8. Strongest Postconditions and Reachable Distributions
  9. Denotational Distribution Transformer Semantics.
  10. Distributional Strongest Postconditions.
  11. Reachable Distributions.
  12. Distributional Invariants
  13. Distributional Invariants for Probabilistic Loops.
  14. From Probabilistic Loops to Markov Chains.
  15. Invariant Verification Framework
  16. ...and 37 more sections

Key Result

corollary 1

For every loop $C = \textnormal{while}\,\textnormal{(}\varphi\textnormal{)}\,\textnormal{\{}B\textnormal{\}}$ and $M \subseteq {\Delta_{\leq 1} \Sigma}$ it holds that

Figures (20)

  • Figure 1: Left: Probabilistic program modeling Von Neumann's algorithm vonNeumann1951, where $\textnormal{\{}\, L\,\textnormal{\}} \, \textnormal{[}p\textnormal{]} \, \textnormal{\{}\, R\,\textnormal{\}}$ executes sub-programs $L$ and $R$ with probability $p$ and $1-p$, respectively. Right: The program's underlying Markov chain (\ref{['def:mdpOfLoop']}, def:mdpOfLoop). The terminal states (doubly circled) have a self-loop, which is important for our theory to work.
  • Figure 2: Left: The Fast Dice Roller (FDR) algorithm adapted from DBLP:journals/corr/abs-1304-1916 for discrete uniform sampling. Right: Lumbroso's distributional invariant DBLP:journals/corr/abs-1304-1916 and two members of the FDR's infinite family of underlying Markov chains (\ref{['def:mdpOfLoop']}, def:mdpOfLoop).
  • Figure 3: Denotational semantics. $\mathsf{D}\llbracket C\rrbracket(\mu)$ is the output distribution of $C$ on input $\mu$.
  • Figure 4: Program $C_{\text{geo}}$ generating a geometric distribution.
  • Figure 5: Left: Probabilistic loop with initial distribution. Right: Reachable fragment of the loop's big-step operational Markov chain. Terminal states have a double boundary.
  • ...and 15 more figures

Theorems & Definitions (47)

  • definition 1: Syntax
  • definition 2: Denotational Semantics
  • definition 3: Distributional $\mathsf{sp}$
  • definition 4: Reachable Distributions
  • corollary 1
  • theorem 1: From $\reachn$ to $\denn$
  • proof
  • definition 5: Markov Chain
  • definition 6: Distributional Markov Chain Invariant DBLP:conf/cav/AkshayCMZ23
  • definition 7: Distributional Loop Invariant
  • ...and 37 more