Compositional imprecise probability: a solution from graded monads and Markov categories
This program is tentative and subject to change.
Imprecise probability is concerned with uncertainty about which probability distributions to use. It has applications in robust statistics and machine learning.
We look at programming language models for imprecise probability. Our desiderata are that we would like our model to support all kinds of composition, categorical and monoidal; in other words, guided by dataflow diagrams. Another equivalent perspective is that we would like a model of synthetic probability in the sense of Markov categories.
Imprecise probability can be modelled in various ways, with the leading monad-based approach using convex sets of probability distributions. This model is not fully compositional because the monad involved is not commutative, meaning it does not have a proper monoidal structure. In this work, we provide a new fully compositional account. The key idea is to name the non-deterministic choices. To manage the renamings and disjointness of names, we use graded monads. We show that the resulting compositional model is maximal and relate it with the earlier monadic approach, proving that we obtain tighter bounds on the uncertainty.
This program is tentative and subject to change.
Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change
15:00 - 16:20 | |||
15:00 20mTalk | A quantitative probabilistic relational Hoare logic POPL Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Benjamin Gregoire INRIA, Davide Davoli Université Côte d’Azur, Inria | ||
15:20 20mTalk | Approximate Relational Reasoning for Higher-Order Probabilistic Programs POPL Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University Pre-print | ||
15:40 20mTalk | Compositional imprecise probability: a solution from graded monads and Markov categories POPL | ||
16:00 20mTalk | Sound and Complete Proof Rules for Probabilistic Termination POPL |