Verifying Performance Properties of Probabilistic Inference

TL;DR

This paper explores formal verification methods for hybrid probabilistic inference systems to ensure performance guarantees, focusing on exact-approximate division and memory bounds.

Contribution

It introduces verification techniques for hybrid inference systems, including semi-symbolic inference and delayed sampling, to guarantee performance and memory bounds.

Findings

Semi-symbolic Inference provides limited guarantees on inference division.

Work extends guarantees to complex programs via program analysis.

Verification ensures bounded memory usage in delayed sampling systems.

Abstract

In this extended abstract, we discuss the opportunity to formally verify that inference systems for probabilistic programming guarantee good performance. In particular, we focus on hybrid inference systems that combine exact and approximate inference to try to exploit the advantages of each. Their performance depends critically on a) the division between exact and approximate inference, and b) the computational resources consumed by exact inference. We describe several projects in this direction. Semi-symbolic Inference (SSI) is a type of hybrid inference system that provides limited guarantees by construction on the exact/approximate division. In addition to these limited guarantees, we also describe ongoing work to extend guarantees to a more complex class of programs, requiring a program analysis to ensure the guarantees. Finally, we also describe work on verifying that inference systems using delayed sampling -- another type of hybrid inference -- execute in bounded memory. Together, these projects show that verification can deliver the performance guarantees that probabilistic programming languages need.