Show simple item record

dc.contributor.authorŚcibior, Adamen
dc.contributor.authorKammar, Ohaden
dc.contributor.authorVákár, Matthijsen
dc.contributor.authorStaton, Samen
dc.contributor.authorYang, Hongseoken
dc.contributor.authorCai, Yufeien
dc.contributor.authorOstermann, Klausen
dc.contributor.authorMoss, Seanen
dc.contributor.authorHeunen, Chrisen
dc.contributor.authorGhahramani, Zoubinen
dc.date.accessioned2018-02-01T17:49:25Z
dc.date.available2018-02-01T17:49:25Z
dc.date.issued2018-01en
dc.identifier.issn2475-1421
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/271507
dc.description.abstractWe present a modular semantic account of Bayesian inference algorithms for probabilistic programming lan- guages, 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 implemen- tation reflects this modularity. We show how to conceptualise and analyse such inference algorithms as ma- nipulating 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 col- lection 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 con- nection between the semantic manipulation and its traditional measure theoretic origins, we use Kock’s syn- thetic measure theory. We demonstrate its usefulness by proving a quasi-Borel counterpart to the Metropolis- Hastings-Green theorem.
dc.languageenen
dc.titleDenotational validation of higher-order Bayesian inferenceen
dc.typeArticle
prism.endingPage29
prism.issueIdentifierPOPLen
prism.publicationDate2018en
prism.publicationNameProceedings of the ACM on Programming Languagesen
prism.startingPage1
prism.volume2en
dc.identifier.doi10.17863/CAM.18497
dcterms.dateAccepted2017-09-26en
rioxxterms.versionofrecord10.1145/3158148en
rioxxterms.versionAM*
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2018-01en
dc.contributor.orcidGhahramani, Zoubin [0000-0002-7464-6475]
dc.identifier.eissn2475-1421
rioxxterms.typeJournal Article/Reviewen
pubs.funder-project-idEPSRC (1471629)
pubs.funder-project-idEPSRC (1361027)
pubs.funder-project-idAlan Turing Institute (EP/N510129/1)
rioxxterms.freetoread.startdate2018-11-10


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record