หน้าแรก>ซอร์สโค้ด JSP>หมวดหมู่อื่นๆ
ดาวน์โหลด

Nn-dependability-kit

NN-predability-KIT เป็นเครื่องมือการวิจัยโอเพนซอร์ซเพื่อช่วยเครือข่ายประสาทวิศวกรรมสำหรับโดเมนที่สำคัญต่อความปลอดภัย

C.-H. Cheng, C.-H. Huang และ G. Nührenberg NN-dependability-KIT: เครือข่ายประสาทวิศวกรรมสำหรับระบบขับขี่แบบอิสระที่สำคัญต่อความปลอดภัย https://arxiv.org/abs/1811.06746

ใบอนุญาต

GNU Affero ทั่วไปใบอนุญาตสาธารณะ (AGPL) เวอร์ชัน 3

คู่มือ

ดู nn_dependability_kit_manual.pdf

ลองใช้เครื่องมือ

ตัวอย่างจะถูกนำเสนอเป็นสมุดบันทึก Jupyter เพื่อให้เข้าใจแนวคิดทีละขั้นตอน

  • [การสร้างตัวชี้วัดและการสร้างกรณีการทดสอบ] GTSRB_NEURON2PROUCTIONCOVERAGE_TESTGEN.IPYNB หรือ GTSRB_ADDITIONALMETRICS.IPYNB หรือ SCINARIO_COVERAGE_A9.IPYNB หรือ KITTI_SCENARIO_COVERAGE.IPYNB ssd_intertationprecision.ipynb
  • [การตรวจสอบอย่างเป็นทางการ] TargetVehicleProcessingNetwork_formalverification.ipynb
  • [การตรวจสอบรันไทม์] gtsrb_runtimemonitoring.ipynb หรือ mnist_runtimemonitoring.ipynb

โครงสร้าง

มีสี่แพ็คเกจภายใต้การพึ่งพา NNDA

  • พื้นฐาน: ผู้อ่านสำหรับแบบจำลองเช่นเดียวกับการเป็นตัวแทนระดับกลางของ NN (เพื่อวัตถุประสงค์ในการตรวจสอบ)
  • ตัวชี้วัด: คำนวณตัวชี้วัดความน่าเชื่อถือสำหรับเครือข่ายประสาท
  • ATG: การสร้างกรณีทดสอบอัตโนมัติเพื่อปรับปรุงตัวชี้วัด
  • อย่างเป็นทางการ: การตรวจสอบอย่างเป็นทางการ (การวิเคราะห์แบบคงที่การแก้ข้อ จำกัด ) ของเครือข่ายประสาท
  • RV: การตรวจสอบรันไทม์ของเครือข่ายประสาท

แพ็คเกจงูหลามที่สำคัญเป็นข้อกำหนด

  • pytorch + numpy + matplotlib + jupyter

  • [การสร้างกรณีทดสอบ] เครื่องมือวิจัยการเพิ่มประสิทธิภาพของ Google

  • [การตรวจสอบการตรวจสอบ / การวิเคราะห์คง

    • CBC Solver ที่จัดส่งล่วงหน้าด้วยเยื่อกระดาษอาจพังในการแก้ปัญหาบางอย่าง เครื่องยนต์วิเคราะห์แบบสแตติกสันนิษฐานว่าตัวแก้ปัญหา GLPK สามารถเรียกได้ (โปรดตั้งค่าตัวแปรพา ธ ) เช่นเมื่อใดก็ตามที่ CBC ล่ม GLPK จะถูกกระตุ้นโดยอัตโนมัติเป็นการเปลี่ยน น่าเสียดายที่สิ่งนี้ไม่สามารถรับประกันได้ว่าตัวแก้ปัญหาทั้งสองจะไม่พังในเวลาเดียวกัน ดังนั้นสำหรับการใช้งานอุตสาหกรรมเราแนะนำอย่างยิ่งให้ใช้ IBM CPLEX เป็นตัวแก้ปัญหา MILP
      • [gnu glpk] http://www.gnu.org/software/glpk/
      • [gplk บน windows] http://winglpk.sourceforge.net/

  • [การตรวจสอบเวลาทำงาน] DD (ไดอะแกรมการตัดสินใจแบบไบนารีใช้โดยใช้ Python)

ใช้ข้อกำหนด. txt เพื่อติดตั้งการพึ่งพาเพื่อเรียกใช้สมุดบันทึกส่วนใหญ่ (ไม่รวม 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] ตัวอย่างใช้รูปภาพสองสามภาพจากชุดข้อมูล VOC2012: Pascal Visual Object Classes (VOC) Challenge Everingham, M. , Van Gool, L. , Williams, CKI, Winn, J. และ Zisserman, A. วารสาร International Journal of Computer Vision, 88 (2), 303-338, 2010, 2010, 2010

หัวข้ออื่น ๆ

A. ตัวชี้วัดที่เกี่ยวข้องกับความแม่นยำในการติดต่อและความไวของการบดเคี้ยว

1. แพ็คเกจเพิ่มเติมที่จะติดตั้ง

  • [ตัวชี้วัด] Saliency (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. ความท้าทายในการตรวจสอบอย่างเป็นทางการเนื่องจากขาดข้อมูลจำเพาะอินพุตและความยืดหยุ่น

ในการทำการตรวจสอบอย่างเป็นทางการเกี่ยวกับเครือข่ายประสาทมีปัญหาสองประการที่เห็นกันทั่วไป

  • ความสามารถในการปรับขนาดของการตรวจสอบอย่างเป็นทางการอาจไม่สามารถจัดการกับเครือข่ายที่ซับซ้อนและลึกมากได้มาก
  • ไม่ทราบรูปร่างของ "รูปร่างของอินพุต" อันที่จริงหนึ่งปกติทำให้ข้อมูลปกติดังนั้นทุกอินพุตมักจะมีช่วง [-1,1] แต่เราอาจต้องการที่จะมี "การเปลี่ยนแปลงมากเกินไป" ที่เข้มงวดมากขึ้นเหนือข้อมูลการฝึกอบรม

ใน KIT ที่พึ่งพา NN เราแนะนำให้ผู้ใช้ดำเนินการตามขั้นตอนต่อไปนี้

  • ทำการวิเคราะห์โดยการใช้ เครือข่ายย่อยของเลเยอร์ที่ใกล้เคียงกับเอาต์พุต เช่นเครือข่ายสีเหลืองของรูปด้านล่าง หากสำหรับทุกอินพุตไปยังเครือข่ายสีเหลืองหนึ่งรับประกันว่าเอาต์พุตที่ไม่ดีจะไม่ถูกสร้างขึ้นดังนั้นสำหรับทุกอินพุตไปยังเครือข่ายที่ลึกและซับซ้อนดั้งเดิมจะไม่มีการผลิตเอาต์พุตที่ไม่ดี
    • พารามิเตอร์ที่ 2 และ 3 ในฟังก์ชั่น loadmlpfrompytorch () ใน nndependability/basics/pytorchreader.py สนับสนุนแนวคิดดังกล่าว

การวาดภาพ

  • เนื่องจากอินพุตไปยังเครือข่ายที่สมบูรณ์อาจนำไปสู่ค่าบางอย่างสำหรับอินพุตของเครือข่ายสีเหลืองหากคุณสมบัติ ด้านความปลอดภัยไม่สามารถพิสูจน์ได้ในเครือข่ายสีเหลืองคำแนะนำเพิ่มเติมของเราคือการป้อนเครือข่ายที่สมบูรณ์ด้วยข้อมูลการฝึกอบรม ตัวอย่างสามารถพบได้ในเซลล์ประสาท n^17_ {1} โดยที่เรียกใช้เครือข่ายด้วยข้อมูลการฝึกอบรมที่มีอยู่ทั้งหมดเรารู้ว่าข้อมูลการฝึกอบรมทำให้ผลลัพธ์ของ n^17_ {1} ล้อมรอบด้วย [-0.1, 0.6] เราสามารถใช้ขอบเขตที่บันทึกไว้เป็นข้อ จำกัด อินพุตสำหรับเครือข่ายสีเหลืองเพื่อทำการตรวจสอบอย่างเป็นทางการ

    • นอกเหนือจากการใช้ช่วงเวลาแล้วเรายังสามารถบันทึกข้อ จำกัด แปดเหลี่ยมหรือแม้แต่รูปแบบการเปิดใช้งานเซลล์ประสาทเพื่อสร้างการตรวจสอบที่เข้มงวดมากขึ้นของข้อมูลที่เข้าชม

  • ความถูกต้องของการตรวจสอบขึ้นอยู่กับสมมติฐานที่ว่าเป็นไปไม่ได้ที่จะมีค่าเซลล์ประสาทที่อยู่นอกช่วงเวลาที่สร้างขึ้นซึ่งเป็นหลักฐาน การสันนิษฐาน สมมติฐานสามารถตรวจสอบได้ง่ายในรันไทม์

ขยาย
ข้อมูลเพิ่มเติม
แอปที่เกี่ยวข้อง
แนะนำสำหรับคุณ
ข้อมูลที่เกี่ยวข้อง ทั้งหมด