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 H/F - INRIA

A propos d'Inria

Inria, l'institut national de recherche dans les sciences et technologies du numérique, est en appui de l'État pour les stratégies nationales de recherche et d'innovation du numérique en tant qu'Agence de programmes. Inria mène plus de 300 projets de recherche et d'innovation avec ses 3500 scientifiques, ingénieurs et personnels d'appui, en partenariat avec les universités et l'écosystème numérique (entreprises, entrepreneurs, acteurs publics). Ensemble, nous explorons des domaines clés comme l'intelligence artificielle, la cybersécurité, l'informatique quantique, le Cloud, la transformation numérique de la santé, les jumeaux numériques ou encore les technologies numériques pour la défense. Nous construisons des solutions concrètes telles que des logiciels, des startups technologiques, des partenariats avec les entreprises du tissu national et des formations de pointe. Notre objectif : l'impact scientifique, technologique et industriel au service de la souveraineté numérique de la France.

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

Contrat renouvelable : Oui

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Chercheur contractuel

Contexte et atouts du poste

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 :

- BELLEest 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-translationont 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.

Mission confiée

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).

Principales activités

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.

Compétences

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.

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 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 oeuvres sociales d'Inria)
• Accès à la formation professionnelle
• Sécurité sociale