Explore Bayesian inference through the lens of program verification in this 45-minute talk by Joost-Pieter Katoen from RWTH Aachen University. Discover how weakest precondition reasoning can be applied to exact inference in Bayesian networks and learn about automated techniques for determining exact expected sampling times. Gain insights into the practical implications of these methods for deciding the appropriateness of sampling-based approaches for given Bayesian networks. Delve into topics such as probabilistic graphical models, weakest pre-expectations, and Bayesian networks as programs. Examine real-world applications, including student mood prediction and printer troubleshooting in Windows 95. This presentation, part of a workshop on combining logic and learning, offers a unique perspective on the intersection of formal methods and statistical approaches in understanding complex systems.
Bayesian Inference by Program Verification - Joost-Pieter Katoen, RWTH Aachen University
Alan Turing Institute via YouTube
Overview
Syllabus
Intro
nature Perspective
Probabilistic graphical models
Student's mood after an exam
Applications
Probabilistic GCL
Let's start simple
A loopy program For
Weakest pre-expectations
Examples
An operational perspective
Bayesian inference by program verification
Example: sampling within a circle
Weakest precondition of id-loops
Bayesian networks as programs
Soundness
Exact inference by wp-reasoning
Termination proofs: the classical case
Proving almost-sure termination
The symmetric random walk
Asymmetric-in-the-limit random walk
Positive almost-sure termination
Run-time invariant synthesis
Coupon collector's problem
Sampling time for example BN
The student's mood example
Experimental results
Printer troubleshooting in Windows 95
Predictive probabilistic programming
Taught by
Alan Turing Institute
