Probabilistic model checking is an automatic procedure for establishing if a desired property holds in a probabilistic model, aimed at verifying quantitative probabilistic specifications such as the probability of a critical failure occurring or expected time to termination. Much progress has been made in recent years in algorithms, tools and applications of probabilistic model checking, as exemplified by the probabilistic model checker PRISM (www.prismmodelchecker.org). However, the unstoppable rise of autonomous systems, from robotic assistants to self-driving cars, is placing greater and greater demands on quantitative modelling and verification technologies. To address the challenges of autonomy we need to consider collaborative, competitive and adversarial behaviour, which is naturally modelled using game-theoretic abstractions, enhanced with stochasticity arising from randomisation and uncertainty. This paper gives an overview of quantitative verification and strategy synthesis techniques developed for turn-based stochastic multi-player games, summarising recent advances concerning multi-objective properties and compositional strategy synthesis. The techniques have been implemented in the PRISM-games model checker built as an extension of PRISM. 

We develop a quantitative analogue of equational reasoning which we call quantitative algebraic reasoning. We define an indexed equality relation of type a =_e b which we think of as saying that “a is approximately equal to b up to an error of e”. The models are universal algebras defined on metric spaces.
We have interesting examples where we have a quantitative equational theory whose free algebras correspond to well known structures. In each case we have finitary and continuous versions. The cases are: Hausdorff metrics from quantitive semilattices; p-Wasserstein metrics (hence also the Kantorovich metric) from barycentric algebras; and the total variation distance from a particular type of barycentric algebras.

This is a joint work with Gordon Plotkin and Prakash Panangaden; preliminary results have been presented at LICS2016.

In this talk I will discuss a complexity dichotomy for exact query evaluation in probabilistic databases, where each record in the database is an independent probabilistic event. I will show that the data complexity of any relational algebra query, which has no repeating relation symbols and disjunction but may have negation, is either polynomial time or #P-hard, and the tractable queries can be recognised efficiently.

This is joint work with Robert Fink.

We consider an agent trying to bring a system to an acceptable state by repeated probabilistic action (stochastic control). Specifically, in each step the agent observes the flaws present in the current state, selects one of them, and addresses it by probabilistically moving to a new state, one where the addressed flaw is most likely absent, but where one or more new flaws may be present. Several recent works on algorithmizations of the Lov\'{a}sz Local Lemma have established sufficient conditions for such an agent to succeed. Motivated by the paradigm of Partially Observable Markov Decision Processes (POMDPs) we study whether such stochastic control is also possible in a noisy environment, where both the process of state-observation and the process of state-evolution are subject to adversarial perturbation (noise). The introduction of noise causes the tools developed for LLL algorithmization to break down since the key LLL ingredient, the sparsity of the causality (dependence) relationship, no longer holds. To overcome this challenge we develop a new analysis where entropy plays a central role, both to measure the rate at which progress towards an acceptable state is made and the rate at which the noise undoes this progress. The end result is a sufficient condition that allows a smooth tradeoff between the intensity of the noise and the amenability of the system, recovering an asymmetric LLL condition in the noiseless case. To our knowledge, this is the first tractability result for a nontrivial class of POMDPs under stochastic memoryless control.

If people could communicate with and interactively modify the behavior of AI systems, both people and machines could behave more intelligently. Unfortunately, most AI systems are black boxes designed to solve a single narrowly defined problem, such as chess or face recognition or click prediction, and adjusting their behavior requires deep technical expertise. In this talk, I will describe progress towards more transparent and flexible AI systems capable of augmenting rather than just replacing human intelligence, building on the emerging field of probabilistic programming. Probabilistic programming draws on probability theory, programming languages, and system software to provide concise, expressive languages for modeling and general-purpose inference engines that both humans and machines can use. This talk focuses on BayesDB and Picture, domain-specific probabilistic programming platforms being developed by my research group, aimed at augmenting intelligence in the fields of data science and computer vision, respectively. BayesDB, which is open source and in use by organizations like the Bill & Melinda Gates Foundation and JPMorgan, lets users who lack statistics training understand the probable implications of data by writing queries in a simple, SQL-like language. Picture, a probabilistic language being developed in collaboration with Microsoft, lets users solve hard computer vision problems such as inferring 3D models of faces, human bodies and novel generic objects from single images by writing short (<50 line) computer graphics programs that generate and render random scenes. Unlike bottom-up vision algorithms, Picture programs build on prior knowledge about scene structure and produce complete 3D wireframes that people can manipulate using ordinary graphics software. This talk will also briefly illustrate the fundamentals of probabilistic programming using Venture, an interactive platform suitable for teaching and applications in fields ranging from statistics to robotics, and concludes with a summary of current and future research directions.

Many modern machine learning applications involve sensitive correlated data, such private information on users connected together into a social network, and measurements of physical activity of a single user across time. However, the current gold standard of privacy in machine learning, differential privacy, cannot adequately address privacy issues in this kind of data. This work looks at a recent generalization of differential privacy, called Pufferfish, that can be used to address privacy in correlated data. The main challenge in applying Pufferfish to correlated data problems is the lack of suitable mechanisms. In this talk, I will present two such mechanisms -- a general mechanism, called the Wasserstein Mechanism, which applies to any Pufferfish framework, and a more computationally efficient one, called the Markov Quilt Mechanism, that exploits structural properties of the correlation model for computational efficiency.

Constrained sampling and counting are two fundamental problems in data analysis. In constrained sampling the task is to sample randomly, subject to a given weighting function, from the set of solutions to a set of given constraints. This problem has numerous applications, including probabilistic reasoning, machine learning, statistical physics, and constrained-random verification. A related problem is that of constrained counting, where the task is to count the total weight, subject to a given weighting function, of the set of solutions of the given constraints. This problem has applications in machine learning, probabilistic reasoning, and planning, among other areas. Both problems can be viewed as aspects of one of the most fundamental problems in artificial intelligence, which is to understand the structure of the solution space of a given set of constraints. This work focuses on the development of new algorithmic techniques for constrained sampling and counting, based on a universal hashing -- a classical algorithmic technique in theoretical computer science. Many of the ideas underlying the proposed approach were go back to the 1980s, but they have never been reduced to practice. Recent progress in Boolean reasoning is enabling us to reduce these algorithmic ideas to practice, and obtain breakthrough results in constrained sampling and counting, providing a new algorithmic toolbox in design verification, machine learning, probabilistic reasoning, and the like. Joint work with Supratik Chakraborty and Kuldeep S. Meel.

Probabilistic inference in high-dimensional probabilistic models (i.e., with many variables) is one of the central problems of statistical machine learning and stochastic decision making. To date, only a handful of distinct methods have been developed, most notably (MCMC) sampling, decomposition, and variational methods. In this talk, I will introduce a new approach where random projections are used to simplify a high-dimensional model while preserving some of its key properties. These random projections can be combined with traditional variational inference methods (information projections) and combinatorial optimization tools. These novel randomized approaches provide provable guarantees on the accuracy, and outperform traditional methods in a range of domains.

I will survey some algorithmic models that try to capture uncertainty in optimization problems, talk about some example problems, and indicate some of the techniques and ideas used to tackle the uncertainty in these problems and get provable guarantees on the performance of these algorithms.