A Verified Compiler for Probability Density Functions

TL;DR

This paper presents a formally verified compiler for probability density functions implemented within Isabelle, ensuring correctness and soundness through rigorous proof and refinement techniques.

Contribution

It introduces a fully verified, executable density compiler for a probabilistic language within a theorem prover, combining formal proof with code generation.

Findings

Successfully formalized the compiler in Isabelle

Proved the compiler's soundness with respect to semantics

Generated executable density functions from probabilistic programs

Abstract

Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a simple probabilistic functional language. In this work, we implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w.r.t. the semantics of the source and target language. Together with Isabelle's code generation for inductive predicates, this yields a fully verified, executable density compiler. The proof is done in two steps, using a standard refinement approach: first, an abstract compiler working with abstract functions modelled directly in the theorem prover's logic is defined and proven sound. Then, this compiler is refined to a concrete version that returns a target-language expression.