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

Le centre Inria de l'Université de Rennes est l'un des huit 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.

Dans le cadre du projet européen (ERC) FRESCO, ce stage a pour objectif d’explorer la traduction automatique d’énoncés de preuves entre deux de ces systèmes (de Lean vers Coq) à 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 du stage 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.

Atouts du poste:

• stage-projet rémunéré au SMIC
• possiblité d’embauche sur CDD (2 ans) au terme du stage

Bien que des datasets existent en Lean et en Coq, il n’existe pas de corpus parallèle pour la traduction entre ces deux systèmes. Le stagiaire aura pour missions :

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

Le stagiaire sera encadré par une chercheuse spécialiste des prouveurs interactifs (Coq, Lean) ainsi que par un ingénieur en machine learning.

• 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.
• Fine-tuning et évaluation d’un modèle LLM pour la traduction d’énoncés mathématiques entre Lean et Coq.

• Langages de programmation : Python
• Expérience avec des modèles et librairies de deep learning.
• une expérience avec un outil de preuve formelle (Coq, Lean, ) serait un atout mais n’est pas obligatoire
• Langue : Candidats maîtrisant l’anglais à un niveau B1 minimum avec une bonne compréhension du français (ou inversement).

• Restauration subventionnée
• Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria