Verifying Sampling Algorithms via Distributional Invariants
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915826436669440 |
|---|---|
| author | Zilken, Daniel Batz, Kevin Katoen, Joost-Pieter Winkler, Tobias |
| author_facet | Zilken, Daniel Batz, Kevin Katoen, Joost-Pieter Winkler, Tobias |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_06410 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Verifying Sampling Algorithms via Distributional Invariants Zilken, Daniel Batz, Kevin Katoen, Joost-Pieter Winkler, Tobias Logic in Computer Science Discrete Mathematics 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. |
| title | Verifying Sampling Algorithms via Distributional Invariants |
| topic | Logic in Computer Science Discrete Mathematics |
| url | https://arxiv.org/abs/2509.06410 |