Exact Inference for Probabilistic Programs

What is PSI?


PSI is a solver which takes as input a probabilistic program and automatically computes the exact probability density function (PDF) represented by that program. To compute the PDF, PSI uses symbolic inference techniques. It handles probabilistic programs with both discrete and continuous distributions. PSI assumes that loops in the probabilistic program are of finite length. PSI's ability to compute exact PDFs is in contrast to almost all existing techniques which are approximate in nature (these use sampling or variational methods).

The PDF computed by PSI can be used for a variety of queries, including computing the probability of assertions, expectations, performing inference, computing differences, quantifying the loss of precision, and others. Because of this, PSI is a useful platform for encoding applications from various domains that require probabilistic reasoning.

Download


Here is the artifact submitted to CAV which was approved: PSI Source Code, Benchmarks and Documentation. We are in the process of open sourcing the entire framework on GitHub and providing additional documentation for using the tool.

Publications


The following paper describes the method behind the PSI solver:

Team

Timon Gehr

Timon
Gehr

PhD Student
ETH Zurich
Website

Sasa Misailovic

Sasa Misailovic

Assistant Professor
UIUC
Website

Martin Vechev

Martin Vechev

Assistant Professor
ETH Zurich
Website