Denotational validation of higher-order Bayesian inference
| Autor: | Matthijs Vákár, Hongseok Yang, Sean K. Moss, Adam Ścibior, Chris Heunen, Yufei Cai, Sam Staton, Ohad Kammar, Klaus Ostermann, Zoubin Ghahramani |
|---|---|
| Přispěvatelé: | Ghahramani, Zoubin [0000-0002-7464-6475], Apollo - University of Cambridge Repository |
| Rok vydání: | 2018 |
| Předmět: |
FOS: Computer and information sciences
Theoretical computer science Measurable function Computer science Function space Bayesian inference Inference 02 engineering and technology commutative monads 01 natural sciences Measure (mathematics) symbols.namesake Denotational semantics applied category theory sigma-monoids 0202 electrical engineering electronic engineering information engineering quasi-Borel spaces synthetic measure theory 0101 mathematics Safety Risk Reliability and Quality Computer Science - Programming Languages 010102 general mathematics Probabilistic logic 020207 software engineering Markov chain Monte Carlo Kock integration symbols initial algebra semantics Particle filter Software Programming Languages (cs.PL) |
| Zdroj: | Scibior, A, Kammar, O, Vákár, M, Staton, S, Yang, H, Cai, Y, Ostermann, K, Moss, S K, Heunen, C & Ghahramani, Z 2018, ' Denotational validation of higher-order Bayesian inference ', Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, 60 . https://doi.org/10.1145/3158148 |
| DOI: | 10.17863/cam.18497 |
| Popis: | 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 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|