Abstraction is a fundamental tool in the analysis and verification of programs. Typically, a program abstraction selectively models particular aspects of the original program while utilizing non-determinism to conservatively account for other behaviors. However, non-deterministic abstractions do not directly apply to the analysis of probabilistic programs. We recently introduced probabilistic program abstractions, which explicitly quantify the non-determinism found in a typical over-approximate program abstraction by using a probabilistic choice. These probabilistic program abstractions are themselves probabilistic programs.

Here we illustrate probabilistic program abstractions by example in the context of predicate abstraction, and describe their application to probabilistic program inference. There is no universal solution to inference: every probabilistic program has subtle properties (for example, sparsity, continuity, conjugacy, submodularity, and discreteness) that require different inference strategies (for example, sampling, message passing, knowledge compilation, or path analysis). We propose to utilize probabilistic program abstractions to automatically decompose probabilistic program inference into several simpler inference problems. This general mechanism for breaking a complex query into sub-queries will allow the use of heterogeneous inference algorithms for different concrete sub-queries, and the abstraction will make precise how these sub-queries together can be used to produce the answer to the original inference query.