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
|Proving expected sensitivity of probabilistic programs|
|Synthesizing Coupling Proofs of Differential Privacy|
|Measurable cones and stable, measurable functions|
|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 K. Moss University of Cambridge, Chris Heunen University of Edinburgh, Zoubin Ghahramani University of Cambridge