Probabilistic Programming Languages (PPLs) allow users to encode statistical inference problems and automatically apply an inference algorithm to solve them. Popular inference algorithms for PPLs, such as sequential Monte Carlo (SMC) and Markov chain Monte Carlo (MCMC), are built around checkpoints—relevant events for the inference algorithm during the execution of a probabilistic program. Deciding the location of checkpoints is, in current PPLs, not done optimally. To solve this problem, we present a static analysis technique that automatically determines checkpoints in programs, relieving PPL users of this task. The analysis identifies a set of checkpoints that execute in the same order in every program run—they are aligned. We formalize alignment, prove the correctness of the analysis, and implement the analysis as part of the higher-order functional PPL Miking CorePPL. By utilizing the alignment analysis, we design two novel inference algorithm variants: aligned SMC and aligned lightweight MCMC. We show, through real-world experiments, that they significantly improve inference execution time and accuracy compared to standard PPL versions of SMC and MCMC.

Probabilistic programming languages (PPLs) allow users to express statistical inference problems that the PPL implementation then, ideally, solves automatically. In particular, PPL users can focus on encoding their inference problems, and need not concern themselves with the intricacies of inference. Universal PPLs are PPLs with great expressive power, meaning that users can express essentially any inference problem. Consequently, universal PPL implementations often use general-purpose inference algorithms that are compatible with all such inference problems. A problem, however, is that general-purpose inference algorithms can often not efficiently solve complex inference problems. Furthermore, for certain inference algorithms, there are no formal correctness proofs in the context of universal PPLs.

This dissertation considers research problems related to Monte Carlo inference algorithms—sampling-based general-purpose inference algorithms that universal PPL implementations often apply. The first research problem concerns the correctness of sequential Monte Carlo (SMC) inference algorithms. A contribution in the dissertation is a proof of correctness for SMC algorithms in the context of universal PPLs. The second research problem concerns execution time improvements when suspending executions—a requirement in many Monte Carlo inference algorithms. The dissertation addresses the problem through two separate approaches. The first approach is a compilation technique targeting high-performance platforms. The second approach is a static suspension analysis guiding a selective continuation-passing style (CPS) transformation, reducing overhead compared to a full CPS transformation. The third research problem concerns inference improvements through alignment—a useful and often overlooked property in PPLs. The dissertation contributions are a formal definition of alignment, a static analysis technique that automatically aligns programs, and aligned versions of SMC and Markov chain Monte Carlo (MCMC) inference algorithms. The final research problem is more practical, and concerns the effective implementation of PPLs. Specifically, the contribution is the Miking CorePPL universal PPL and its compiler. Overall, the contributions in the dissertation significantly improve the efficiency of Monte Carlo algorithms as applied in universal PPLs.

Probabilistiska programmeringsspråk (PPL:er) tillåter användare att uttrycka statistiska inferensproblem som PPL-implementationen sedan, i bästa fall, löser automatiskt. I synnerhet kan PPL-användare fokusera på att uttrycka sina inferensproblem utan att behöva bekymra sig om svårigheter tillhörande inferensen. Universella PPL:er är PPL:er med stor uttrycksfullhet, vilket innebär att användare kan uttrycka i princip vilket inferensproblem som helst. Följaktligen använder universella PPL-implementationer ofta inferensalgoritmer för allmänna ändamål som är kompatibla med alla sådana inferensproblem. Ett problem är dock att inferensalgoritmer för allmänna ändamål ofta inte effektivt kan lösa komplexa inferensproblem. Dessutom finns det inga formella korrekthetsbevis för vissa inferensalgoritmer när de används i universella PPL:er.

I denna avhandling behandlas forskningsproblem som rör Monte Carlo-inferensalgoritmer—samplingbaserade inferensalgoritmer för allmänna ändamål som universella PPL-implementationer ofta tillämpar. Det första forskningsproblemet rör korrektheten av sekventiella Monte Carlo-inferensalgoritmer (SMC). Ett bidrag i avhandlingen är ett korrekthetsbevis för SMC-algoritmer i universella PPL:er. Det andra forskningsproblemet rör förbättringar av exekveringstid vid exekveringsavbrott—ett krav i många Monte Carlo-inferensalgoritmer. Avhandlingen behandlar problemet genom två separata tillvägagångssätt. Det första tillvägagångssättet är en kompileringsteknik som riktar sig mot högpresterande plattformar. Det andra tillvägagångssättet är en statisk avbrottsanalys som styr en selektiv transformation till fortsättningsskickande stil (CPS), vilket reducerar exekveringstid jämfört med en fullständig CPS-transformation. Det tredje forskningsproblemet rör inferensförbättringar genom samordning—en användbar och ofta förbisedd egenskap i PPL:er. Avhandlingens bidrag är en formell definition av samordning, en statisk analysteknik som automatiskt samordnar program, samt samordnade versioner av SMC- och Markovkedjebaserade Monte Carlo-inferensalgoritmer (MCMC). Det sista forskningsproblemet är mer praktiskt och rör den effektiva implementationen av PPL:er. Konkret är bidraget den universella PPL:en Miking CorePPL och dess kompilator. Sammanfattningsvis förbättrar avhandlingens bidrag avsevärt effektiviteten hos Monte Carlo-algoritmer som tillämpas i universella PPL:er.

Probabilistic programming languages (PPLs) allow users to encode arbitrary inference problems, and PPL implementations provide general-purpose automatic inference for these problems. However, constructing inference implementations that are efficient enough is challenging for many real-world problems. Often, this is due to PPLs not fully exploiting available parallelization and optimization opportunities. For example, handling probabilistic checkpoints in PPLs through continuation-passing style transformations or non-preemptive multitasking—as is done in many popular PPLs—often disallows compilation to low-level languages required for high-performance platforms such as GPUs. To solve the checkpoint problem, we introduce the concept of PPL control-flow graphs (PCFGs)—a simple and efficient approach to checkpoints in low-level languages. We use this approach to implement RootPPL: a low-level PPL built on CUDA and C++ with OpenMP, providing highly efficient and massively parallel SMC inference. We also introduce a general method of compiling universal high-level PPLs to PCFGs and illustrate its application when compiling Miking CorePPL—a high-level universal PPL—to RootPPL. The approach is the first to compile a universal PPL to GPUs with SMC inference. We evaluate RootPPL and the CorePPL compiler through a set of real-world experiments in the domains of phylogenetics and epidemiology, demonstrating up to 6x speedups over state-of-the-art PPLs implementing SMC inference.

Probabilistic programming is an approach to reasoning under uncertainty by encoding inference problems as programs. In order to solve these inference problems, probabilistic programming languages (PPLs) employ different inference algorithms, such as sequential Monte Carlo (SMC), Markov chain Monte Carlo (MCMC), or variational methods. Existing research on such algorithms mainly concerns their implementation and efficiency, rather than the correctness of the algorithms themselves when applied in the context of expressive PPLs. To remedy this, we give a correctness proof for SMC methods in the context of an expressive PPL calculus, representative of popular PPLs such as WebPPL, Anglican, and Birch. Previous work have studied correctness of MCMC using an operational semantics, and correctness of SMC and MCMC in a denotational setting without term recursion. However, for SMC inference—one of the most commonly used algorithms in PPLs as of today—no formal correctness proof exists in an operational setting. In particular, an open question is if the resample locations in a probabilistic program affects the correctness of SMC. We solve this fundamental problem, and make four novel contributions: (i) we extend an untyped PPL lambda calculus and operational semantics to include explicit resample terms, expressing synchronization points in SMC inference; (ii) we prove, for the first time, that subject to mild restrictions, any placement of the explicit resample terms is valid for a generic form of SMC inference; (iii) as a result of (ii), our calculus benefits from classic results from the SMC literature: a law of large numbers and an unbiased estimate of the model evidence; and (iv) we formalize the bootstrap particle filter for the calculus and discuss how our results can be further extended to other SMC algorithms. 

Statistical phylogenetic analysis currently relies on complex, dedicated software packages, making it difficult for evolutionary biologists to explore new models and inference strategies. Recent years have seen more generic solutions based on probabilistic graphical models, but this formalism can only partly express phylogenetic problems. Here, we show that universal probabilistic programming languages (PPLs) solve the expressivity problem, while still supporting automated generation of efficient inference algorithms. To prove the latter point, we develop automated generation of sequential Monte Carlo (SMC) algorithms for PPL descriptions of arbitrary biological diversification (birth-death) models. SMC is a new inference strategy for these problems, supporting both parameter inference and efficient estimation of Bayes factors that are used in model testing. We take advantage of this in automatically generating SMC algorithms for several recent diversification models that have been difficult or impossible to tackle previously. Finally, applying these algorithms to 40 bird phylogenies, we show that models with slowing diversification, constant turnover and many small shifts generally explain the data best. Our work opens up several related problem domains to PPL approaches, and shows that few hurdles remain before these techniques can be effectively applied to the full range of phylogenetic models. Ronquist, Kudlicka, Senderov and colleagues present universal probabilistic programming as a powerful method for modeling and inference in statistical phylogenetics. They provide an accessible introduction to these techniques and apply them in inferring complex patterns of diversification and turnover in birds.

We introduce a dynamic mechanism for the solution of analytically-tractable substructure in probabilistic programs, using conjugate priors and affine transformations to reduce variance in Monte Carlo estimators. For inference with Sequential Monte Carlo, this automatically yields improvements such as locallyoptimal proposals and Rao–Blackwellization. The mechanism maintains a directed graph alongside the running program that evolves dynamically as operations are triggered upon it. Nodes of the graph represent random variables, edges the analytically-tractable relationships between them. Random variables remain in the graph for as long as possible, to be sampled only when they are used by the program in a way that cannot be resolved analytically. In the meantime, they are conditioned on as many observations as possible. We demonstrate the mechanism with a few pedagogical examples, as well as a linearnonlinear state-space model with simulated data, and an epidemiological model with real data of a dengue outbreak in Micronesia. In all cases one or more variables are automatically marginalized out to significantly reduce variance in estimates of the marginal likelihood, in the final case facilitating a randomweight or pseudo-marginal-type importance sampler for parameter estimation. We have implemented the approach in Anglican and a new probabilistic programming language called Birch.

We introduce a dynamic mechanism for the solution of analytically-tractable substructure in probabilistic programs, using conjugate priors and affine transformations to reduce variance in Monte Carlo estimators. For inference with Sequential Monte Carlo, this automatically yields improvements such as locally-optimal proposals and Rao–Blackwellization. The mechanism maintains a directed graph alongside the running program that evolves dynamically as operations are triggered upon it. Nodes of the graph represent random variables, edges the analytically-tractable relationships between them. Random variables remain in the graph for as long as possible, to be sampled only when they are used by the program in a way that cannot be resolved analytically. In the meantime, they are conditioned on as many observations as possible. We demonstrate the mechanism with a few pedagogical examples, as well as a linear-nonlinear state-space model with simulated data, and an epidemiological model with real data of a dengue outbreak in Micronesia. In all cases one or more variables are automatically marginalized out to significantly reduce variance in estimates of the marginal likelihood, in the final case facilitating a random-weight or pseudo-marginal-type importance sampler for parameter estimation. We have implemented the approach in Anglican and a new probabilistic programming language called Birch.

Probabilistic programming languages (PPLs) make it possible to separate the concerns between probabilistic models and Bayesian inference algorithms. However, to make such inference efficient is technically very challenging, both in terms of execution time performance and inference accuracy. One successful optimization approach is the previously published work on dynamically delayed sampling. This runtime method makes use of analytical relations between random variables to reduce inference variance; however, tracking these relations introduces runtime overhead. Furthermore, implementing the dynamic approach in a statically typed language introduces type problems because delaying the sampling of random variables changes their types. Our work advances the state-of-the-art in two aspects. Firstly, to reduce the runtime overhead, we develop a compile-time version of delayed sampling. By incorporating optimization procedures during compilation, we eliminate the need for runtime relation tracking and consequent overhead. However, the compile-time version may not always be effective due to the program's possible dynamic behavior, such as stochastic branches, or the complexity of handling recursion. Secondly, we introduce constructs to implement dynamically delayed sampling in a statically typed universal PPL. Dynamically delayed sampling in statically typed languages is a viable optimization for complex Bayesian models, whereas simple models ought to be statically optimized. We evaluate both statically and dynamically delayed sampling on real-world examples, such as latent Dirichlet allocation and phylogenetic models, and implement the methods in a statically typed PPL, Miking CorePPL.

Probabilistic programming languages (PPLs) make encoding and automatically solving statistical inference problems relatively easy by separating models from the inference algorithm. A popular choice for solving inference problems is to use Monte Carlo inference algorithms. For higher-order functional PPLs, these inference algorithms rely on execution suspension to perform inference, most often enabled through a full continuation-passing style (CPS) transformation. However, standard CPS transformations for PPL compilers introduce significant overhead, a problem the community has generally overlooked. State-of-the-art solutions either perform complete CPS transformations with performance penalties due to unnecessary closure allocations or use efficient, but complex, low-level solutions that are often not available in high-level languages. In contrast to prior work, we develop a new approach that is both efficient and easy to implement using higher-order languages. Specifically, we design a novel static suspension analysis technique that determines the parts of a program that require suspension, given a particular inference algorithm. The analysis result allows selectively CPS transforming the program only where necessary. We formally prove the correctness of the suspension analysis and implement both the suspension analysis and selective CPS transformation in the Miking CorePPL compiler. We evaluate the implementation for a large number of Monte Carlo inference algorithms on real-world models from phylogenetics, epidemiology, and topic modeling. The evaluation results demonstrate significant improvements across all models and inference algorithms.