Bayesian inference, of posterior knowledge from prior knowledge and observed evidence, is typically defined by Bayes’s rule, which says the posterior multiplied by the probability of an observation equals a joint probability. But the observation of a continuous quantity usually has probability zero, in which case Bayes’s rule says only that the unknown times zero is zero. To infer a posterior distribution from a zero-probability observation, the statistical notion of disintegration tells us to specify the observation as an expression rather than a predicate, but does not tell us how to compute the posterior. We present the first method of computing a disintegration from a probabilistic program and an expression of a quantity to be observed, even when the observation has probability zero. Because the method produces an exact posterior term and preserves a semantics in which monadic terms denote measures, it composes with other inference methods in a modular way—without sacrificing accuracy or performance.
Wed 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:20 - 16:00 | |||
14:20 25mTalk | Beginner's Luck: A Language for Property-Based Generators POPL Leonidas Lampropoulos University of Pennsylvania, Diane Gallois-Wong Inria Paris, ENS Paris, Cătălin Hriţcu Inria Paris, John Hughes Chalmers University of Technology, Benjamin C. Pierce University of Pennsylvania, Li-yao Xia ENS Paris Pre-print | ||
14:45 25mTalk | Exact Bayesian Inference by Symbolic Disintegration POPL Pre-print | ||
15:10 25mTalk | Stochastic Invariants for Probabilistic Termination POPL Krishnendu Chatterjee IST Austria, Petr Novotný IST Austria, Djordje Zikelic University of Cambridge | ||
15:35 25mTalk | Coupling proofs are probabilistic product programs POPL |