Aguirre, A;
Barthe, G;
Hsu, J;
Kaminski, BL;
Katoen, J-P;
Matheja, C;
(2021)
A Pre-expectation Calculus for Probabilistic Sensitivity.
Proceedings of the ACM on Programming Languages
, 5
(POPL)
, Article 52. 10.1145/3434333.
Preview |
Text
Kaminski_3434333.pdf - Published Version Download (386kB) | Preview |
Abstract
Sensitivity properties describe how changes to the input of a program affect the output, typically by upper bounding the distance between the outputs of two runs by a monotone function of the distance between the corresponding inputs. When programs are probabilistic, the distance between outputs is a distance between distributions. The Kantorovich lifting provides a general way of defining a distance between distributions by lifting the distance of the underlying sample space; by choosing an appropriate distance on the base space, one can recover other usual probabilistic distances, such as the Total Variation distance. We develop a relational pre-expectation calculus to upper bound the Kantorovich distance between two executions of a probabilistic program. We illustrate our methods by proving algorithmic stability of a machine learning algorithm, convergence of a reinforcement learning algorithm, and fast mixing for card shuffling algorithms. We also consider some extensions: using our calculus to show convergence of Markov chains to the uniform distribution over states and an asynchronous extension to reason about pairs of program executions with different control flow.
| Type: | Article |
|---|---|
| Title: | A Pre-expectation Calculus for Probabilistic Sensitivity |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3434333 |
| Publisher version: | https://doi.org/10.1145/3434333 |
| Language: | English |
| Additional information: | © 2021 Copyright held by the owner/author(s). This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited. |
| Keywords: | probabilistic programming, verification |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10115803 |
Loading...
Loading...Loading...Loading...Archive Staff Only
 |
View Item |
