Probabilistic program semantics – PPS

Probabilities are essential in Computer Science. Many algorithms use probabilistic choices for efficiency or convenience. Recently, probabilistic programming, and more specifically, functional probabilistic programming, has shown crucial in various works in Bayesian inference and Machine Learning. Such languages are used to represent formally statistical models and for developing probabilistic data analysis.

So it is becoming more and more essential to develop formal methods for probabilistic computing (semantics, type systems, logical frameworks for program verification, abstract machines etc.) to systematize the analysis and certification of functional probabilistic programs. This research activity is growing very fast at an international level, especially in the programming languages community. Our goal is to develop such formal methods.

We focus our approach on the notions of linearity and computational resources which are at the core of Linear Logic (LL). We are convinced that the many connections between Proof Theory, Linear Algebra and the Theory of Programming Languages which arise within LL will play a key role in the development of formal methods for probabilistic programming.

This conviction is supported by our most recent results (denotational models for probabilistic programs and their differentials, metrics for program reasoning, typing systems and realizability techniques for almost sure termination, higher-order model checking, algebraic and probabilistic rewriting systems, probabilistic models based on game semantics and geometry of interaction, etc.), thus establishing that our proposal is both topical and timely.

These preliminary results have been achieved by various groups among us, working independently and scattered in different laboratories. One major objective of this project is to join our forces and complementing expertises, organizing our efforts in a strong research program, structured along the following five work-packages.

Probabilities, Differentials and Machine Learning (1), this is the main axis of our proposal defining our long-term objective: give a clear semantical status to the linear methods used in Bayesian inference using LL and to the differential methods used in Machine Learning adapting the basic ideas of differential LL.

(2) Denotational and (3) Operational Semantics: these are the central concepts of the project, where our research is already very active and recognized. Our aim is to push further these investigations throughout the next work-packages.

(4) From Qualitative to Quantitative Observations: we move from the standard approaches to programs equivalence, based on denotational and game models, bisimulations, etc, to more sophisticated instruments based on norms and distances, more relevant in probabilistic programming.

(5) Towards Effective Tools for Quantitative Observations: we extract from the theory developed so far computable devices (type systems, model-checking, etc.) allowing to perform (with suitable restrictions) program quantitative analysis.

This 4 year project gathers 4 partners, IRIF -- coordinator site and LIPN (Paris), I2M (Marseille) and Inria FOCUS (Sophia and Bologna, Italy). It will hire one doctoral student and two post-doc researchers. The coordinator will be Thomas Ehrhard and the other PI's are Giulio Manzonetto, Lionel Vaux and Martin Avanzini.