Proving expected sensitivity of probabilistic programs
Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program’s input lead to bounded changes in the output. We propose an average notion of program sensitivity for probabilistic programs—expected sensitivity—that averages a distance function over a probabilistic coupling of the two output distributions from two nearby inputs. By varying the distance functions, expected sensitivity captures useful notions of probabilistic function sensitivity, including algorithmic stability of machine learning algorithms and convergence of Markov chains.
Furthermore, expected sensitivity satisfies clean compositional properties and is amenable to formal verification. We develop a relational program logic called ExSeL for proving expected sensitivity properties, featuring two key components. First, relational pre-conditions and post-conditions are expressed using distances, which can be seen as a real-valued generalization of typical boolean-valued (relational) assertions. Second, judgments —with distances as pre-conditions and post-conditions— are interpreted in terms of expectation coupling, a novel, quantitative generalization of probabilistic couplings which supports compositional reasoning.
We demonstrate our logic on two classes of examples: uniform stability of the Stochastic Gradient Method algorithm from machine learning, and rapid mixing for a model of asexual population dynamics. We also extend our logic with a transitivity principle for expectation couplings to capture the path coupling, and we demonstrate our extension by proving rapid mixing of the Glauber dynamics from statistical physics.
Fri 12 JanDisplayed time zone: Tijuana, Baja California change
13:40 - 15:20
ProbabilityResearch Papers at Watercourt
Chair(s): Lars Birkedal Aarhus University
|Proving expected sensitivity of probabilistic programs|
Gilles Barthe IMDEA Software Institute, Thomas Espitau Universite Pierre et Marie Curie, Benjamin Gregoire INRIA, Justin Hsu University College London, Pierre-Yves Strub Ecole Polytechnique
|Synthesizing Coupling Proofs of Differential Privacy|
Aws Albarghouthi University of Wisconsin-Madison, Justin Hsu University College London
|Measurable cones and stable, measurable functions|
Thomas Ehrhard CNRS and University Paris Diderot, Michele Pagani University Paris Diderot, Christine Tasson University Paris Diderot
|Denotational validation of higher-order Bayesian inference|
Adam Ścibior University of Cambridge and MPI Tuebingen, Ohad Kammar University of Oxford, Matthijs Vákár University of Oxford, Sam Staton University of Oxford, Hongseok Yang University of Oxford, Yufei Cai University of Tuebingen, Klaus Ostermann University of Tuebingen, Sean Moss University of Oxford, Chris Heunen University of Edinburgh, Zoubin Ghahramani University of Cambridge