چکیده
رویکردهای یادگیری ماشین بطور موفق برای خلق مولفه های کنترل با عملکرد بالا در سیستمهای رایا-فیزیکی مورد استفاده قرار گرفته اند و در آنها، دینامیک کنترل از ترکیب چند زیرسیستم بدست می آید. ولی ممکن است این رویکردها فاقد اعتبار لازم برای تضمین کاربرد معتبرشان در بافتی با ایمنی حیاتی باشند. ما در این مقاله، ترکیبی از تکنیکهای صحت سنجی اثبات قضیه و حساب بازه ای برای تحلیل ویژگیهای ایمنی در سیستمهای حلقه بسته که مولفه های شبکه عصبی را در برمیگیرند پیشنهاد میدهیم. ما کاربرد رویکرد پیشنهادی مان برای یک کنترلر پیش بینی کنندۀ مدل در رانندگی اتومات را شرح داده و عملکرد صحت سنجی شبکه عصبی را با سایر ابزارهای موجود مقایسه میکنیم. نتایج نشان میدهند که عملکرد صحت سنجی شبکه عصبی حلقه باز با کمک تکنیک حساب بازه ای در اثبات ویژگیها با سربار زمانی کوچکتر، بهتر از سایر رویکردهای موجود است. ما همچنین قابلیت ترکیب دو رویکرد را برای ساختن یک مدل رسمی از شبکه در منطق مرتبه بالاتر سیستم کنترل شده در یک حلقه بسته شرح میدهیم.
مطالعات مرتبط
چند مطالعه بر صحت سنجی رسمی یا تحلیلی شبکه های عصبی با کمک چندین تئوری متمرکز شده اند که اکثر آنها از تابع فعالسازی واحد یکسوشده خطی (ReLU) شبکه عصبی پیشخور استفاده میکنند. جدول 1 خلاصه ای از پژوهشهای مختلف گروه بندی شده بر حسب رویکرد / تکنولوژی مبنای بکار رفته برای صحت سنجی را نشان میدهد.
ابزار مبتنی بر نظریه صدق پذیری در پیمانه (SMT)
محققان مطالعه Katz و دیگران (2017) تکنیک سودمندی در استفاده از STM برای صحت سنجی شبکه های عصبی عمیق (کاملاً متصل) مبتنی بر تابع ReLU پیشنهاد میدهند. محققان مطالعه Puline و Tacchella (2010)، روش STM مشابهی برای صحت سنجی پرسپترون چندلایه توصیف کرده و شبکه های عصبی پیشخور مبتنی بر تابع سیگموئید را با یک تابع فعالسازی خطی تکه ای استخراج کردند. مجدد محققان از توابع فعالسازی شبه-ReLU در مطالعه Ehlers (2017) استفاده کردند تا یک رویکرد STM برای صحت سنجی ویژگیهای شبکه های عصبی پیشخور خطی تکه ای پیشنهاد دهند. همچنین مجدداً بر مبنای توابع فعالسازی ReLU، محققان در مطالعه Katz و دیگران (2019)، رویکرد Marabou را بعنوان مکمل مطالعه Katz و دیگران (2017) برای ارتقای قابلیتهای صحت سنجی لایه پیچشی و لایه ادغام معرفی کردند. سایر روشها مثل Narodyoska و دیگران (2018) بواسطه برخورداری از امتیاز نظریه صدق پذیری بولی، از حلگرهای SAT و حلگرهای صدق پذیری گزاره ای برای صحت سنجی ویژگیهای شبکه عصبی استفاده میکنند.
