Projects per year
Abstract
We present a modular semantic account of Bayesian inference algorithms for probabilistic programming languages, as used in 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 higherorder functions and inductive types, and their denotational semantics.
Semantic accounts of continuous distributions use measurable spaces. However, our use of higherorder 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 quasiBorel 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 quasiBorel counterpart to the MetropolisHastingsGreen theorem.
Semantic accounts of continuous distributions use measurable spaces. However, our use of higherorder 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 quasiBorel 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 quasiBorel counterpart to the MetropolisHastingsGreen theorem.
Original language  English 

Article number  60 
Number of pages  31 
Journal  Proceedings of the ACM on Programming Languages 
Volume  2 
Issue number  POPL 
Early online date  27 Dec 2017 
DOIs  
Publication status  Published  1 Jan 2018 
Event  45th ACM SIGPLAN Symposium on Principles of Programming Languages  Los Angeles, United States Duration: 10 Jan 2018 → 12 Jan 2018 https://popl18.sigplan.org/ 
Fingerprint Dive into the research topics of 'Denotational validation of higherorder Bayesian inference'. Together they form a unique fingerprint.
Projects
 1 Finished
Profiles

Ohad Kammar
 School of Informatics  Senior Research Fellow
 Laboratory for Foundations of Computer Science
 Foundations of Computation
Person: Academic: Research Active