2026-09-19T05:17:09Zhttps://api.repository.cam.ac.uk/server/oai/request

oai:www.repository.cam.ac.uk:1810/2951672025-12-19T22:43:11Zcom_1810_213729com_1810_256065col_1810_219485

Formally justified and modular Bayesian inference for probabilistic programs 10.17863/CAM.42233 Ścibior, Adam Michał Ghahramani, Zoubin Probabilistic modelling offers a simple and coherent framework to describe the real world in the face of uncertainty. Furthermore, by applying Bayes' rule it is possible to use probabilistic models to make inferences about the state of the world from partial observations. While traditionally probabilistic models were constructed on paper, more recently the approach of probabilistic programming enables users to write the models in executable languages resembling computer programs and to freely mix them with deterministic code. It has long been recognised that the semantics of programming languages is complicated and the intuitive understanding that programmers have is often inaccurate, resulting in difficult to understand bugs and unexpected program behaviours. Programming languages are therefore studied in a rigorous way using formal languages with mathematically defined semantics. Traditionally formal semantics of probabilistic programs are defined using exact inference results, but in practice exact Bayesian inference is not tractable and approximate methods are used instead, posing a question of how the results of these algorithms relate to the exact results. Correctness of such approximate methods is usually argued somewhat less rigorously, without reference to a formal semantics. In this dissertation we formally develop denotational semantics for probabilistic programs that correspond to popular sampling algorithms often used in practice. The semantics is defined for an expressive typed lambda calculus with higher-order functions and inductive types, extended with probabilistic effects for sampling and conditioning, allowing continuous distributions and unbounded likelihoods. It makes crucial use of the recently developed formalism of quasi-Borel spaces to bring all these elements together. We provide semantics corresponding to several variants of Markov chain Monte Carlo and Sequential Monte Carlo methods and formally prove a notion of correctness for these algorithms in the context of probabilistic programming. We also show that the semantic construction can be directly mapped to an implementation using established functional programming abstractions called monad transformers. We develop a compact Haskell library for probabilistic programming closely corresponding to the semantic construction, giving users a high level of assurance in the correctness of the implementation. We also demonstrate on a collection of benchmarks that the library offers performance competitive with existing systems of similar scope. An important property of our construction, both the semantics and the implementation, is the high degree of modularity it offers. All the inference algorithms are constructed by combining small building blocks in a setup where the type system ensures correctness of compositions. We show that with basic building blocks corresponding to vanilla Metropolis-Hastings and Sequential Monte Carlo we can implement more advanced algorithms known in the literature, such as Resample-Move Sequential Monte Carlo, Particle Marginal Metropolis-Hastings, and Sequential Monte Carlo squared. These implementations are very concise, reducing the effort required to produce them and the scope for bugs. On top of that, our modular construction enables in some cases deterministic testing of randomised inference algorithms, further increasing reliability of the implementation. University of Cambridge 2019-10-26 Thesis Doctoral Doctor of Philosophy (PhD) en Engineering and Physical Sciences Research Council, Cambridge Trust, Cambridge-Tuebingen programme https://www.repository.cam.ac.uk/handle/1810/295167 https://www.repository.cam.ac.uk/bitstreams/d2851189-e73e-4439-85ff-a648eded82b8/download 1e2a7e161e72449acfb30327fb63c884 https://www.repository.cam.ac.uk/bitstreams/ca8a7aae-1031-49f8-a94c-9e361d3bc7fc/download 87eda9de84448d1f82354d60eee3eb5f https://www.rioxx.net/licenses/all-rights-reserved/ probabilistic programming machine learning Bayesian inference functional programming denotational semantics Haskell Monte Carlo Markov chain Monte Carlo Sequential Monte Carlo quasi-Borel spaces monads monad transformers programming languages lambda calculus importance sampling