nn dependability kit

NN依赖性量

NN依赖性kit是一种开源研究工具，可帮助工程神经网络，以实现安全至关重要的领域。

C.-H。 Cheng，C.-H。黄和G.Nührenberg。 NN依赖性KIT：用于安全至关重要自主驾驶系统的工程神经网络。 https://arxiv.org/abs/1811.06746

执照

GNU AFFERO通用公共许可证（AGPL）版本3

手动的

请参阅nn_depentability_kit_manual.pdf

尝试工具

示例作为jupyter笔记本，以允许对概念的分步理解。

• [指标和测试案例生成] gtsrb_neuron2proctiveCoverage_testgen.ipynb或gtsrb_additionalmetrics.ipynb，或sceasario_coverage_a9.ipyynb，或kitti_scenario_coveraio_coverage.ipynb，or Mnipoddott ssd_interpretationprecision.ipynb
• [正式验证] targetVehicleProcessingnetwork_formalverification.ipynb
• [运行时验证] gtsrb_runtimemonitoring.ipynb或mnist_runtimemonitoring.ipynb

结构

有四个包裹在NNDETABINABY下，即

• 基本：模型的读者以及NN的中间表示（出于验证目的）
• 指标：对神经网络的可靠性指标
• ATG：自动测试案例生成以改善指标
• 正式：神经网络的正式验证（静态分析，约束解决）
• RV：神经网络的运行时监视

重要的python套件作为要求

• pytorch + numpy + matplotlib + jupyter

• [测试案例生成] Google优化研究工具

• [验证 /静态分析]纸浆（基于Python的MILP连接器到CBC和其他求解器）

  • 用纸浆预先运送的CBC求解器可能会在解决一些问题时崩溃。静态分析引擎假设可以调用GLPK求解器（请设置路径变量），以便每当CBC崩溃时，GLPK会自动触发作为替换。不幸的是，这不能保证两个求解器不会同时崩溃。因此，对于工业用法，我们强烈建议将IBM CPLEX用作基础的MILP求解器。
    • [gnu glpk] http://www.gnu.org/software/glpk/
    • [Windows上的GPLK] http://winglpk.sourceforge.net/

• [运行时验证] DD（使用Python实施的二进制决策图）

使用要求.txt安装依赖项来运行大多数笔记本电脑（不包括张量）。

相关出版物

• [指标与测试案例生成] 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示例]该示例使用了VOC2012数据集中的几张图片：Pascal Visual Object类（VOC）挑战Everingham，M.，Van Gool，L.

其他主题

A.与肠内精度和遮挡灵敏度有关的指标

1。要安装的其他软件包

• [指标]显着性（https://github.com/pair-code/sality）使用以下方式使用它：

 # 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依赖性套件中，我们建议用户继续进行以下步骤。

• 通过采用近传输图层的子网进行分析，例如下图的黄色网络。如果对于黄色网络的每个输入，可以保证不会产生不良输出，那么对于原始非常深且复杂的网络的每个输入，都不会产生不良的输出。
  • function LoadMlpFrompyTorch（）中的第二个和第三个参数在nndeptipity/basics/pytorchreader中。Py支持这样的概念

• 由于完整网络的输入只能导致黄色网络输入的某些值，如果无法在黄色网络上证明安全属性，我们的进一步建议是用培训数据为完整的网络提供供应完整的网络，以便基于访问量的输入来得出更严格的过度透视。可以在Neuron n^17_ {1}中找到一个示例，其中通过所有可用的培训数据运行网络，我们知道训练数据使得n^17_ {1}的输出由[-0.1，0.6]绑定。因此，我们可以将记录的绑定用作黄色网络的输入约束来执行正式验证。

  • 除了使用间隔外，还可以记录八角形约束甚至神经元激活模式，以创造访问的数据的更严格的过度应用。

• 验证的正确性是基于一个假设，即无法将神经元值放在创建的间隔之外，这是假定保证的证明。可以在运行时轻松监视该假设。