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

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.