nn-ependability-kit
NN-Dependable-KIT هي أداة بحث مفتوحة المصدر لمساعدة الشبكات العصبية الهندسية للمجالات الحرجة للسلامة.
C.-H. Cheng ، C.-H. هوانغ ، وج. نورنبرغ. NN-Dependable-KIT: الشبكات العصبية الهندسية لأنظمة القيادة المستقلة الحرجة للسلامة . https://arxiv.org/abs/1811.06746
رخصة
Gnu Affero General License (AGPL) الإصدار 3
يدوي
انظر nn_dependability_kit_manual.pdf
جرب الأداة
يتم تقديم أمثلة على أنها دفاتر Jupyter للسماح بفهم خطوة بخطوة على المفاهيم.
- [مقاييس وتوليد حالة الاختبار] gtsrb_neuron2projectioncoverage_testgen.ipynb ، أو gtsrb_additionalmetrics.ipynb ، أو sinario_coverage_a9 ssd_interpretationprecision.ipynb
- [التحقق الرسمي] TargetveHicleProcessingNetwork_Formalverification.ipynb
- [التحقق من وقت التشغيل] gtsrb_runtimemonitoring.ipynb ، أو mnist_runtimemonitoring.ipynb
بناء
هناك أربع حزم تحت قابلية nndepend
- أساسي: قارئ للنماذج وكذلك التمثيل الوسيط لـ NN (لأغراض التحقق)
- المقاييس: حساب مقاييس الاعتمادية للشبكات العصبية
- ATG: توليد حالة الاختبار التلقائي لتحسين المقاييس
- رسمي: التحقق الرسمي (التحليل الثابت ، حل القيد) للشبكات العصبية
- RV: مراقبة وقت التشغيل للشبكات العصبية
حزم بيثون مهمة كمتطلبات
pytorch + numpy + matplotlib + jupyter
[توليد حالة اختبار] أدوات أبحاث تحسين Google
[التحقق / التحليل الثابت] اللب (موصل MITHON المستند إلى Python إلى CBC وغيرها من الحلول)
- CBC Solver قبل الشحنة مع اللب قد تعطل في حل بعض المشاكل. يفترض محرك التحليل الثابت أنه يمكن استدعاء GLPK Solver (يرجى إعداد متغير المسار) ، بحيث يتم تشغيل GLPK تلقائيًا كبديل. لسوء الحظ ، لا يمكن أن يضمن هذا أن كلا المحللين لن ينهاران في نفس الوقت. لذلك ، من أجل الاستخدام الصناعي ، ننصح بشدة استخدام IBM Cplex باعتباره MILP Solver الأساسي.
- [GNU GLPK] http://www.gnu.org/software/glpk/
- [gplk on windows] http://winglpk.sourceforge.net/
[التحقق من وقت التشغيل] DD (مخطط القرار الثنائي الذي تم تنفيذه باستخدام Python)
استخدم المتطلبات. txt لتثبيت التبعيات لتشغيل معظم دفاتر الملاحظات (باستثناء TensorFlow).
المنشورات ذات الصلة
- [Metrics & Test Case Generation] 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 (VOC) Everingham ، M.
مواضيع أخرى
أ. المقاييس المتعلقة بدقة التهوية وحساسية انسداد
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 ../../
التحديات في التحقق الرسمي بسبب نقص مواصفات الإدخال وقابلية التوسع
للقيام بالتحقق الرسمي على الشبكات العصبية ، هناك مشكلتان شائعتان.
- قد لا تكون قابلية التحقق الرسمية قادرة على التعامل مع شبكات معقدة للغاية وعميقة للغاية
- "شكل المدخلات" غير معروف. في الواقع ، يقوم المرء عادةً بتطبيع البيانات بحيث يكون لكل إدخال عادة نطاقًا من [-1،1] ، لكن قد نرغب في الحصول على "الإفراط في القرب" على بيانات التدريب.
في NN-Dependable-KIT ، ننصح المستخدمين بالمضي قدماً في الخطوات التالية.
- قم بإجراء التحليل من خلال أخذ شبكة فرعية من الطبقات القريبة من الإخراج مثل الشبكة الصفراء للشكل أدناه. إذا كان لكل إدخال إلى الشبكة الصفراء ، أنه لن يتم إنتاج الإخراج السيئ ، فكل مدخلات إلى الشبكة الأصلية العميقة والمعقدة ، لن يتم إنتاج أي إخراج سيئ.
- المعلمات الثانية والثالثة في وظيفة loadmlpfrompytorch () في nndependability/الأساسيات/pytorchreader.py دعم مثل هذا المفهوم
نظرًا لأن المدخلات إلى الشبكة الكاملة قد تؤدي فقط إلى قيم معينة لإدخال الشبكة الصفراء ، إذا كان لا يمكن إثبات خاصية الأمان على الشبكة الصفراء ، فإن توصيتنا الإضافية هي إطعام الشبكة الكاملة مع بيانات التدريب ، من أجل استخلاص الإفراط في القرب من التشديد استنادًا إلى المدخلات التي تمت زيارتها للشبكة الصفراء. يمكن العثور على مثال في Neuron n^17_ {1} ، حيث من خلال تشغيل الشبكة مع جميع بيانات التدريب المتاحة ، نعلم أن بيانات التدريب تجعل إخراج n^17_ {1} يحدها [-0.1 ، 0.6]. يمكننا بالتالي استخدام الحد المسجل كقيود إدخال للشبكة الصفراء لإجراء التحقق الرسمي.
- بصرف النظر عن استخدام الفواصل الزمنية ، يمكن للمرء أيضًا تسجيل قيود المثمن أو حتى أنماط تنشيط الخلايا العصبية لإنشاء تشويش أكثر إحكاما للبيانات التي تمت زيارتها.
تستند صحة التحقق إلى افتراض أنه من المستحيل أن يكون هناك قيم خلية للخلايا العصبية تجلس خارج الفاصل الزمني الذي تم إنشاؤه ، وهو دليل على الافتراض . يمكن مراقبة الافتراض بسهولة في وقت التشغيل.
