Sémantique des programmes probabilistes – PPS

Les probabilités sont essentielles en informatique. De nombreux algorithmes utilisent des choix probabilistes par souci d'efficacité ou pour des raisons pratiques. Plus récemment, la programmation stochastique, et plus spécialement, la programmation stochastique fonctionnelle, a commencé à jouer un rôle crucial dans différents travaux sur l'inférence bayésienne et en Machine Learning. De tels langages sont utilisés pour représenter formellement des modèles statistiques et en analyse de données probabiliste.

Il devient donc de plus en plus important de développer des méthodes formelles pour la programmation probabiliste (sémantique, systèmes de typage, formalismes logiques pour la vérification, machines abstraites etc) pour systématiser l'analyse et la certification des programmes fonctionnels probabilistes. Cette activité de recherche est en pleine croissance à l'échelle mondiale, notamment dans la communauté des langages de programmation. Notre but est de développer de telles méthodes formelles.

Notre approche se caractérise par l'importance donnée à la linéarité et à l'analyse des ressources calculatoires, qui sont au coeur de la Logique Linéaire (LL). Nous sommes convaincus que les nombreuses connexions entre théorie de la démonstration, algèbre linéaire et théorie des langages de programmation, qui sont apparues en logique linéaire, doivent jouer un rôle central dans le développement de ces méthodes formelles.

Cette conviction est étayée par nos résultats les plus récents (modèles dénotationnels pour les programmes probabilistes et leurs différentielles, métriques pour raisonner sur les programmes, systèmes de typage et techniques de réalisabilité pour la terminaison presque sûre, model-checking d'ordre supérieur, systèmes de réécriture algébriques et probabilistes, modèles probabilistes en sémantique des jeux et en géométrie de l'interaction etc), ce qui montre que notre proposition est pertinente et arrive au bon moment.

Ces résultats préliminaires ont été obtenus par différents groupes parmi nous, travaillant indépendamment et dispersée dans plusieurs laboratoires. Un objectif majeur de ce projet est de coordonner ces forces et ces expertises complémentaires en organisant ces efforts autour de cinq axes scientifiques.

Probabilités, Dérivées et Apprentissage automatique (1), c'est l'axe principal orientant à long terme notre projet: donner un statut sémantique clair aux méthodes utilisées en inférence bayésienne en utilisant la LL, et aux méthodes différentielles de l'apprentissage automatique en adaptant les idées de base de la LL différentielle.

Sémantique dénotationnelle (2) et opérationnelle (3): ce sont les notions centrales du projet, et ce sont des domaines dans lesquels nous sommes très actifs et reconnus. Nous voulons prolonger ces investigations pour fonder les autres axes scientifiques du projet.

(4) Des observations qualitatives aux observations quantitatives: nous voulons passer de l'approche habituelle de l'équivalence de programmes, à base de relations, à une approche plus pertinente dans un cadre probabiliste, à base de normes et de distances.

(5) Vers des outils effectifs pour les observations quantitatives: nous voulons extraire de la théorie développée jusqu'ici des concepts effectifs (systèmes de typage, model-checking etc) permettant, avec des restrictions adaptées, d'effectuer des analyses quantitatives de programmes, avec, nous l'espérons, des applications à l'axe (1).

Ce projet sur 4 ans rassemble 4 partenaires, IRIF - site principal - et LIPN, (Paris), I2M (Marseille), et Inria FOCUS (Sophia et Bologne, Italie). Le projet financera une thèse de doctorat et deux postes de chercheurs post-doctorants de un an chacun. Le coordinateur du projet sera Thomas Ehrhard et les responsables des sites partenaires seront Giulio Manzonetto, Lionel Vaux et Martin Avanzini.