Modèles d'apprentissage automatique porteurs de preuves – ProML

L'apprentissage automatique a révolutionné des domaines tels que la vision par ordinateur et le traitement du langage naturel. Cependant, le déploiement de modèles d'apprentissage automatique dans des secteurs critiques pour la sécurité exige des garanties en termes de fiabilité, de robustesse et d'interprétabilité. ProML propose un nouveau paradigme pour spécifier et certifier ces modèles. Notre objectif est de développer une méthode de vérification formelle avant déploiement, accompagnée de certificats ou preuves vérifiables par machine, expliquant et justifiant les prédictions, pour permettre une validation indépendante.

Pour relever le défi des spécifications formelles des modèles d'apprentissage, notamment les réseaux de neurones, nous adopterons une approche d'apprentissage des spécifications. Plutôt que de construire manuellement des spécifications dans l’espace d’entrée brute, nous générerons automatiquement des spécifications formelles sur des représentations apprises, qui possèdent des propriétés disjonctives et compositionnelles utiles.

Cela permettra de concevoir des moteurs de vérification et d’explication optimisés, permettant une vérification systématique ou des explications de prédiction sur une région plus large de l’espace d’entrée. Nous pensons que cette approche permet de repondre aux défis de passage à l'échelle des méthodes actuelles de vérification et d'explications. À la fin du projet, nous visons de grands modèles avec des données d'entrée séquentielles, qui sont actuellement hors de portée de l’état de l’art.

Enfin, en nous inspirant des recherches fondamentales sur le code porteur de preuve, nous permettrons des prédictions et explications certifiées, vérifiables par machine, en temps réel lors de l'inférence des modèles. Ce projet améliorera les normes de sécurité et d'explicabilité en apprentissage automatique, renforçant ainsi la transparence et la responsabilité dans divers domaines d'application.