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]綁定。因此，我們可以將記錄的綁定用作黃色網絡的輸入約束來執行正式驗證。

  • 除了使用間隔外，還可以記錄八角形約束甚至神經元激活模式，以創造訪問的數據的更嚴格的過度應用。

• 驗證的正確性是基於一個假設，即無法將神經元值放在創建的間隔之外，這是假定保證的證明。可以在運行時輕鬆監視該假設。