1: \begin{abstract}

2:   \emph{Program sensitivity}, also known as \emph{Lipschitz continuity},

3:   describes how small changes in a program's input lead to bounded changes in

4:   the output. We propose an average notion of program sensitivity for

5:   probabilistic programs---\emph{expected sensitivity}---that averages a

6:   distance function over a probabilistic coupling of two output

7:   distributions from two similar inputs. By varying the distance,

8:   expected sensitivity recovers useful notions of probabilistic function

9:   sensitivity, including stability of machine learning algorithms

10:   and convergence of Markov chains.

11: 

12:   Furthermore, expected sensitivity satisfies clean compositional

13:   properties and is amenable to formal verification. We develop a

14:   relational program logic called \SYSTEM for proving expected

15:   sensitivity properties. Our logic features two key ideas. First,

16:   relational pre-conditions and post-conditions are expressed using

17:   \emph{distances}, a real-valued generalization

18:   of typical boolean-valued (relational) assertions. Second, judgments

19:   are interpreted in terms of \emph{expectation coupling}, a novel,

20:   quantitative generalization of probabilistic couplings which

21:   supports compositional reasoning.

22: 

23:   We demonstrate our logic on examples beyond the reach of prior relational

24:   logics. Our main example formalizes uniform stability of the stochastic

25:   gradient method.

26:   Furthermore, we prove rapid mixing for a probabilistic model of population

27:   dynamics. We also extend our logic with a transitivity principle for

28:   expectation couplings to capture the \emph{path coupling} proof

29:   technique by \citet{bubley1997path}, and formalize

30:   rapid mixing of the Glauber dynamics from

31:   statistical physics.

32: \end{abstract}

33: