אתה שוגה, אלגוריתם

לפעמים, הדרך הכי טובה לתקן משהו היא לנסות להרוס אותו. כך עובד אימות פורמלי – ניסיונות לערער את מערכות התוכנה ולהוכיח את נכונותן, כדי לוודא שהן נטולות באגים. לאחרונה הגיעו הסטודנטים יעל ליבוביץ וייס ועומר כהן לתוצאות מעניינות מאוד בתחום, במסגרת פרויקט שלהם בתחום האימות הפורמלי והלמידה העמוקה, בהנחיית פרופ' הלל קוגלר והדוקטורנט אברהם רביב. "הפרויקט עסק בשילוב כלים של אימות אלגוריתמים באלגוריתמים של זיהוי אובייקטים, כאלו המוטמעים במצלמות של רכב אוטונומי, למשל, וצריכות לזהות את כל האובייקטים מסביב: כביש, תמרורים, מכוניות, אנשים וכולי", מספר אברהם רביב. "במסגרת הפרויקט, השתמשו הסטודנטים במודלים של למידה עמוקה, המשמשים בין היתר לסיווג וזיהוי של אובייקטים בתמונה, ובכלי אימות פורמלי על מנת לבדוק כיצד האלגוריתמים של זיהוי אובייקטים מתמודדים עם תמונות מורעשות".

הפרויקט נעשה במסגרת המסלול להנדסת מחשבים. יעל ועומר לומדים שניהם במסלול, במסגרת תוכנית אקדמיה בתיכון, עם התמחות בסייבר ובעיבוד וניתוח נתונים. הפרויקט ממשיך את עבודתו של רועי אסא, סטודנט לשעבר באותה התוכנית, ופותח לראשונה במסגרת ההאקתון של הפקולטה. "המטרה בפרויקט הייתה להצליח למצוא התקפות על מיקום האובייקט, התקפות חדשניות שנחשבות קשות יחסית לאיתור", מספרת יעל. "במסגרת הפרויקט השתמשנו בכלים של אימות פורמלי כדי ליצור הרעשה מינימלית לתמונות, כזו שכמעט ולא נראית לעין, אבל שתגרום למודל הלמידה העמוקה לסווג את האובייקטים בתמונה בצורה לא נכונה. חילקנו את ההתקפות לארבע סוגי התקפות עיקריים. הראשונה, והמעניינת ביותר, היא התקפה על מיקום האובייקט; השנייה - התקפה על סיווג האובייקט; השלישית היא שבנוסף לאובייקט המקורי שזוהה נכון זוהו עוד אובייקטים שאינם נכונים; והרביעית היא שבנוסף לאובייקט המקורי שזוהה לא נכון, זוהו אובייקטים נוספים שאינם נכונים. רצינו להוכיח שניתן לתקוף את הרשת עבור כל אחת מהמתקפות".

הפרויקט הציג תוצאות מעניינות מאוד. "בפועל, הצלחנו לשלב כלי של אימות פורמלי שייצור התקפות רעש על מודל למידה עמוקה שמסווג מספר רב של אובייקטים בתמונה (ולא אחד), תוך התחשבות במיקום האובייקט בתמונה", אומר עומר. "התוצאות שהגענו אליהן ייחודיות, כי הראינו שאנו מצליחים להוסיף רעש מזערי לתמונות וזה גורם לאלגוריתם לשגיאות משמעותיות, כמו למשל לזהות אובייקטים במקומות לא נכונים - מה שיכול להיות מאוד קריטי, למשל, ברכב אוטונומי. ומרגע שגילינו את השגיאות האלה – אפשר לעבור על האלגוריתם כדי לתקן אותו. בשורה התחתונה, התוצאות האלה יכולות להפוך את הרכבים האוטונומיים לבטוחים יותר".