Transforming Probabilistic Programs for Model Checking

TL;DR

This paper introduces a static analysis method to transform probabilistic programs into efficient sampling code, automating key model checking tasks and enhancing Bayesian workflows in probabilistic programming.

Contribution

It presents a novel static analysis approach that automates the transformation of probabilistic programs into sampling code, enabling more efficient model checking.

Findings

Automated transformation of probabilistic programs into sampling code.

Application to Stan language for Bayesian workflows.

Improved efficiency in model checking tasks.

Abstract

Probabilistic programming is perfectly suited to reliable and transparent data science, as it allows the user to specify their models in a high-level language without worrying about the complexities of how to fit the models. Static analysis of probabilistic programs presents even further opportunities for enabling a high-level style of programming, by automating time-consuming and error-prone tasks. We apply static analysis to probabilistic programs to automate large parts of two crucial model checking methods: Prior Predictive Checks and Simulation-Based Calibration. Our method transforms a probabilistic program specifying a density function into an efficient forward-sampling form. To achieve this transformation, we extract a factor graph from a probabilistic program using static analysis, generate a set of proposal directed acyclic graphs using a SAT solver, select a graph which will produce provably correct sampling code, then generate one or more sampling programs. We allow minimal user interaction to broaden the scope of application beyond what is possible with static analysis alone. We present an implementation targeting the popular Stan probabilistic programming language, automating large parts of a robust Bayesian workflow for a wide community of probabilistic programming users.