UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

A Pre-expectation Calculus for Probabilistic Sensitivity

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) 10.1145/3434333. (In press).

[img] Text
main.pdf - Accepted version
Access restricted to UCL open access staff until 25 May 2021.

Download (942kB)

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
DOI: 10.1145/3434333
Publisher version: https://dl.acm.org/journal/pacmpl
Language: English
Keywords: probabilistic programming, verification
UCL classification: UCL
UCL > Provost and Vice Provost Offices
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
Downloads since deposit
0Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item