Post-Doctorant F/H Aprentissage artificiel pour la traduction entre bibliothèques de mathématiques formalisées.

Le centre Inria de Lyon est le 9ème centre de recherche Inria. Créé en janvier 2022, il regroupe environ 300 personnes au sein de 17 équipes de recherche et des services supports à la recherche.

Ses équipes sont localisées à Villeurbanne, à Lyon Gerland, ainsi qu’à Saint-Etienne.

Le centre de Lyon est présent dans les domaines du logiciel, du calcul distribué et haute performance, des systèmes embarqués, du calcul quantique et de respect de la vie privée dans le monde numérique, mais aussi de la santé et de la biologie numériques.

Le postdoc se déroulera dans le cadre du défi Inria LLM4Code, dont les objectifs sont d'appliquer des techniques d'apprentissage automatique à la génération automatique de code, et en particulier pour les bibliothèques d'assistants de preuves, telles que les bibliothèques Coq.

La recherche sera menée dans le laboratoire LIP de l'ENS Lyon sous la supervision locale de Cyril Cohen, au sein de l'équipe CASH. Cependant, il y aura des réunions fréquentes, et des rencontres régulières en personne, avec les participants des autres lots de travail du projet LLM4Code.

Les frais de déplacement sont couverts dans les limites du barème en vigueur.

Mission :

Avec l'aide des membres des projets et de leurs collaborateurs, la personne recrutée travaillera sur les traductions automatisées à partir de, vers et entre les bibliothèques de mathématiques formalisées en utilisant des techniques modernes d'IA, et en particulier des modèles de langue de grande taille (LLM).

Ces traductions peuvent nécessiter des modifications non triviales des assistants de preuve utilisés, telles que la création de plugins, l'utilisation de méta-programmation, ou la reformulation des bibliothèques de manière à mieux convenir à l'apprentissage automatique.

Il sera également nécessaire de mettre en place des entraînements, des ajustements fins et/ou des techniques RAG sur des modèles existants, et d'évaluer la pertinence de chaque méthode.

Les résultats attendus de ce travail sont des publications de recherche et la production de logiciels.

Pour une meilleure connaissance du sujet de recherche proposé :

L'état de l'art, la bibliographie et les références scientifiques évoluent rapidement. Nous suggérons de lire le récent survey A Survey on Deep Learning for Theorem Proving par Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si, avec un focus particulier sur les publications concernant Coq ou Lean.

Collaboration :

La personne recrutée sera principalement en contact avec Cyril Cohen, mais travaillera également à distance avec d'autres membres de LLM4Code.

Responsabilités :

La personne recrutée sera responsable de la mise en place de l'infrastructure logicielle pour mener les expériences et prendre des initiatives pour les choix de logiciels et de matériel disponible, dans les limites permises par Inria.

Activités principales  :

• Déterminer comment entraîner, ajuster finement, ou utiliser des techniques RAG sur des modèles existants, et combiner ces methodes, pour atteindre la traduction souhaitée.
• Mettre en place l'infrastructure pour implémenter et reproduire ces méthodes.
• Implémenter des extensions de Coq ou Lean afin d'extraire des données pertinentes.
• Documenter les logiciels résultants.
• Collecter les résultats, exécuter des benchmarks et publier des articles scientifiques.

Activités supplémentaires :

• Concevoir des interfaces utilisateur pour rendre l'outil résultant plus largement utilisable.
• Déterminer un schéma de maintenance à long terme pour ceux-ci.

Compétences techniques et niveau requis :

• Connaître les bases d'au moins un assistant de preuve, de préférence en théorie des types dépendents.
• Comprendre les différences entre les diverses techniques d'apprentissage artificiel.
• Savoir mettre en oeuvre l'entrainement d'un modèle en pratique.

Langues :

• Anglais courant.

Compétences relationnelles :

• Communiquer ses résultats.
• Travailller en autonomie, tout en discutant des stratégies à adopter avec les autres membres du projets.
• Écouter les retours.

Compétences additionnelles appréciées :

• Expertise en LLM.
• Expertise en Coq ou Lean.
• Git, Github, Hugging Face, WandB, et autres plateformes de partage de code, model etc.

• Restauration subventionnée
• Transports publics remboursés partiellement
• Congés : 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
• Possibilité de télétravail (90 jours par an flottants) et aménagement du temps de travail (sauf pour les stagiaires et apprentis)
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
• Accès à la formation professionnelle
• Participation employeur mutuelle santé (sous conditions)

2788 € brut / mois