nn dependability kit

nn-dependability-kit

NN-Dependability-KIT adalah alat penelitian open source untuk membantu rekayasa jaringan saraf untuk domain kritis keselamatan.

C.-H. Cheng, C.-H. Huang, dan G. Nührenberg. NN-Dependability-KIT: Rekayasa Jaringan Saraf untuk Sistem Mengemudi Otonomi Kritis Kritis . https://arxiv.org/abs/1811.06746

Lisensi

GNU Affero General Public License (AGPL) Versi 3

Manual

Lihat nn_dependability_kit_manual.pdf

Coba alatnya

Contoh disajikan sebagai notebook Jupyter untuk memungkinkan pemahaman langkah demi langkah atas konsep.

• [Metrik & Generasi Kasus Uji] GTSRB_NEURON2PROQUICECOVERAGE_TESTGEN.IPYNB, atau GTSRB_ADDITIONALMETRICS.IPYNB, ATAU SCREENIO_COVERAGE_A9.IPYNB, atau KITti_Scenario_coverage.ipynb, or mnist_neuron2prroqueage.ipynb, or mnist_neuron2proqueage. Ssd_interpretationprecision.ipynb
• [Verifikasi Formal] TargetVehicleProcessingNetwork_FORMALVERIFIKASI.IPYNB
• [Verifikasi runtime] gtsrb_runtimemonitoring.ipynb, atau mnist_runtimemonitoring.ipynb

Struktur

Ada empat paket di bawah nndependability, yaitu

• BASIC: Pembaca untuk model serta representasi menengah NN (untuk tujuan verifikasi)
• Metrik: Hitung metrik ketergantungan untuk jaringan saraf
• ATG: Generasi kasus uji otomatis untuk meningkatkan metrik
• Formal: Verifikasi Formal (Analisis Statis, Pemecahan Kendala) dari Jaringan Saraf
• RV: Pemantauan runtime jaringan saraf

Paket Python Penting sebagai Persyaratan

• Pytorch + numpy + matplotlib + jupyter

• [Generasi Kasus Uji] Alat Penelitian Optimasi Google

• [Verifikasi / Analisis Statis] BULP (konektor MILP berbasis Python ke CBC dan pemecah lainnya)

  • Solver CBC yang telah dikirim pra-bubur mungkin macet dalam memecahkan beberapa masalah. Mesin analisis statis mengasumsikan bahwa pemecah GLPK dapat dipanggil (silakan atur variabel jalur), sehingga setiap kali CBC macet, GLPK secara otomatis dipicu sebagai pengganti. Sayangnya, ini tidak dapat menjamin bahwa kedua pemecah tidak akan macet pada saat yang sama. Oleh karena itu, untuk penggunaan industri kami sangat menyarankan untuk menggunakan IBM CPLEX sebagai pemecah MILP yang mendasarinya.
    • [GNU GLPK] http://www.gnu.org/software/glpk/
    • [Gplk di windows] http://winglpk.sourceforge.net/

• [Verifikasi run-time] dd (diagram keputusan biner diimplementasikan menggunakan python)

Gunakan persyaratan.txt untuk menginstal dependensi untuk menjalankan sebagian besar notebook (tidak termasuk TensorFlow).

Publikasi terkait

• [Metrik & Pembuatan Kasus Uji] https://arxiv.org/abs/1806.02338
• [Verifikasi Formal] https://arxiv.org/abs/1705.01040, https://arxiv.org/abs/1904.04706
• [Verifikasi Runtime] https://arxiv.org/abs/1809.06573
• [SSD-Example] Contoh ini menggunakan beberapa gambar dari Dataset VOC2012: Pascal Visual Object Class (VOC) Challenge Everingham, M., Van Gool, L., Williams, CKI, Winn, J. dan Zisserman, A. International Journal of Computer Vision, 88 (2), 303-338,

Topik lainnya

A. Metrik yang terkait dengan presisi intrepretasi dan sensitivitas oklusi

1. Paket tambahan untuk diinstal

• [Metrik] Saliency (https://github.com/pair-code/saliency) Gunakan dengan cara berikut:

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

2. Persiapan untuk contoh 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. Tantangan dalam verifikasi formal karena kurangnya spesifikasi input dan skalabilitas

Untuk melakukan verifikasi formal melalui jaringan saraf, ada dua masalah yang biasa terlihat.

• Skalabilitas verifikasi formal mungkin tidak dapat menangani jaringan yang sangat kompleks dan sangat dalam
• "Bentuk input" tidak diketahui. Memang salah satu biasanya menormalkan data sehingga setiap input umumnya memiliki kisaran [-1,1], tetapi kita mungkin ingin memiliki "penandakan berlebihan" yang lebih ketat atas data pelatihan.

Di NN-Dependability-Kit, kami menyarankan pengguna untuk melanjutkan dengan langkah-langkah berikut.

• Lakukan analisis dengan mengambil subnetwork lapisan dekat-ke-output seperti jaringan kuning dari gambar di bawah ini. Jika untuk setiap input ke jaringan kuning, seseorang menjamin bahwa output yang buruk tidak akan diproduksi, maka untuk setiap input ke jaringan asli yang sangat dalam & kompleks, tidak ada output buruk yang akan diproduksi.
  • Parameter ke -2 dan ke -3 dalam fungsi loadmlpfrompytorch () dalam nndependabilitas/dasar/pytorchreader.py mendukung konsep semacam itu

• Karena input ke jaringan yang lengkap hanya dapat mengarah pada nilai-nilai tertentu untuk input jaringan kuning, jika properti keselamatan tidak dapat dibuktikan pada jaringan kuning, rekomendasi kami lebih lanjut adalah memberi makan jaringan lengkap dengan data pelatihan, untuk memperoleh aproksimasi berlebih yang lebih ketat berdasarkan input yang dikunjungi untuk jaringan kuning. Contoh dapat ditemukan di neuron n^17_ {1}, di mana dengan menjalankan jaringan dengan semua data pelatihan yang tersedia, kita tahu bahwa data pelatihan membuat output dari n^17_ {1} dibatasi oleh [-0.1, 0.6]. Dengan demikian kita dapat menggunakan batasan terikat yang direkam sebagai batasan input untuk jaringan kuning untuk melakukan verifikasi formal.

  • Selain menggunakan interval, seseorang juga dapat merekam kendala oktagon atau bahkan pola aktivasi neuron untuk membuat penampilan berlebih yang lebih ketat dari data yang dikunjungi.

• Kebenaran verifikasi didasarkan pada asumsi bahwa tidak mungkin untuk memiliki nilai neuron yang duduk di luar interval yang dibuat, yang merupakan bukti yang ditunjuk oleh asumsikan . Asumsinya dapat dengan mudah dipantau dalam runtime.