A pre-expectation calculus for probabilistic sensitivity
OPEN ACCESS
Loading...
Author / Producer
Date
2021-01
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
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.
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
5 (POPL)
Pages / Article No.
52
Publisher
Association for Computing Machinery
Event
48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
probabilistic programming; verification
Organisational unit
Notes
Funding
Related publications and datasets
Is new version of: http://hdl.handle.net/20.500.11850/525194