Smith, William Robert; (2025) Sampling languages: Semantics and verification of sampling-based inference algorithms for probabilistic programming. Doctoral thesis (Ph.D), UCL (University College London).

Preview	Text main.pdf - Accepted Version Download (1MB) | Preview
Preview	Text (Supplemental material) Smith_10215443_Declaration Form_sigs_removed.pdf Download (259kB) | Preview

Abstract

Practical probabilistic programs, especially those with approximate conditioning, by necessity combine a number of sampling techniques in sequence in order to produce samples - as well as certain complex language features in order to implement those techniques. Sufficiently complex probabilistic programs therefore require a compositional approach to verification, beginning with the fundamentals of language design, syntax, and semantics, and building to the higher-level questions about samplers and their statistical properties. In this thesis, we design a typed probabilistic programming language which is equipped with the features necessary to serve as a setting for the verification of sampling techniques. These features include: continuous random variables; higher-order functions; dependent types; compatibility with deterministic, that is to say pseudorandom, generation of samples; and samplers for (the marginal distributions of) stochastic processes. We give a semantics for the language in terms of concrete concepts, and show equivalence of the denotational and operational semantics. We present a set of rules for the effective verification of sampler equivalence in a suitable subset of the language. Stating, in this setting, the desired targeting relationship between samplers and the probability measures that they are to produce samples from, we then lay out a calculus centred on this targeting relationship, which enables the compositional verification of sampling techniques such as importance sampling and rejection sampling. These verification procedures are then extended so as to enable the verification of samplers which produce samples targeting (the marginal distributions of) stochastic processes. We conclude by arguing that a sampling language with these features is a natural compilation target for a probabilistic programming language with approximate Bayesian conditioning, flexible enough to frame many Bayesian inference methods in common use without incorporating features that hinder effective verification.

Download activity - last month

Export as JSONCSVXML

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as CSVXMLJSON

Archive Staff Only

View Item