Scalable Analysis of Probabilistic Models and Programs

Probabilistic programs describe recipes on how to infer conclusions about big data from a mixture of uncertain data and real-world observations. Bayesian networks, a key model in decision-making, are simple instances of such programs. Probabilistic programs are used to steer autonomous robots and self-driving cars, are key to describe security mechanisms, and naturally encode randomised algorithms. Due to their learning ability, they are rapidly encroaching on AI and probabilistic machine learning.

This talk focuses on syntax-based verification of discrete probabilistic programs. We will show how weakest pre-condition style reasoning can be used to determine quantitative program properties such as the probability of divergence, bounds on the expected outcomes of program expressions, or the program’s expected run-time. Complementary to Holtzen’s talk on straight-line code, we focus primarily on how to treat possibly unbounded loops and recursion.

We will present automated methods such as k-induction and how to find loop invariants in a CEGIS-like fashion. An outlook will be given of some alternative automated techniques for program equivalence and how to exploit model checking for obtaining lower bounds on loops in probabilistic programs.

Probabilistic Circuits (PCs) are a unified framework for tractable probabilistic models that support efficient computation of various probabilistic queries (e.g., marginal probabilities). One key challenge is to scale PCs to model large and high-dimensional real-world datasets: we observe that as the number of parameters in PCs increases, their performance immediately plateaus. This phenomenon suggests that the existing optimizers fail to exploit the full expressive power of large PCs. We propose to overcome such bottleneck by latent variable distillation: we leverage the less tractable but more expressive deep generative models to provide extra supervision over the latent variables of PCs. Specifically, we extract information from Transformer-based generative models to assign values to latent variables of PCs, providing guidance to PC optimizers. Experiments on both image and language modeling benchmarks (e.g., ImageNet and WikiText-2) show that latent variable distillation substantially boosts the performance of large PCs compared to their counterparts without latent variable distillation. In particular, on the image modeling benchmarks, PCs achieve competitive performance against some of the widely-used deep generative models, including variational autoencoders and flow-based models, opening up new avenues for tractable generative modeling.

Neurosymbolic AI (NeSy) is regarded as the third wave in AI. It aims at combining knowledge representation and reasoning with neural networks. Numerous approaches to NeSy are being developed and there exists an “alphabet soup” of different systems, whose relationships are often unclear. I will discuss the state-of-the-art in NeSy and argue that there are many similarities with statistical relational AI (StarAI).
Taking inspiration from StarAI, and exploiting these similarities, I will argue that Neurosymbolic AI = Logic + Probability + Neural Networks. I will also provide a recipe for developing NeSy approaches: start from a logic, add a probabilistic interpretation, and then turn neural networks into “neural predicates”. Probability is interpreted broadly here and is necessary to provide a quantitative and differentiable component to the logic. At the semantic and the computation level, one can then combine logical circuits (ako proof structures) labeled with probability, and neural networks in computation graphs.

I will illustrate the recipe with NeSy systems such as DeepProbLog, a deep probabilistic extension of Prolog, and DeepStochLog, a neural network extension of stochastic definite clause grammars (or stochastic logic programs).

The key references of the talk are as follows: [1, 2, 3].

Probabilistic model checking is an automated technique for the formal verification of stochastic systems. This tutorial will provide an introduction to some of the key ingredients of this technique, giving a particular focus on the similarities and differences with some of the other fields represented at the seminar, such as probabilistic programming, probabilistic circuits and, probabilistic planning.
I will cover: (i) the types of probabilistic models typically used; (ii) the use of temporal logic to formalise quantitative behavioural specifications, in particular for models such as Markov chains and Markov decision processes; (iii) the solution techniques usually used by probabilistic model checking tools, and the approaches taken to improve scalability and efficiency; and (iv) modelling languages for probabilistic verification. In the final part of the talk, I will discuss how this framework has been extended to support multi-agent systems modelled as stochastic games.

In a recent series of works, we investigate optimizing strategies in Markov decision processes (MDPs) using Monte Carlo Tree Search (MCTS). We introduce symbolic advice to enhance MCTS, biasing its selection and simulation strategies while maintaining its theoretical guarantees. Efficient implementation of symbolic advice is achieved using QBF and SAT solvers. Additionally, we integrate formal methods and deep learning to produce superior receding horizon policies in large MDPs. Model-checking techniques guide MCTS for high-quality decision sampling, which subsequently trains a neural network to imitate the sampled policy. This network can guide low-latency MCTS online searches or serve as an independent policy when quick responses are vital. Statistical model checking identifies areas needing extra samples and highlights discrepancies between the neural network and the offline policy. Our methodologies are validated using the Pac-Man and Frozen Lake environments, benchmarks in evaluating reinforcement-learning algorithms. The results outperform standard MCTS and human players.
The main related papers to the talk are as follows: [1, 2, 3].

Parametric Bayesian networks (pBNs) are extensions of Bayesian networks that allow conditional probability tables (CPTs) to include unknown parameters rather than concrete probabilities. We present in this talk alternative techniques to find the correct values for the parameters with respect to a given constraint. The key is to translate (a) pBNs to parametric Markov chains (pMCs) and (b) pBN constraints to reachability constraints. This allows exploiting the state-of-the-art parameter synthesis techniques for pMCs to target pBN problems including sensitivity analysis, (minimal-change) parameter tuning, and parameter space partitioning. We address pBNs with an arbitrary number of parameterized CPTs and with arbitrary dependencies between the parameters. This lifts the limitations of the existing pBN techniques. Our experimental results indicate that our techniques scale up to 800 unknown parameters for large Bayesian networks with $\sim 100$ random variables.

Planning aims to find sequences of actions that achieve a goal or optimize a cost-based objective given an initial starting state. Modern planning methods seek to leverage the structure in symbolic domain specification languages to improve the efficiency of the search process. The Relational Dynamic Influence Diagram Language (RDDL) is a probabilistic programming language that has been developed to compactly model real-world stochastic planning problems, i.e., Markov Decision Processes (MDPs), and specifically factored MDPs with highly structured transition and reward functions. In this tutorial, we will cover the basics of RDDL and present recent language extensions and capabilities through the incremental development and extension of running examples based on real-world domains. We will also introduce a range of planning methodologies that leverage RDDL structure covering Monte Carlo Tree Search (MCTS), mathematical programming, gradient-based optimization, and symbolic methods.

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.

One of the most well-studied and highly performing planning approaches used in Model-Based Reinforcement Learning (MBRL) is Monte-Carlo Tree Search (MCTS). Key challenges of MCTS-based MBRL methods remain dedicated deep exploration and reliability in the face of the unknown, and both challenges can be alleviated through principled epistemic uncertainty estimation in the predictions of MCTS. We present two main contributions: First, we develop methodology to propagate epistemic uncertainty in MCTS, enabling agents to estimate the epistemic uncertainty in their predictions. Second, we utilize the propagated uncertainty for a novel deep exploration algorithm by explicitly planning to explore. We incorporate our approach into variations of MCTS-based MBRL approaches with learned and provided models, and empirically show deep exploration through successful epistemic uncertainty estimation achieved by our approach. We compare to a non-planning-based deep-exploration baseline, and demonstrate that planning with epistemic MCTS significantly outperforms non-planning based exploration in the investigated setting.