אימות פורמלי של רשתות נוירונים ולמידה עמוקה

Formal Verification of Neural Networks and Deep Learning

אימות פורמלי (Formal Verification) מאפשר שימוש באלגוריתמים ושיטות מתמטיות להוכחת נכונות של מערכות תוכנה וחומרה מורכבות. אחד האתגרים המרכזיים הנוכחיים הוא לתאר פתרונות שהתקבלו בשיטות של Deep Learning ולהוכיח שהם אכן עומדים בדרישות. החשיבות של הוכחת נכונות של מערכת נוירונים נעשית משמעותית לאור ההתקדמות הדרמטית בשיטות ללמוד רשתות אך המגבלות הקיימות בהבנת ההתנהגות של הרשת שנלמדה. 

במהלך הפרויקט הסטודנטים ירכשו ידע באימות פורמלי (Formal Verification) ויישמו אותו באמצעות פיתוח אלגוריתמים שמאפשרים לתאר ולאפיין התנהגות דינמית של רשתות נוירונים. הפרויקט ידרוש הבנת תאורטית של החומר ויכולת תכנות גבוהה למימוש יעיל של האלגוריתמים. 
 

דרישות:

83691 Formal Verification and Synthesis (במקביל לפרויקט)

83670 Biological Computation (במקביל לפרויקט)
 

מקורות:

Ian Goodfellow, Yoshua Bengio and Aaron Courville. Deep Learning. MIT Press, 2016.

G. Katz, C. Barrett, D. Dill, K. Julian and M. Kochenderfer. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks.Proc. 29th Int. Conf. on Computer Aided Verification (CAV). Heidelberg, Germany, July 2017. To appear. 

Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).