Fri 12 Jan 2018 14:55 - 15:20 at Watercourt - Probability Chair(s): Lars Birkedal

We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in Bayesian data science and machine learning. Sophisticated inference algorithms are often explained in terms of composition of smaller parts. However, neither their theoretical justification nor their implementation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as manipulating intermediate representations of probabilistic programs using higher-order functions and inductive types, and their denotational semantics.

Semantic accounts of continuous distributions use measurable spaces. However, our use of higher-order functions presents a substantial technical difficulty: it is impossible to define a measurable space structure over the collection of measurable functions between arbitrary measurable spaces that is compatible with standard operations on those functions, such as function application. We overcome this difficulty using quasi-Borel spaces, a recently proposed mathematical structure that supports both function spaces and continuous distributions.

We define a class of semantic structures for representing probabilistic programs, and semantic validity criteria for transformations of these representations in terms of distribution preservation. We develop a collection of building blocks for composing representations. We use these building blocks to validate common inference algorithms such as Sequential Monte Carlo and Markov Chain Monte Carlo. To emphasize the connection between the semantic manipulation and its traditional measure theoretic origins, we use Kock’s synthetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis-Hastings-Green theorem. Finally, although not discussed in the paper, we provide an implementation of the concepts described in this paper as a Haskell library.

Fri 12 Jan

Displayed time zone: Tijuana, Baja California change

13:40 - 15:20
ProbabilityResearch Papers at Watercourt
Chair(s): Lars Birkedal Aarhus University
13:40
25m
Talk
Proving expected sensitivity of probabilistic programs
Research Papers
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
14:05
25m
Talk
Synthesizing Coupling Proofs of Differential Privacy
Research Papers
Aws Albarghouthi University of Wisconsin-Madison, Justin Hsu University College London
14:30
25m
Talk
Measurable cones and stable, measurable functions
Research Papers
Thomas Ehrhard CNRS and University Paris Diderot, Michele Pagani University Paris Diderot, Christine Tasson University Paris Diderot
14:55
25m
Talk
Denotational validation of higher-order Bayesian inference
Research Papers
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