nn dependability kit

nn依存性キット

NN依存性 - キットは、安全性クリティカルなドメインのエンジニアリングニューラルネットワークを支援するためのオープンソースの研究ツールです。

C.-H。チェン、C.-H。 Huang、およびG.Nührenberg。 NN依存性 - キット：安全性が批判的な自律駆動システムのためのエンジニアリングニューラルネットワーク。 https://arxiv.org/abs/1811.06746

ライセンス

GNU Affero General Public License（AGPL）バージョン3

マニュアル

nn_dependability_kit_manual.pdfを参照してください

ツールを試してみてください

例は、概念に対する段階的な理解を可能にするJupyterノートブックとして提示されています。

• [メトリックとテストケース生成] gtsrb_neuron2projectioncoverage_testgen.ipynb、またはgtsrb_additionalmetrics.ipynb、またはsinario_coverage_a9.ipynb、またはkitti_scenario_coverage.ipynb ssd_interpretationprecision.ipynb
• [正式な検証] TargetVehicleProcessingNetwork_formalverification.ipynb
• [ランタイム検証] gtsrb_runtimemonitoring.ipynb、またはmnist_runtimemonitoring.ipynb

構造

つまり、nndependabilityの下に4つのパッケージがあります

• 基本：モデルの読者とNNの中間表現（検証目的で）
• メトリック：ニューラルネットワークの信頼性メトリックを計算します
• ATG：メトリックを改善するための自動テストケース生成
• 正式：ニューラルネットワークの正式な検証（静的分析、制約解決）
• RV：ニューラルネットワークのランタイム監視

要件として重要なPythonパッケージ

• pytorch + numpy + matplotlib + jupyter

• [テストケース生成] Google Optimization Research Tools

• [検証 /静的分析]パルプ（CBCおよびその他のソルバーへのPythonベースのMILPコネクタ）

  • パルプと事前に発送されたCBCソルバーは、いくつかの問題を解決するためにクラッシュする可能性があります。静的分析エンジンは、GLPKソルバーを呼び出すことができると想定しており（パス変数を設定してください）、CBCがクラッシュするたびに、GLPKが自動的に交換としてトリガーされるようにします。残念ながら、これは両方の2つのソルバーが同時にクラッシュしないことを保証することはできません。したがって、産業用の使用については、基礎となるMILPソルバーとしてIBM Cplexを使用することを強くお勧めします。
    • [GNU GLPK] http://www.gnu.org/software/glpk/
    • [WindowsのGPLK] http://winglpk.sourceforge.net/

• [実行時間検証] DD（Pythonを使用して実装されたバイナリ決定図）

要件を使用して、ほとんどのノートブックを実行するために依存関係をインストールします（Tensorflowを除く）。

関連する出版物

• [メトリックとテストケース生成] 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データセットのいくつかの写真を使用しています：Pascal Visual Object Classes（VOC）Challenge Everingham、M.、Van Gool、L.、Williams、CKI、Winn、J。

その他のトピック

A.脳卒中の精度と閉塞感度に関連するメトリック

1。インストールする追加パッケージ

• [メトリック]顕著性（https://github.com/pair-code/saliency）次の方法で使用します。

 # 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.入力仕様の欠如とスケーラビリティによる正式な検証の課題

ニューラルネットワークをめぐる正式な検証を行うには、一般的に見られる2つの問題があります。

• 正式な検証のスケーラビリティは、非常に複雑で非常に深いネットワークを処理できない場合があります
• 「入力の形状」は不明です。実際、一般的にデータを正規化しているため、すべての入力が一般的に[-1,1]の範囲を持つことがありますが、トレーニングデータにより厳しい「過度に近接」したい場合があります。

NN依存性キットでは、ユーザーに次の手順を進めることをお勧めします。

• 以下の図の黄色のネットワークのような出力層の近くのサブネットワークを取得して分析を実行します。黄色のネットワークへの入力ごとに、不良出力が生成されないことを保証する場合、元の非常に深い複雑なネットワークへの入力ごとに、悪い出力は生成されません。
  • nndependability/basics/pytorchreader.pyの関数loadmlpfrompytorch（）の2番目と3番目のパラメーターは、そのような概念をサポートします

• 完全なネットワークへの入力は、黄色のネットワークの入力の特定の値にのみつながる可能性があるため、黄色のネットワークで安全プロパティを証明できない場合、イエローネットワークの訪問入力に基づいてより緊密な過剰近接を導き出すために、完全なネットワークをトレーニングデータに供給することがさらに推奨されます。例は、Neuron N^17_ {1}に記載されています。ここで、利用可能なすべてのトレーニングデータを使用してネットワークを実行することにより、トレーニングデータが[-0.1、0.6]で制限されているn^17_ {1}の出力を作成することがわかります。したがって、黄色ネットワークの入力制約として記録されたバウンドを使用して、正式な検証を実行できます。

  • 間隔を使用することとは別に、オクタゴンの制約を記録したり、ニューロンの活性化パターンを記録して、訪問されたデータのより緊密な過剰補償を作成することもできます。

• 検証の正しさは、作成された間隔の外側にニューロンの値を置くことは不可能であるという仮定に基づいています。これは想定保証証明です。仮定はランタイムで簡単に監視できます。