Stage de Master

Apprentissage automatique et traduction de démonstrations formelles

 

 

 

Contexte scientifique

Une même démonstration formelle peut être exprimée dans plusieurs langages différents, soit parce qu'elle a été développée dans des systèmes différents (e.g. Coq, Lean, HOL-Light), soit parce que plusieurs langages coexistent à l'intérieur du même système formel : par exemple un langage de bas niveau (termes-preuves) et un langage de haut niveau (tactiques). La traduction depuis un langage de tactiques vers un langage de termes-preuves est déjà faite : c'est le rôle d'un moteur de tactiques. La traduction inverse est plus difficile. Cependant, cette tâche est est parfaitement adaptée aux dernières méthodes d'apprentissage profond et aux réseaux de neurones.

But du stage

Le but du stage est d'utiliser un système d'apprentissage automatique basé sur du deep learning pour développer une traduction depuis le langage des termes de preuves de Lean vers le langage des tactiques de Lean. Il s'agit : De manière plus générale, l'interopérabilité entre systèmes de preuves est souvent effectuée en traduisant des termes preuves et ce sujet répond au besoin d'avoir aussi ces preuves dans un langage de haut niveau, par exemple pour les modifier ou pour augmenter la collection de théorèmes formalisés à travers les différents systèmes formels.

Encadrement et lieu du stage

Le stage se déroulera de de mars à juillet 2022.
Il sera encadré par Guillaume Lample (Facebook) et Gilles Dowek (Inria et ENS de Paris-Saclay).
Il se déroulera au Laboratoire de méthodes formelles à Paris-Saclay et chez Facebook.

Contact: guillaume.lample@gmail.com, gilles.dowek@ens-paris-saclay.fr