nn-зависимость-Kit
NN-зависимость-KIT-это инструмент исследования с открытым исходным кодом, помогающий инженерным нейронным сетям для критических доменов безопасности.
C.-H. Ченг, C.-H. Хуан и Г. Нюренберг. NN-зависимость-KIT: инженерные нейронные сети для критически важных систем автономного вождения . https://arxiv.org/abs/1811.06746
Лицензия
GNU Affero Общая публичная лицензия (AGPL) Версия 3
Руководство
См. Nn_dependability_kit_manual.pdf
Попробуйте инструмент
Примеры представлены в виде ноутбуков Юпитера, позволяющих пошаговать понимание концепций.
- [Metrics & Test Case Generation] GTSRB_NEURON2PROCHERCOVERAGE_TESTGEN.IPYNB, или GTSRB_ADDITIONALMETRICS.IPYNB, или сценарий_COVERAGE_A9.IPYNB, или KITTI_SCENARIO_COVERAGE.IPYNB, или MNIST_NEURON2PROGECECOVERGEGERIPGEN. SSD_INTERPTRATIONPRECIONS.IPYNB
- [Формальная проверка] TargetVehicleProcessingNetwork_formalverification.ipynb
- [Проверка времени выполнения] gtsrb_runtimemonitoring.ipynb, или mnist_runtimemonitoring.ipynb
Структура
Есть четыре пакета в рамках независимости, а именно
- Базовый: читатель для моделей, а также промежуточное представление NN (для целей проверки)
- Метрики: расчет показателей надежности для нейронных сетей
- ATG: Автоматическое генерация тестовых случаев для улучшения метрик
- Формальная: формальная проверка (статический анализ, решение ограничений) нейронных сетей
- RV: мониторинг времени выполнения нейронных сетей
Важные пакеты Python в качестве требований
Pytorch + numpy + matplotlib + jupyter
[Инструменты тестового случая Google Optimization
[Проверка / Статический анализ] мякоть (разъем MILP на основе Python к CBC и другим решателям)
- CBC Solver Pre-Spected с пульпой может рухнуть при решении некоторых проблем. Двигатель статического анализа предполагает, что решатель GLPK может быть вызван (пожалуйста, настройте переменную пути), так что всякий раз, когда CBC вылетает, GLPK автоматически запускается в качестве замены. К сожалению, это не может гарантировать, что оба двух решателя не будут сбой одновременно. Поэтому для промышленного использования мы настоятельно рекомендуем использовать IBM CPLEX в качестве основного решателя MILP.
- [GNU GLPK] http://www.gnu.org/software/glpk/
- [GPLK в Windows] http://winglpk.sourceforge.net/
[Проверка времени выполнения] DD (бинарная диаграмма принятия решений, реализованная с использованием Python)
Используйте требования.
Связанные публикации
- [Метрики и генерация тестовых случаев] https://arxiv.org/abs/1806.02338
- [Формальная проверка] https://arxiv.org/abs/1705.01040, https://arxiv.org/abs/1904.04706
- [Проверка времени выполнения] https://arxiv.org/abs/1809.06573
- [SSD-Example] В примере используется несколько картинок из набора данных VOC2012: The Pascal Visual Abject Class Classe (VOC).
Другие темы
A. Метрики, связанные с точностью интропецировки и чувствительностью к окклюзии
1. Дополнительный пакет, который будет установлен
- [Метрики] значимость (https://github.com/pair-code/saliecty) Используйте ее следующим образом:
# init submodule for saliency
cd nndependability/metrics/saliency-source/
git submodule init
git submodule update
cd ..
ln -s saliency-source/saliency saliency
cd ../../
2. Подготовка к примеру 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. Проблемы в формальной проверке из -за отсутствия спецификации ввода и масштабируемости
Чтобы сделать официальную проверку в нейронных сетях, существуют две общепринятые проблемы.
- Масштабируемость формальной проверки может не иметь возможности обрабатывать очень сложные и очень глубокие сети
- «Форма ввода» неизвестна. Действительно, один обычно нормализует данные, поэтому каждый вход обычно имеет диапазон [-1,1], но мы можем пожелать иметь более жесткую «чрезмерную оценку» по сравнению с данными обучения.
В NN-зависимости-KIT мы советуем пользователям выполнять следующие шаги.
- Выполните анализ, взяв подсети слоев, близких к выходу, таких как желтая сеть на приведенной ниже рисунке. Если для каждого входа в желтую сеть, он гарантирует, что плохой выход не будет произведен, то для каждого входа в исходную очень глубокую и сложную сеть не будет произведено плохой выход.
- 2 -й и 3 -й параметры в функциональной загрузке mlpfrompytorch () в nnddependability/basics/pytorchreader.py Поддерживают такую концепцию
Поскольку входные данные в полную сеть могут привести к определенным значениям для ввода желтой сети, если свойство безопасности не может быть доказано в желтой сети, наша дальнейшая рекомендация заключается в том, чтобы подавать полную сеть с помощью учебных данных, чтобы получить более жесткую чрезмерную оценку на основе посещаемых входов для желтой сети. Пример можно найти в нейроне n^17_ {1}, где, запустив сеть со всеми доступными учебными данными, мы знаем, что учебные данные делают вывод N^17_ {1}, ограниченный [-0,1, 0,6]. Таким образом, мы можем использовать записанную границу в качестве входных ограничений для желтой сети для выполнения формальной проверки.
- Помимо использования интервалов, можно также записать ограничения восьмиугольника или даже паттерны активации нейронов, чтобы создать более плотную чрезмерную применение посещаемых данных.
Правильность проверки основана на предположении, что невозможно иметь значения нейронов, сидящих за пределами созданного интервала, что является доказательством гарантии предположения . Предположение можно легко контролировать во время выполнения.
