Notre société repose sur des systèmes logiciels critiques (par exemple pour la sûreté ferroviaire ou nucléaire) dont le dysfonctionnement peut entraîner des conséquences graves pour les personnes, l’environnement et les infrastructures. Un très haut niveau de confiance dans leur bon fonctionnement est donc exigé avant leur déploiement. Parmi les domaines qui composent la recherche informatique, la science des langages de programmation s’attache à inventer de nouvelles façons de concevoir et écrire des logiciels plus sûrs.
Toutefois, l’intégration de réseaux de neurones dans les systèmes critiques rebat les cartes. Leurs modalités de conception les rendent difficiles à décrire formellement et donc à vérifier. En particulier, Python, le langage de programmation le plus utilisé pour la conception des réseaux de neurones, est très difficile à analyser. De plus, les réseaux de neurones ne sont constitués que de successions de très gros calculs algébriques, sans lien apparent avec le résultat qu’ils fournissent.
Par conséquent, les caractéristiques des réseaux de neurones sont très éloignées de celles des logiciels classiques auxquels est habituée la communauté de la vérification de programmes.
Nous avons d’abord décrit les conséquences de la vérification des réseaux de neurones sur les outils de vérification de programmes. Les points à retenir sont les suivants :
Nous avons enfin proposé des langages de description adaptés à cette approche.
La spécification des réseaux de neurones constitue un important sujet de recherche, auquel nous devons répondre à un niveau fondamental : celui du langage de programmation.
