Bayesian Inference by Symbolic Model Checking

TL;DR

This paper introduces a novel approach to Bayesian inference by translating Bayesian networks into Markov chains and utilizing symbolic model checking techniques, demonstrating efficiency on large benchmarks.

Contribution

It presents a new method for Bayesian inference using symbolic model checking and MTBDDs, bridging probabilistic graphical models with formal verification tools.

Findings

Symbolic data structures like MTBDDs improve inference efficiency.

The approach scales well on large Bayesian network benchmarks.

Comparison shows competitive performance with existing AI inference methods.

Abstract

This paper applies probabilistic model checking techniques for discrete Markov chains to inference in Bayesian networks. We present a simple translation from Bayesian networks into tree-like Markov chains such that inference can be reduced to computing reachability probabilities. Using a prototypical implementation on top of the Storm model checker, we show that symbolic data structures such as multi-terminal BDDs (MTBDDs) are very effective to perform inference on large Bayesian network benchmarks. We compare our result to inference using probabilistic sentential decision diagrams and vtrees, a scalable symbolic technique in AI inference tools.