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 construire une base de données de preuves
exprimées dans un langage et dans l'autre,
- d'entraîner un modèle de traduction automatique sur
ces données, en particulier un réseau de neurone,
- d'utiliser le traducteur obtenu pour traduire en Lean des
preuves HOL-Light en se basant sur la forme de termes-preuve commune
entre les systèmes formels.
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 2023.
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