Post-Doctorant F/H Apprentissage artificiel pour la traduction entre bibliothèques de mathématiques formalisées.
Type de contrat : CDD
Niveau de diplôme exigé : Thèse ou équivalent
Fonction : Post-Doctorant
A propos du centre ou de la direction fonctionnelle
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.
Contexte et atouts du poste
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 et à distance avec Nicolas Tabareau de l'équipe GALINETTE à Nantes. 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 confiée
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 et Nicolas Tabareau, 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.
Principales activités
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
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.
Avantages
- 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)
Rémunération
2788 € brut / mois
Informations générales
- Thème/Domaine : Architecture, langages et compilation
- Ville : Lyon
- Centre Inria : Centre Inria de Lyon
- Date de prise de fonction souhaitée : 2024-11-01
- Durée de contrat : 2 ans
- Date limite pour postuler : 2024-10-31
Attention: Les candidatures doivent être déposées en ligne sur le site Inria. Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
Consignes pour postuler
Les candidatures doivent être déposées en ligne sur le site Inria.
Le traitement des candidatures adressées par d'autres canaux n'est pas garanti.
Sécurité défense :
Ce poste est susceptible d’être affecté dans une zone à régime restrictif (ZRR), telle que définie dans le décret n°2011-1425 relatif à la protection du potentiel scientifique et technique de la nation (PPST). L’autorisation d’accès à une zone est délivrée par le chef d’établissement, après avis ministériel favorable, tel que défini dans l’arrêté du 03 juillet 2012, relatif à la PPST. Un avis ministériel défavorable pour un poste affecté dans une ZRR aurait pour conséquence l’annulation du recrutement.
Politique de recrutement :
Dans le cadre de sa politique diversité, tous les postes Inria sont accessibles aux personnes en situation de handicap.
Contacts
- Équipe Inria : CASH
-
Recruteur :
Cohen Cyril / cyril.cohen@inria.fr
L'essentiel pour réussir
Le ou la candidate devra manifester un intérêt pour la constructions de bibliothèques mathématiques formalisées et l'apprentissage automatique. Bien qu'une formation approfondie en assistant de preuve ne soit pas attendue, il est important d'en connaître les principes généraux et d'avoir envie d'en apprendre plus. De la même manière, il n'est pas nécessaire d'être expert en IA, mais il est attendu d'en connaitre assez pour pouvoir se mettre à jour rapidement (de manière autonome ou bien au contact des membres du projet), et d'avoir la volonté de mettre en oeuvre des techniques d'apprentissage artificiel en pratique.
A propos d'Inria
Inria est l’institut national de recherche dédié aux sciences et technologies du numérique. Il emploie 2600 personnes. Ses 215 équipes-projets agiles, en général communes avec des partenaires académiques, impliquent plus de 3900 scientifiques pour relever les défis du numérique, souvent à l’interface d’autres disciplines. L’institut fait appel à de nombreux talents dans plus d’une quarantaine de métiers différents. 900 personnels d’appui à la recherche et à l’innovation contribuent à faire émerger et grandir des projets scientifiques ou entrepreneuriaux qui impactent le monde. Inria travaille avec de nombreuses entreprises et a accompagné la création de plus de 200 start-up. L'institut s'efforce ainsi de répondre aux enjeux de la transformation numérique de la science, de la société et de l'économie.