Création de dataset et entrainement de modèles de traduction entre bibliothèques de preuve formelle

Le centre Inria de l'Université de Rennes est un des neuf centres d’Inria et compte plus d'une trentaine d’équipes de recherche. Le centre Inria est un acteur majeur et reconnu dans le domaine des sciences numériques. Il est au cœur d'un riche écosystème de R&D et d’innovation : PME fortement innovantes, grands groupes industriels, pôles de compétitivité, acteurs de la recherche et de l’enseignement supérieur, laboratoires d'excellence, institut de recherche technologique.

Coq/Rocq et Lean sont logiciels, appelés prouveurs interactifs, conçus pour écrire et valider des preuves de propriétés mathématiques grâce à une interaction entre utilisateurices et machine. Par exemple, ils sont utilisés dans le monde académique ainsi que dans l’industrie pour prouver la correction de programmes critiques et sophistiqués dans des domaines variés (cybersécurité, compilation, architecture, etc.). L’une des forces de ce type de méthodes formelles est son expressivité, qui permet en fait de formaliser et de vérifier des théories mathématiques arbitrairement sophistiquées. De fait, ces prouveurs interactifs sont aussi utilisés par des chercheurs en mathématiques aussi bien que par des chercheurs en méthodes formelles.

Un des grands défi de ce domaine est de démocratiser la production des bibliothèques de code de ces prouveurs, et de leur concevoir un environnement de développement moderne et productif. Le contexte général de ce poste est d’explorer comment les techniques de génération de code basées sur des outils d’IA peuvent se transposer aux prouveurs interactifs.

Dans le cadre du projet européen ERC FRESCO, et en collaboration avec les chercheurs du défi Inria LLM4Code,  la mission de ce poste est plus particulièrement d’explorer la traduction automatique d’énoncés de preuves entre deux de ces systèmes (en particulier de Lean vers Coq/Rocq) à l’aide de Large Language Models (LLM). Nous nous concentrerons plus particulièrement sur deux grandes bibliothèques : mathlib pour Lean, et Mathematical Components (ou mathcomp ) pour Coq. Ces deux bibliothèques partagent un socle théorique commun et sont guidées par des principes similaires en termes de structure et de pratiques. L’objectif sera de traduire les énoncés mathématiques présents dans mathlib, mais absents de mathcomp, en veillant à maintenir la précision des notations mathématiques lors de la traduction. La traduction des scripts de preuve pourra être abordée dans une phase ultérieure.

Bien que des datasets existent en Lean et en Coq/Rocq, il n’existe pas de corpus parallèle pour la traduction entre ces deux systèmes. La personne recrutée aura pour missions :

• De créer un dataset parallèle pour permettre le fine-tuning des LLM si nécessaire.
• D’entraîner un LLM pour effectuer la traduction automatique d’énoncés de preuve de Lean vers Coq.
• D’évaluer les performances d’un modèle de traduction Lean -> Coq/Rocq sur des énoncés de preuves mathématiques.

L’ingénieur sera encadré par une chercheuse spécialiste des prouveurs interactifs (Coq, Lean) ainsi que par un ingénieur en machine learning. Les expérimentations seront menées en collaborations avec une équipe élargie de chercheurs Inria travaillant sur l’intégration d’outils de machine learning dans les prouveurs interactifs.

• Effectuer une recherche bibliographique sur l’état de l’art de la traduction automatique pour les langages disposant de peu de données.
• Construire un dataset parallèle à partir des énoncés disponibles dans mathlib et mathcomp et d’expériences existantes entre des énoncés disponibles dans des prouveurs interactifs et des textes mathématiques en langue naturelle. Le point de départ pourra être les datasets minF2F, putnamBench et proofnet.
• Fine-tuning et évaluation d’un modèle LLM pour la traduction d’énoncés mathématiques entre Lean et Coq.
• Communiquer régulièrement sur les résultats expérimentaux obtenus avec les chercheurs et ingénieurs support impliqués dans ces collaborations.

• Langages de programmation : Python
• Expérience avec des modèles et librairies de deep learning.
• Compétence en entraînement, RL, orchestration
• Fonctionnement GPU
• Langue : Candidats maîtrisant l'anglais à un niveau B1 minimum avec une bonne compréhension du français (ou inversement).
• Travail en équipe en distanciel
• Une expérience avec un outil de preuve formelle (Coq, Lean, ) serait un atout mais n'est pas obligatoire.

• 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 (après 6 mois d'ancienneté) 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

Selon expériences