NN-Dépendabilité-kit
NN-Dépendabilité-Kit est un outil de recherche open source pour aider les réseaux de neurones d'ingénierie pour les domaines critiques de sécurité.
C.-H. Cheng, C.-H. Huang et G. Nührenberg. NN-Dépendabilité-kit: réseaux de neurones en ingénierie pour les systèmes de conduite autonomes critiques . https://arxiv.org/abs/1811.06746
Licence
GNU Affero General Public License (AGPL) Version 3
Manuel
Voir nn_dependabilité_kit_manual.pdf
Essayez l'outil
Les exemples sont présentés comme des cahiers Jupyter pour permettre une compréhension étape par étape sur les concepts.
- [Metrics & Test Case Generation] GTSRB_NEURON2PROIFFICATIONSCOVEAGE_TESTGEN.IPynb, ou gtsrb_additionalmetrics.ipynb, ou scénario_cocounage_a9.ipynb, ou kitti_scenario_coverage.ipynt Ssd_interpretationprecision.ipynb
- [Vérification formelle] TargetVehicleProcessingNetwork_formalVerification.ipynb
- [Vérification d'exécution] gtsrb_runtimemonitoring.ipynb, ou mnist_runtimemonitoring.ipynb
Structure
Il y a quatre packages sous nndeprendabilité, à savoir
- Basique: lecteur pour les modèles ainsi que la représentation intermédiaire de NN (à des fins de vérification)
- Métriques: calculer les mesures de fiabilité pour les réseaux de neurones
- ATG: génération automatique de cas de test pour améliorer les mesures
- formel: vérification formelle (analyse statique, résolution de contraintes) des réseaux de neurones
- VR: surveillance de l'exécution des réseaux de neurones
Packages Python importants comme exigences
Pytorch + Numpy + Matplotlib + Jupyter
[Génération de cas de test] Outils de recherche Google Optimization
[Vérification / analyse statique] Pulp (connecteur MILP basé sur Python à CBC et à d'autres solveurs)
- Le solveur CBC pré-expédié avec pulpe peut s'écraser pour résoudre certains problèmes. Le moteur d'analyse statique suppose que le solveur GLPK peut être appelé (veuillez configurer la variable de chemin), de sorte que chaque fois que CBC se bloque, GLPK est automatiquement déclenché en remplacement. Malheureusement, cela ne peut garantir que les deux deux solveurs ne s'écraseront pas en même temps. Par conséquent, pour l'utilisation industrielle, nous conseillons fortement d'utiliser IBM CPLEX comme solveur MILP sous-jacent.
- [GNU GLPK] http://www.gnu.org/software/glpk/
- [Gplk sur Windows] http://winglpk.sourceforge.net/
[Vérification d'exécution] DD (diagramme de décision binaire implémenté à l'aide de Python)
Utilisez les exigences.txt pour installer des dépendances pour exécuter la plupart des ordinateurs portables (à l'exclusion de TensorFlow).
Publications connexes
- [Génération de cas de métriques et de tests] https://arxiv.org/abs/1806.02338
- [Vérification formelle] https://arxiv.org/abs/1705.01040, https://arxiv.org/abs/1904.04706
- [Vérification d'exécution] https://arxiv.org/abs/1809.06573
- [SSD-Exemple] L'exemple utilise quelques images de l'ensemble de données VOC2012: The Pascal Visual Objectes Classes (VOC) Challenge Everingham, M., Van Gool, L., Williams, CKI, Winn, J. et Zisserman, A. International Journal of Computer Vision, 88 (2), 303-338, 2010, 2010
Autres sujets
A. Métriques liées à la précision d'intréprétation et à la sensibilité à l'occlusion
1. Package supplémentaire à installer
- [Metrics] Sailenmey (https://github.com/pair-code/saliency) Utilisez-le de la manière suivante:
# init submodule for saliency
cd nndependability/metrics/saliency-source/
git submodule init
git submodule update
cd ..
ln -s saliency-source/saliency saliency
cd ../../
2. Préparation de l'exemple SSD
cd models/SSD-Tensorflow/
git submodule init
git submodule update
# prepare weights
cd checkpoints/
unzip ssd_300_vgg.ckpt.zip
cd ../
# install custom changes to module SSD-Tensorflow that allows using saliency
git apply ../ssd_tensorflow_diff.diff
cd ../../
B. Défis de vérification formelle en raison du manque de spécification et d'évolutivité des entrées
Pour faire une vérification formelle sur les réseaux de neurones, il y a deux problèmes couramment observés.
- L'évolutivité de la vérification formelle peut ne pas être en mesure de gérer des réseaux très complexes et très profonds
- La "forme de l'entrée" est inconnue. En effet, on normalise généralement les données, donc chaque entrée a généralement une gamme de [-1,1], mais nous voulons peut-être avoir une "sur-approximation" plus serrée sur les données de formation.
Dans NN-Dépendabilité-kit, nous conseillons aux utilisateurs de procéder aux étapes suivantes.
- Effectuez l'analyse en prenant un sous-réseau de couches à proximité comme le réseau jaune de la figure ci-dessous. Si pour chaque entrée du réseau jaune, on garantit que la mauvaise sortie ne sera pas produite, alors pour chaque entrée du réseau très profond et complexe d'origine, aucune mauvaise sortie ne sera produite.
- Les 2e et 3e paramètres en fonction chargentmlpfropytorch () dans nndeprendabilité / basics / pytorchreader.py prennent en charge un tel concept
Comme les entrées du réseau complet ne peuvent entraîner que certaines valeurs pour l'entrée du réseau jaune, si la propriété de sécurité ne peut pas être prouvée sur le réseau jaune, notre autre recommandation consiste à nourrir le réseau complet avec des données de formation, afin de dériver une excession excessive plus serrée basée sur les entrées visitées pour le réseau jaune. Un exemple peut être trouvé dans le neurone n ^ 17_ {1}, où en exécutant le réseau avec toutes les données de formation disponibles, nous savons que les données de formation font la sortie de N ^ 17_ {1} délimitée par [-0.1, 0.6]. Nous pouvons donc utiliser la limite enregistrée comme contraintes d'entrée pour le réseau jaune pour effectuer une vérification formelle.
- En plus d'utiliser des intervalles, on peut également enregistrer des contraintes d'octogone ou même des modèles d'activation des neurones pour créer une exagération excessive plus serrée des données visitées.
La correction de la vérification est basée sur l'hypothèse qu'il est impossible d'avoir des valeurs de neurones assises en dehors de l'intervalle créé, qui est une preuve de présume-garantie . L'hypothèse peut être facilement surveillée lors de l'exécution.
