Dahlqvist, F; Silva, A; Smith, W; (2023) Deterministic stream-sampling for probabilistic programming: semantics and verification. In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE: Boston, MA, USA.

Preview

Text main.pdf - Accepted Version Download (506kB) | Preview

Abstract

Probabilistic programming languages rely fundamentally on some notion of sampling, and this is doubly true for probabilistic programming languages which perform Bayesian inference using Monte Carlo techniques. Verifying samplers - proving that they generate samples from the correct distribution - is crucial to the use of probabilistic programming languages for statistical modelling and inference. However, the typical denotational semantics of probabilistic programs is incompatible with deterministic notions of sampling. This is problematic, considering that most statistical inference is performed using pseudorandom number generators.We present a higher-order probabilistic programming language centred on the notion of samplers and sampler operations. We give this language an operational and denotational semantics in terms of continuous maps between topological spaces. Our language also supports discontinuous operations, such as comparisons between reals, by using the type system to track discontinuities. This feature might be of independent interest, for example in the context of differentiable programming.Using this language, we develop tools for the formal verification of sampler correctness. We present an equational calculus to reason about equivalence of samplers, and a sound calculus to prove semantic correctness of samplers, i.e. that a sampler correctly targets a given measure by construction.

Download activity - last month

Export as XMLCSVJSON

Download activity - last 12 months

Export as JSONCSVXML

Downloads by country - last 12 months

Export as JSONXMLCSV

Archive Staff Only

View Item