Proving Expected Sensitivity of Probabilistic Programs

Explore a 23-minute conference presentation from POPL 2018 that introduces expected sensitivity, a novel average notion of program sensitivity for probabilistic programs. Delve into how this mathematical concept averages distance functions over probabilistic couplings of output distributions from similar inputs. Learn about EpRHL, a relational program logic developed for proving expected sensitivity properties, which uses distances for relational conditions and expectation coupling for compositional reasoning. Discover practical applications through examples including the uniform stability of stochastic gradient method and rapid mixing in population dynamics models. Understand how the logic extends to incorporate the path coupling technique by Bubley and Dyer, demonstrated through an analysis of Glauber dynamics in statistical physics. Presented by researchers from IMDEA Software Institute, UPMC, Inria, University College London, and École Polytechnique, this talk offers valuable insights into formal verification of probabilistic program properties.