L’intégration de composants IA au sein de systèmes critiques nécessite une grande confiance dans leur sûreté ; cette confiance peut par exemple être assurée par l’usage de techniques de vérification formelle. Différents verrous sont identifiés pour permettre l’utilisation de ces dernières : tout d’abord, les programmes à base d’IA manipulent des données de grande taille (images, sons, textes), ce qui rend leur formalisation délicate. De plus, les programmes à base d’IA sont conçus suivant des algorithmes probabilistes qui donnent des structures de programmes qui dépassent la capacité actuelle des outils de vérification classiques.
La plateforme CAISAR a donc pour objectif de lever ces verrous suivant trois axes de travail :
À ce titre, la plateforme CAISAR fournit un langage de spécification développé par le CEA-List qui permet une grande flexibilité de modélisation.
Le site web CAISAR fournit un manuel utilisateur accompagné d’exemples et de tutoriels. Il présente notamment deux cas d’usages gérés par CAISAR : la preuve de propriétés fonctionnelles d’un système anticollision d’avions (ACAS-Xu), ainsi que la robustesse de classifieurs face à des perturbations visuelles de la base de données de chiffres manuscrits fournie par MNIST (Mixed National Institute of Standards and Technology).
CAISAR évolue et s’améliore constamment pour répondre à des besoins de plus en plus complexes et réels. Le prochain véritable défi consistera à spécifier et à vérifier des modèles d’intelligence artificielle hétérogènes, tels que ceux composés de réseaux neuronaux et de machine à vecteurs de support. Pour ce faire, il sera nécessaire de concevoir un mécanisme de collaboration entre les différents prouveurs intégrés dans CAISAR, ce qui est ambitieux en matière de vérification formelle d’IA.
Pour en savoir plus :
CAISAR est une plateforme open source qui combine différents outils de preuve et de test afin d’améliorer la confiance des IA via un langage de spécification formel et expressif.
