Contexte et atouts du poste
Dans le cadre des projets ERC Fresco et AI4Maths soutenu par Renaissance Philanthropy, l'objectif est de développer des techniques de traduction automatique et certifiée entre les assistants à la preuve Lean et Rocq, afin de rendre totalement transparent le fait qu'une bibliothèque mathématique ou logicielle ait été formalisée dans l'un ou l'autre système.
Ce travail s'inscrit dans un contexte de collaboration étroite avec le SIC d'Inria Rennes ainsi qu'avec les équipes Argo, Gallinette et PiCube. Il impliquera des interactions régulières avec ces partenaires et nécessitera des séjours fréquents sur les différents sites afin de favoriser les échanges scientifiques et le développement conjoint des outils et des fondements théoriques associés.
Mission confiée
### Missions
La personne recrutée contribuera au développement de nouvelles méthodes de traduction automatique entre les assistants à la preuve Lean et Rocq, en s'appuyant sur les capacités des modèles de langage de dernière génération (*Frontier LLMs*).
Dans un premier temps, elle participera à la conception et à l'évaluation de chaînes de traduction exploitant les modèles les plus performants du marché afin d'identifier les architectures et stratégies les plus adaptées à la formalisation mathématique et à la traduction certifiée de preuves.
Dans un second temps, elle contribuera au développement, à l'adaptation et à l'entraînement de modèles open source spécialisés, avec pour objectif d'atteindre des performances comparables à celles des modèles propriétaires tout en permettant un déploiement local, une meilleure maîtrise des coûts d'infrastructure, de la confidentialité des données et de l'empreinte environnementale.
Les travaux incluront également la constitution de jeux de données, l'évaluation des modèles sur des corpus de preuves formelles, l'intégration des outils développés dans les environnements Lean et Rocq, ainsi que l'étude de mécanismes de vérification permettant de garantir la correction des traductions produites.
Collaboration
La personne recrutée évoluera dans un environnement fortement collaboratif, à l'interface entre intelligence artificielle, méthodes formelles et assistants à la preuve.
Elle travaillera en étroite interaction avec le SIC d'Inria Rennes ainsi qu'avec les équipes Argo, Gallinette et PiCube. Ces collaborations donneront lieu à des échanges scientifiques réguliers, à la participation à des réunions de projet, ainsi qu'à des séjours fréquents sur les différents sites partenaires afin de favoriser le transfert de compétences et le développement conjoint des outils de traduction et de vérification.
Principales activités
Principales activités
Analyser les besoins scientifiques des projets ERC Fresco et AI4Maths en matière de traduction automatique et certifiée entre les assistants à la preuve Lean et Rocq.
Développer des programmes, applications et chaînes de traitement basés sur des modèles de langage de dernière génération (Frontier LLMs) pour la traduction de preuves formelles et de bibliothèques mathématiques.
Concevoir, adapter et évaluer des modèles open source spécialisés afin d'obtenir des performances comparables aux modèles propriétaires tout en permettant un déploiement local et une maîtrise de l'empreinte environnementale.
Constituer des jeux de données, tester, évaluer et améliorer les systèmes développés jusqu'à validation sur des corpus représentatifs de preuves formelles.
Rédiger la documentation technique, les rapports d'avancement et les publications associées aux travaux réalisés.
Activités complémentaires
Présenter l'avancement des travaux aux partenaires scientifiques des projets et participer aux réunions de coordination avec le SIC d'Inria Rennes et les équipes Argo, Gallinette et PiCube.
Diffuser les outils et modèles développés auprès des communautés Lean, Rocq et intelligence artificielle via des dépôts open source et des démonstrateurs.
Assurer une veille scientifique et technologique sur les modèles de langage, l'IA pour les mathématiques et les assistants à la preuve, et contribuer à l'animation de la communauté autour de ces thématiques.
Compétences
Compétences techniques et niveau requis
Bonne maîtrise de la programmation (Python, OCaml, Rust ou langage équivalent).
Connaissances en intelligence artificielle, en particulier sur les modèles de langage (LLM), l'apprentissage automatique ou le traitement automatique des langues.
Capacité à conduire des expérimentations, analyser des résultats et évaluer des systèmes d'IA.
Maîtrise des outils de développement collaboratif (Git, intégration continue, gestion de projets logiciels).
Niveau Master ou équivalent en informatique, intelligence artificielle, mathématiques appliquées ou domaine connexe.
Langues
Anglais scientifique : niveau B2 minimum, C1 souhaité (lecture d'articles, rédaction technique et échanges scientifiques).
Français : capacité à évoluer dans un environnement de travail francophone.
Compétences relationnelles
Capacité à travailler en équipe dans un contexte de recherche collaborative.
Curiosité scientifique et goût pour l'apprentissage continu.
Autonomie dans la conduite de projets et la résolution de problèmes.
Qualités de communication écrite et orale.
Capacité à interagir avec des interlocuteurs issus de disciplines variées (IA, méthodes formelles, mathématiques, génie logiciel).
Compétences additionnelles appréciées
Connaissances des assistants à la preuve (Lean, Rocq/Coq, Isabelle, HOL, etc.).
Expérience avec les modèles open source et leur adaptation (fine-tuning, RAG, évaluation).
Connaissances en vérification formelle, théorie des types ou mathématiques formelles.
Expérience de contribution à des projets open source ou de recherche.
Publications, stage de recherche ou participation à des projets en intelligence artificielle ou en méthodes formelles.
Avantages
Rémunération
Selon expérience
En cliquant sur "JE DÉPOSE MON CV", vous acceptez nos CGU et déclarez avoir pris connaissance de la politique de protection des données du site jobijoba.com.