EMBEr · Exploring Moment-Based Equivalence for probabilistic programs

Probabilistic programming has become an increasingly popular paradigm for representing probabilistic models due to the possibility of decoupling model representation and probabilistic inference. As for any class of models, equivalence is a paramount property, as it allows for reduction and comparison. However, the current notion of equivalence for probabilistic programs is very strict, relying on distributional equality and its weaker variants. These existing notions of equivalence are particularly unsuitable for applications where only partial knowledge of the systems is available, a common scenario in Bayesian inference. A common strategy to account for missing information is to resort to summary statistics, i.e. moments.The objective of EMBEr (Exploring Moment-Based Equivalence for probabilistic prograams) is to establish the theoretical, algorithmic, and practical foundations of a new notion of equivalence based on moments comparison. This novel approach aims to determine when two models described by probabilistic programs have the same expectations with respect to a family of functions. The project will comprise both theoretical investigations and the development of a proof-of-concept algorithm and a proof-of-concept tool for equivalence testing. EMBEr will leverage on existing knowledge on moment-based inference and equivalence testing for probabilistic programs, to propose a more flexible notion of equivalence, that will impact formal methods and programming languages, and more broadly, will advance probabilistic modeling, including Bayesian inference and cyber-physical systems.