Abstract:

In this talk, I will give a perspective on inference in Bayes’ networks

(BNs) using program verification. I will argue how weakest precondition

reasoning a la Dijkstra can be used for exact inference (and more). As

exact inference is NP-complete, inference is typically done by means of

simulation. I will show how by means of wp-reasoning exact expected

sampling times of BNs can be obtained in a fully automated fashion. An

experimental evaluation on BN benchmarks demonstrates that very large

expected sampling times (in the magnitude of millions of years) can be

inferred within less than a second. This provides a means to decide

whether sampling-based methods are appropriate for a given BN. The key

ingredients are to reason at program code in a compositional manner.