IA générative pour les preuves formelles H/F

Description du Poste

Résumé du projet scientifique

Les assistants de preuve (Rocq/Coq, Lean) permettent de certifier des résultats mathématiques avec une rigueur absolue. Des jalons comme la preuve du théorème des quatre couleurs par Gonthier illustrent leur puissance. Leur limite historique réside dans l'effort humain considérable qu'exige la traduction d'une preuve mathématique en script formel, freinant ainsi le passage à l'échelle.
Les progrès récents de l'IA générative changent la donne : des modèles entraînés sur des corpus de preuves formelles peuvent désormais générer et explorer des preuves de manière largement autonome. Un atout décisif de ce paradigme est la vérifiabilité intrinsèque des preuves produites, leur validité est attestée mécaniquement, sans expertise externe, levant ainsi les doutes habituels sur la fiabilité des sorties d'IA.
Développer des modèles efficaces pour cette tâche requiert une expertise à l'intersection des assistants de preuve, des architectures de modèles de langage et des mathématiques.

Résumé du projet d'enseignement

Le projet d’enseignement sera discuté avec le site

Unités d'accueil potentiels

• INSMI - CNRS Mathématiques
• ICJ - Institut Camille Jordan
• LIP - Laboratoire de l'informatique du parallélisme
• UMPA - Unité de Mathématiques Pures et Appliquées

Votre Profil

Profil Recherché

Titulaire d’un doctorat ou diplôme équivalent ou justifiant de titres et travaux scientifiques jugés équivalents par l’instance compétente de l’établissement. Il n’y a aucune condition d’âge ou de nationalité pour candidater. Tous les emplois CNRS sont accessibles aux personnes en situation de handicap en bénéficiant d’aménagement d’épreuves rendus nécessaires par la nature du handicap

Votre Environnement de Travail

Stratégie du laboratoire d'accueil

Nous ciblons pour cette CPJ l’écosystème lyonnais qui s’intéresse tout particulièrement au sujet de la théorie des preuves tant en mathématiques qu’en informatique. Le LIP, plus particulièrement l’équipe PLUME, et l’ICJ sont au cœur de ces enjeux en matière de vérification formelle et pourront accueillir naturellement la CPJ.

Stratégie d'établissement

Les IA génératives de type LLM sont en train de modifier profondément la thématique des preuves formelles à l’interface entre les Mathématiques et les Sciences informatiques. Leurs capacités à générer une preuve au sens « théorie de la preuve » se consolident même si cela reste encore fragile. Les récents travaux menés en particulier par exemple en « Lean » montre que la dynamique est enclenchée et que c’est un sujet dont il faut se saisir de manière stratégique pour s’attaquer à des verrous scientifiques nouveaux et très interdisciplinaires dans ce domaine.
Un des axes du COMP CNRS concerne l’IA générative pour les sciences. Cette Chaire de Professeur Junior se place pleinement dans cette initiative. Elle permettra au CNRS de se positionner sur un domaine à fort potentiel et crucial concernant l’évolution de la recherche en mathématiques.

Stratégie Internationale

Le CNRS accueille et recrute largement des chercheuses et chercheurs à l’international. Plus de 30% des personnes recrutées viennent de l’étranger. Ce recrutement aura cette même ambition.

Rémunération et avantages

Rémunération

Rémunération brute annuelle de 54600 Euros à 57800 Euros selon l’expérience professionnelle

Financement total

200k€

Congés et RTT annuels

44 jours

Pratique et Indemnisation du TT

Pratique et indemnisation du TT

Transport

Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€

Politique de recherche

Science ouverte

Le CNRS développe une politique forte en faveur de la science ouverte. La science ouverte consiste à rendre « accessibles autant que possible et fermés autant que nécessaire » les résultats de la recherche. À ce titre, le CNRS vise à ce que 100 % des textes des publications issues des travaux de ses unités soient rendues accessibles à tous, notamment grâce au dépôt dans HAL. Les données produites doivent aussi être rendues disponibles et réutilisables, sauf restriction particulière. Par ailleurs, les principes directeurs de l’évaluation individuelle sont revus en conformité avec la déclaration DORA, plus qualitatifs et tenant compte de toutes les facettes du métier de chercheur.

Science et société

La relation science-société est désormais reconnue comme une dimension à part entière de l'activité scientifique. Le projet développera cette dimension en synergie avec tous les partenaires. Les travaux de recherche qui en seront issus contribueront à éclairer la décision publique. Des initiatives de sciences participatives pourront être initiées avec des acteurs de l’écosystème socio-économique et culturel du projet.

Diffusion scientifique

La diffusion des résultats passera par des avancées scientifiques de niveau mondial, qui peuvent se caractériser par des productions de tout type : publications, logiciels, brevets, livres… Par ailleurs, le projet mettra en œuvre une communication vers des cibles diverses telles que communautés scientifiques, médias, décideurs, grand public, scolaires, etc., avec un calendrier adapté. Des outils spécifiques pourront être développés comme des sites web, des newsletters ou encore des rencontres, colloques internationaux, écoles d’été et conférences.

À propos de l’offre

À propos du CNRS

Le CNRS est un acteur majeur de la recherche fondamentale à une échelle mondiale. Le CNRS est le seul organisme français actif dans tous les domaines scientifiques. Sa position unique de multi-spécialiste lui permet d’associer les différentes disciplines pour affronter les défis les plus importants du monde contemporain, en lien avec les acteurs du changement.

Le CNRS

Les métiers de la recherche