nn dependability kit

nn-dependabilidad-kit

NN-Dependability-Kit es una herramienta de investigación de código abierto para ayudar a la ingeniería de redes neuronales para dominios críticos de seguridad.

C.-H. Cheng, C.-H. Huang y G. Nührenberg. NN-Dependabilidad-Kit: Ingeniería de redes neuronales para sistemas de conducción autónoma crítica de seguridad . https://arxiv.org/abs/1811.06746

Licencia

GNU Affero General Public License (AGPL) Versión 3

Manual

Ver NN_Dependability_Kit_Manual.pdf

Prueba la herramienta

Los ejemplos se presentan como cuadernos Jupyter para permitir la comprensión paso a paso sobre los conceptos.

• [Generación de casos de métricos y pruebas] GTSRB_NEURON2ProyectionCoverage_Testgen.ipynb, o gtsrb_additionalMetrics.ipynb, o escenario_coverage_a9.ipynb, o kitti_scenario_coverage.ipynb, o mnist_neuron2procycoverage_testgengen.ipynb, or.ipynb, or.ipynb, Ssd_interpretationprecision.ipynb
• [Verificación formal] TargetVehicleProcessingNetwork_formalverification.ipynb
• [Verificación de tiempo de ejecución] gtsrb_runtimemonitoring.ipynb, o mnist_runtimemonitoring.ipynb

Estructura

Hay cuatro paquetes bajo NnDependability, a saber

• Básico: Lector para modelos, así como la representación intermedia de NN (para fines de verificación)
• Métricas: Calcule las métricas de confiabilidad para las redes neuronales
• ATG: Generación automática de casos de prueba para mejorar las métricas
• Formal: Verificación formal (análisis estático, resolución de restricciones) de redes neuronales
• RV: monitoreo de tiempo de ejecución de redes neuronales

Paquetes importantes de Python como requisitos

• Pytorch + numpy + matplotlib + jupyter

• [Generación de casos de prueba] Herramientas de investigación de optimización de Google

• [Verificación / análisis estático] Pulp (conector MILP basado en Python a CBC y otros solucionadores)

  • El solucionador CBC pre-enviado con pulpa puede bloquearse para resolver algunos problemas. El motor de análisis estático supone que se puede llamar al solucionador GLPK (configurar la variable de ruta), de modo que cada vez que CBC se bloquea, GLPK se activa automáticamente como un reemplazo. Desafortunadamente, esto no puede garantizar que ambos dos solucionadores no se bloqueen al mismo tiempo. Por lo tanto, para el uso industrial, recomendamos usar IBM CPlex como el solucionador MILP subyacente.
    • [GNU GLPK] http://www.gnu.org/software/glpk/
    • [GPLK en Windows] http://winglpk.sourceforge.net/

• [Verificación de tiempo de ejecución] DD (diagrama de decisiones binarias implementado con Python)

Use requisitos.txt para instalar dependencias para ejecutar la mayoría de los cuadernos (excluyendo TensorFlow).

Publicaciones relacionadas

• [Métricas y generación de casos de prueba] https://arxiv.org/abs/1806.02338
• [Verificación formal] https://arxiv.org/abs/1705.01040, https://arxiv.org/abs/1904.04706
• [Verificación de tiempo de ejecución] https://arxiv.org/abs/1809.06573
• [SSD-EXample] El ejemplo usa algunas imágenes del conjunto de datos VOC2012: The Pascal Visual Object Classes (VOC) Desafío Everingham, M., Van Gool, L., Williams, CKI, Winn, J. y Zisserman, A. International Journal of Computer Vision, 88 (2), 303-338, 2010, 2010, 2010, 2010, 2010

Otros temas

A. Métricas relacionadas con la precisión de la intrepreación y la sensibilidad a la oclusión

1. Paquete adicional para instalarse

• [Métricas] Saliente (https://github.com/pair-code/salience) Úselo de la siguiente manera:

 # init submodule for saliency
cd nndependability/metrics/saliency-source/
git submodule init
git submodule update
cd ..
ln -s saliency-source/saliency saliency
cd ../../

2. Preparación para el ejemplo de 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. Desafíos en la verificación formal debido a la falta de especificación de entrada y escalabilidad

Para hacer una verificación formal sobre redes neuronales, hay dos problemas comúnmente vistos.

• Es posible que la escalabilidad de la verificación formal no pueda manejar redes muy complejas y muy profundas.
• Se desconoce la "forma de la entrada". De hecho, uno normaliza comúnmente los datos, por lo que cada entrada comúnmente tiene un rango de [-1,1], pero es posible que deseemos tener una "sobrecargación" más estricta sobre los datos de entrenamiento.

En NN-Dependability-Kit, recomendamos a los usuarios que continúen con los siguientes pasos.

• Realice el análisis tomando una subred de capas cercanas a la salida como la red amarilla de la figura a continuación. Si por cada entrada a la red amarilla, se garantiza que no se producirá una mala producción, entonces para cada entrada a la red original muy profunda y compleja, no se producirá una salida mala.
  • El segundo y tercer parámetros en la función loadMlpFrompyTorch () en NnDependability/Basics/PytorchReader.py admite tal concepto

• Como las entradas en la red completa solo pueden conducir a ciertos valores para la entrada de la red amarilla, si la propiedad de seguridad no se puede probar en la red amarilla, nuestra recomendación adicional es alimentar a la red completa con datos de capacitación, para obtener una sobrecargación más estricta basada en las entradas visitadas para la red amarilla. Se puede encontrar un ejemplo en Neuron n^17_ {1}, donde al ejecutar la red con todos los datos de entrenamiento disponibles, sabemos que los datos de entrenamiento hacen que la salida de n^17_ {1} se acerne por [-0.1, 0.6]. Por lo tanto, podemos usar los límites registrados como restricciones de entrada para la red amarilla para realizar una verificación formal.

  • Además del uso de intervalos, también se puede registrar restricciones de octágono o incluso patrones de activación de neuronas para crear una excesiva apelimación más estricta de los datos visitados.

• La corrección de la verificación se basa en la suposición de que es imposible tener valores de neuronas sentados fuera del intervalo creado, lo cual es una prueba de garantía de asumir . La suposición se puede monitorear fácilmente en tiempo de ejecución.