L’objectif de ce stage est d’utiliser l’IA pour aider les ingénieurs à prouver mathématiquement que des
logiciels critiques (aéronautique, ferroviaire, automobile…) respectent les principes de sécurité et sont
exempts de bugs critiques.
L’IA permettra de diminuer le temps de travail des ingénieurs car la vérification formelle est très
puissante mais complexe et chronophage.
La construction de preuves (en particulier via des lemmes, des tactiques et des règles de vérification)
reste une tâche complexe et chronophage, nécessitant souvent une expertise significative en matière
de prouveurs de théorèmes et de cadres de modélisation.
Les récentes avancées en Intelligence Artificielle (IA), notamment les grands modèles de langage (LLM)
et les systèmes de raisonnement multi-agents, ont ouvert de nouvelles opportunités pour automatiser
et assister les processus de vérification formelle.
Les techniques pilotées par l’IA peuvent générer automatiquement des scripts de preuve, suggérer des
lemmes auxiliaires, optimiser les stratégies de vérification et identifier des invariants réutilisables,
réduisant ainsi l’effort manuel et améliorant la productivité.
Apprentissage de l’IA :
- Les prouveurs de théorèmes modernes (Rocq (Ex-Coq), Isabelle, etc.) fournissent une vaste
littérature de preuves formelles. Ces exemples pourraient servir de jeux de données
d’entraînement pour des IA capables d’apprendre à prédire les étapes de preuve, les tactiques
et les lemmes.
- L’apprentissage par renforcement peut être réalisé avec une correction de preuve évaluée par
le prouveur de théorèmes lui-même.
IA appliquée à des outils particuliers :
- Atelier B & HLL : Ces environnements nécessitent que les utilisateurs construisent des
obligations de preuve pour assurer la correction des spécifications système. Des modèles d’IA
entraînés sur des preuves issues de la littérature peuvent suggérer des scripts de preuve, des
règles utilisateur et des lemmes auxiliaires.
- Simulink, HLL ou Frama-C : Des modèles d’IA peuvent assister dans l’inférence d’invariants.
– Vous avez des connaissances en méthode formelle (Expérience pratique avec Coq/Rocq ou
Isabelle) et des compétences en développement informatique (Python, OCaml, …) ;
– Vous avez des connaissances en intelligence artificielle ou en apprentissage automatique ;
– Vous aimez travailler en équipe et faites preuve de curiosité, d’autonomie et d’un bon sens
de l’organisation.
Apprentissage : 1 à 3 ans
Stage : 6 mois
