Advanced Research Position – Intelligence artificielle pour les mathématiques formelles : qualité, évaluation et traduction des preuves générées par les modèles de langage

Advanced Research Position – Intelligence artificielle pour les mathématiques formelles : qualité, évaluation et traduction des preuves générées par les modèles de langage Download job offer in PDF format The offer description be low is in French Renewable contract : Yes Level of qualifications required : PhD or equivalent Fonction : Tempary Research Position Context Les modèles de langage de dernière génération (Frontier LLMs) produisent désormais des preuves Lean correctes à un niveau de compétition, voire de recherche. Deux verrous majeurs subsistent toutefois pour que ces capacités profitent réellement aux communautés de la formalisation et des mathématiques : la qualité du code produit, souvent très en deçà des standards de Mathlib et de la lisibilité attendue par les mathématiciens, et le cloisonnement des bibliothèques formelles entre assistants à la preuve (Mathlib dans Lean, Mathematical Components dans Rocq), voire entre versions successives d'un même assistant. Le poste s'inscrit dans le cadre du projet BELLE, soutenu par le AI for Math Fund (Renaissance Philanthropy) au sein de l'équipe Argo (Inria, Paris) avec ses partenaires : - BELLE est un projet ouvert et collaboratif qui vise à mesurer et à optimiser la qualité du code Lean généré par IA, au-delà de la seule correction. Il prévoit la définition d'une suite de métriques de qualité validée par la communauté Mathlib, la constitution d'un jeu de données de préférences annoté par des experts (*BELLE-Prefs*), un pipeline d'évaluation open source et un agent d'audit de qualité, puis le fine-tuning de modèles par apprentissage par renforcement (GRPO) à partir des métriques calibrées. Comment obtenir d'un modèle de langage du code formel qui soit non seulement correct, mais aussi concis, lisible, réutilisable et conforme aux usages des bibliothèques cibles. Les métriques et les données de préférence produites par BELLE fournissent précisément les signaux d'évaluation et de récompense dont les modèles de back-translation ont besoin. L'Advanced Research Position est créée pour prendre en charge l'axe intelligence artificielle de cette direction de recherche. Le poste offre un environnement scientifique rare, à l'interface de l'apprentissage profond, des assistants à la preuve et des mathématiques. Assignment Missions La personne recrutée assurera la responsabilité scientifique et technique de l'axe « modèles de langage » du projet BELLE en lien avec le responsable scientifique. Forte d'une expérience confirmée en recherche en apprentissage automatique et d'une solide culture mathématique, elle conduira les travaux de recherche, encadrera les personnels non permanents recrutés sur ces thématiques et portera le dialogue avec les communautés de la formalisation. Elle pilotera la conception du jeu de données de préférences BELLE-Prefs : sélection de plus de 200 tâches de formalisation sur trois niveaux de difficulté (licence, compétition, recherche), génération de solutions candidates à partir de modèles frontière, de stratégies de prompting, d'outils de recherche de preuve et de l'historique des pull requests de Mathlib, et protocole d'annotation experte selon deux perspectives complémentaires (standards de contribution à Mathlib d'une part, lisibilité et clarté mathématique d'autre part). Elle dirigera la calibration des métriques automatiques (analyse statique, profilage, LLM-as-a-judge) sur les jugements humains, puis l'étude de fine-tuning par GRPO utilisant ces métriques comme signal de récompense, incluant la comparaison entre modèle de base, modèle guidé par le guide de bonnes pratiques (agent.md) et modèle fine-tuné, ainsi que l'analyse de la synergie entre qualité et correction. Elle veillera à la mutualisation de l'infrastructure d'entraînement et d'évaluation (Jean Zay), à la reproductibilité des expériences et à la diffusion ouverte de l'ensemble des artefacts produits (jeux de données, pipelines, modèles, baselines). Encadrement et collaboration La personne recrutée encadrera au quotidien le post-doctorant du projet BELLE ainsi que les stagiaires. Elle animera les réunions de coordination hebdomadaires et le dépôt de projet partagé, et associera les doctorants des équipes partenaires aux discussions afin d'entretenir un environnement académique riche et créatif. Elle évoluera dans un environnement fortement collaboratif, à l'interface entre intelligence artificielle, méthodes formelles et mathématiques. Elle travaillera en étroite interaction avec les équipes PiCube, l'ENS, les partenaires académiques du projet BELLE (chercheurs en méthodes formelles, mathématicien professionnel) et les communautés Lean/Mathlib et Rocq. Ces collaborations donneront lieu à des échanges scientifiques réguliers et à des interactions avec les autres initiatives soutenues par le AI for Math Fund (Mathlib Initiative, Formal Frontier, LeanEval). Main activities Principales activités 1. Définir avec les partenaires la feuille de route scientifique de l'axe IA du projet BELLE et des travaux de traduction entre assistants à la preuve, en assurer le suivi (jalons, livrables, ressources de calcul) et rendre compte de l'avancement aux partenaires et au bailleur. 2. Concevoir et superviser la construction des jeux de données : tâches de formalisation et solutions candidates pour BELLE-Prefs ; corpus de preuves bas niveau / haut niveau issus de la compilation de Mathlib, de Mathematical Components et de l'intégration continue de Rocq ; protocoles d'annotation experte, étude pilote et mesure de l'accord inter-annotateurs. 3. Développer et calibrer les méthodes d'évaluation de la qualité du code formel : métriques dures (métaprogrammation Lean 4, profilage de l'élaboration), métriques douces (LLM-as-a-judge guidé par agent.md), agrégation en profils de qualité interprétables, corrélation avec les jugements humains (τ de Kendall, ρ de Spearman) et baselines de qualité des modèles frontière. 4. Conduire les expériences d'entraînement et d'adaptation de modèles ouverts : fine-tuning par préférences (DPO) et par renforcement (GRPO) avec récompenses de qualité, apprentissage de la *back-translation* bas niveau → haut niveau, études comparatives et analyse des résultats, sur les infrastructures GPU nationales. 5. Encadrer les post-doctorants, ingénieurs et stagiaires affectés à ces travaux, et garantir la qualité logicielle, la reproductibilité et la maintenabilité des artefacts livrés (versionnage des chaînes Lean/Mathlib et Rocq, documentation). 6. Rédiger les publications scientifiques, la documentation technique et les rapports d'avancement associés aux travaux réalisés. Activités complémentaires 1. Piloter l'engagement avec les communautés : entretiens structurés avec les mainteneurs de Mathlib, échanges avec des mathématiciens professionnels, co-construction et itération du guide de bonnes pratiques (agent.md), recrutement et animation du panel d'annotateurs experts, organisation du séminaire des experts. 2. Diffuser les résultats et les outils auprès des communautés Lean, Rocq et intelligence artificielle : dépôts open source (BELLE-Prefs, pipeline d'évaluation et agent d'audit, modèles, outils de traduction), présentations sur Lean Zulip et à Lean Together, communications dans les conférences d'apprentissage automatique et de méthodes formelles. 3. Assurer une veille scientifique et technologique sur les modèles de langage pour les mathématiques (prouveurs neuronaux, autoformalisation, apprentissage par renforcement pour les LLM) et sur l'évolution des écosystèmes Lean/Mathlib et Rocq, et contribuer à l'animation de la communauté autour de ces thématiques. Skills Compétences techniques et niveau requis - Doctorat en mathématiques, en informatique ou dans un domaine connexe, suivi d'une expérience de recherche confirmée en apprentissage automatique, en milieu académique ou industriel, attestée par des publications et par la conduite de projets de recherche de bout en bout. - Expertise des grands modèles de langage : entraînement et adaptation (fine-tuning supervisé, DPO, GRPO et apprentissage par renforcement), évaluation (benchmarks, LLM-as-a-judge), prompting et conception d'agents. - Maîtrise de la méthodologie d'évaluation empirique : conception de métriques et de protocoles d'annotation, construction et curation de jeux de données, mesure de l'accord inter-annotateurs, analyse statistique et interprétation des résultats. - Très bonne maîtrise de Python et de l'écosystème d'apprentissage profond (PyTorch, Hugging Face, moteurs d'inférence), expérience de l'entraînement distribué sur clusters GPU. - Maîtrise des outils de développement collaboratif (Git, intégration continue, gestion de projets logiciels) et des pratiques de reproductibilité. - Solide culture mathématique permettant d'apprécier la lisibilité et la clarté de formalisations et de dialoguer avec des mathématiciens professionnels. Langues - Anglais scientifique : niveau C1 minimum, bilingue souhaité (rédaction d'articles, animation d'échanges avec une communauté internationale). - Français : capacité à évoluer dans un environnement de travail francophone. Compétences relationnelles - Leadership scientifique et capacité à fédérer une équipe pluridisciplinaire (IA, méthodes formelles, mathématiques, génie logiciel). - Expérience avérée de l'encadrement de chercheurs et d'ingénieurs, goût pour le mentorat. - Autonomie, sens de l'organisation et rigueur dans la conduite de projets financés comportant des jalons et des livrables. - Qualités de communication écrite et orale ; capacité à interagir avec des communautés de pratique (Lean/Mathlib, Rocq) et avec des interlocuteurs non spécialistes de l'IA. - Curiosité scientifique, goût pour l'expérimentation et l'apprentissage continu dans un domaine en évolution rapide. Compétences additionnelles appréciées - Expérience en IA pour les mathématiques : résolution de problèmes de compétition, autoformalisation, prouveurs neuronaux, recherche d'information structurée sur des corpus mathématiques. - Expérience du transfert de la recherche vers des outils ou produits d'IA, et de la collaboration avec des partenaires industriels. - Contributions à des projets open source ou à des initiatives communautaires en IA pour les mathématiques. Benefits package • 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 et aménagement du temps de travail • Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.) • Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria) • Accès à la formation professionnelle • Sécurité sociale Apply for this position Share • Facebook • Linkedin • Twitter • Email General Information • Theme/Domain : Optimization, machine learning and statistical methods Statistics (Big data) (BAP E) • Town/city : Paris • Inria Center : Centre Inria de Paris • Starting date : 2026-12-01 • Duration of contract : 12 months • Deadline to apply : 2026-11-14 Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed. Instruction to apply Defence Security : This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment. Recruitment Policy : As part of its diversity policy, all Inria positions are accessible to people with disabilities. Contacts • Inria Team : ARGO • Recruiter : Lelarge Marc / Marc.Lelarge@inria.fr About Inria Inria, the French national institute for research in digital science and technology, supports the French government in national research and innovation strategies in the digital field, acting as Digital Programs Agency. Inria leads over 300 research and innovation projects with its 3,500 scientists, engineers, and support staff, in partnership with universities and the digital ecosystem (businesses, entrepreneurs, and public stakeholders). Together, we explore strategic fields such as artificial intelligence, cybersecurity, quantum computing, cloud technologies, digital transformation in healthcare, digital twins, and digital technologies for defence. We develop practical solutions such as software, tech startups, partnerships with national companies, and cutting-edge training programmes. Our goal is to drive scientific, technological, and industrial excellence to ensure France’s digital sovereignty.