SHF: Medium: Formally Verified Compilation of Probabilistic Programs

Artificial intelligence is becoming an integral part of society, and is poised to affect increasingly many aspects of life. Like any other software, artificial-intelligence applications can have errors with potentially serious consequences. As a result, improving the quality of artificial-intelligence software is a critical challenge.

One promising technology for addressing this challenge is the use of probabilistic programming languages, which let programmers implement artificial-intelligence applications in a simpler and safer way. The focus of this project is to develop techniques and tools to transform probabilistic programs into code executable on a computer. More specifically, the aim is to understand how to make such tools free of errors while being as efficient as possible.

This project develops a verified compiler and runtime for the Stan probabilistic programming language. The compiler is developed in the Coq proof assistant, and connects to CompCert, an existing verified compiler for C programs. Programs written in Stan will be compiled to CompCert C through a succession of transformations, each of which handles a specific feature of Stan.

These program transformations are specific to probabilistic programming languages, and include truncating distributions and re-parameterizing to support constraints on random variables. The runtime implements a Markov Chain Monte Carlo algorithm that uses the compiled program to perform inference. The formal proof defines the semantics of the Stan program as a probability measure and shows that the compiled program asymptotically generates samples from this measure.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.