Contexte et atouts du poste
Le postdoc se déroulera dans le cadre d'une collaboration entre Guillaume Baudart, Marc Lelarge et Nicolas Tabareau, 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 des bibliothèques Rocq et Lean.
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 Guillaume Baudart, Marc Lelarge et Nicolas Tabareau. Cependant, il y aura des réunions fréquentes, et des rencontres régulières en personne, avec les co-superviseurs et les participants 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, en utilisant des techniques modernes d'IA, et en particulier des modèles de langue de grande taille (LLM), sur :
1. les traductions automatisées à partir de, vers et entre les bibliothèques de mathématiques formalisées, entre assistants de preuves ou au sein du même assistant de preuve,
2. l'automatisation de la documentation et de la recherche de théorème,
3. la construction de preuve par collaboration entre plusieurs agents et des prouveurs.
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 techniques de programmation agentique, d'apprentissage supervisé (finetuning), et d'apprentissage par renforcement (reinforcement learning) sur des modèle existants, et d'évaluer la pertinence de chaque méthode.
Les résultats attendus de ce travail sont des publications de recherche, la production de logiciels et des présentations publiques en workshop
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 par exemple :
4. Training Chain-of-Thought via Latent-Variable Inference
5. Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
6. Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning
7. Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction
8. Solving Formal Math Problems by Decomposition and Iterative Reflection
9. Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
10. Hilbert: Recursively Building Formal Proofs with Informal Reasoning
Collaboration
La personne recrutée sera principalement en contact avec Cyril Cohen à Lyon, ainsi que Guillaume Baudart, Marc Lelarge 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
11. Déterminer comment entraîner (finetuning et/ou reinforcement learning), et programmer des agents sur des modèles existants et combiner ces méthodes pour remplir les missions énoncées ci-dessus.
12. Mettre en place l'infrastructure pour implémenter et reproduire ces méthodes.
13. Implémenter des extensions de Rocq ou Lean afin d'extraire des données pertinentes.
14. Documenter les logiciels résultants.
15. Collecter les résultats, exécuter des benchmarks et publier des articles scientifiques.
Activités supplémentaires
16. Concevoir des interfaces utilisateur pour rendre l'outil résultant plus largement utilisable.
17. Déterminer un schéma de maintenance à long terme pour ceux-ci.
18. Mise en place de scripts et process documentés à destination d'utilisateur·ices non spécialistes.
Compétences
Compétences techniques et niveau requis :
19. Connaître les bases d'au moins Lean et Rocq.
20. Comprendre les différences entre les diverses techniques d'apprentissage artificiel.
21. Savoir mettre en oeuvre l'entrainement d'un modèle en pratique.
Langues :
22. Anglais courant.
Compétences relationnelles :
23. Communiquer ses résultats.
24. Travailller en autonomie, tout en discutant des stratégies à adopter avec les autres membres du projets.
25. Écouter les retours.
Compétences additionnelles appréciées :
26. Expertise en LLM.
27. Expertise en Rocq et Lean.
28. Git, Github, Hugging Face, WandB, et autres plateformes de partage de code, model etc.
29. Éxécuter du code sur Jean Zay
Avantages
30. Restauration subventionnée
31. Transports publics remboursés partiellement
32. 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)
33. Possibilité de télétravail (90 jours par an flottants) et aménagement du temps de travail (sauf pour les stagiaires et apprentis)
34. Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
35. Accès à la formation professionnelle
36. Participation employeur mutuelle santé (sous conditions)
Rémunération
A partir de 3085 € brut / mois
En cliquant sur "JE DÉPOSE MON CV", vous acceptez nos CGU et déclarez avoir pris connaissance de la politique de protection des données du site jobijoba.com.