Raisonnements formellement certifiés en apprentissage automatique – ForML

Les progrès actuels de l'apprentissage machine (ML) laissent présager un panel toujours plus large d'utilisations des modèles ML. Toutefois, dans les domaines jugés à haut risque, mais aussi dans les domaines critiques pour la sécurité, le déploiement de modèles ML devrait être étayé par des outils de raisonnement rigoureux, capables d'identifier les limites éventuelles de ces modèles. Concrètement, il s'agit de savoir si le modèle ML est suffisamment robuste, ne présente pas de biais, mais aussi si ses actions peuvent être comprises par un utilisateur humain ou validées automatiquement.
Le projet ForML propose de réaliser des avancées fondamentales dans l'état de l'art des approches formelles pour le raisonnement sur les modèles ML. Le projet ForML propose d'exploiter des outils bien connus de l'analyse logicielle, notamment l'interprétation abstraite et le raffinement de l'abstraction guidé par des contre-exemples, afin de fournir une nouvelle génération d'outils efficaces et rigoureux pour raisonner sur les modèles ML. Le projet ForML sera également pionnier dans la certification de ces outils en exploitant des assistants de preuve.