Logic of Probabilistic Programming (Thematic Month 2022)

Probabilities play an increasing role in computer science. Important deterministically-intractable problems admit feasible approximate probabilistic solutions. Probabilistic algorithms are essential in distributed computing and numerical computing (Monte Carlo methods), not to mention the role of probabilistic methods in deep learning (stochastic gradient). Linear logic shows quite useful in this setting because some of the most basic notions of probability theory are linear: Markov chains or kernels, Bayesian networks etc.

The general purpose of this week is not only to present the state of the art on the applications of proof theory, category theory and denotational semantics to the analysis of probabilistic programs and to the foundation of probabilistic formal methods for program and system verification, but also to stress the specificities of Bayesian programming and machine learning where programs represent statistical models.

The program of the week is designed for conveying to the non-specialist a coherent picture of this exciting and very active area.

Les probabilités jouent un rôle croissant en informatique. Ainsi, des problèmes très importants n’acceptent pas de solution déterministe ou seulement des solutions d’une trop grande complexité, mais deviennent approximativement faisables dans un cadre probabiliste. Les algorithmes probabilistes sont aussi essentiels dans les systèmes distribués, en calcul numérique (méthode de Monte Carlo) etc. Sans parler du rôle essentiel des méthodes probabilistes en deep learning (gradient stochastique). La logique linéaire est ici cruciale car certaines des notions les plus fondamentales de la théorie des probabilités sont de nature essentiellement linéaire : c’est le cas par exemple des chaînes et des noyaux de Markov et des réseaux bayésiens. L’objectif général de cette semaine est non seulement de présenter l’état de l’art sur les applications de la théorie de la démonstration, de la théorie des catégories et de la sémantique dénotationnelle à l’analyse des programmes probabilistes, dans la perspective de la mise au point de méthodes formelles pour la vérification et la validation des programmes et des systèmes, mais aussi de mettre l’accent sur les spécificités de la programmation bayésienne et du machine learning dans laquelle les programmes représentent des modèles statistiques. Le programme de la semaine est conçu de façon à permettre aux chercheurs non spécialistes ou débutants de se faire une idée aussi cohérente que possible de ce sujet en pleine ébullition.