גיא כץ

פרס קריל 2021
האונ' העברית בירושלים

גיא כץ (Guy Katz) – אימות פורמלי של רשתות נוירונים עמוקות.

 

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

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

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

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

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

זוכי פרס קריל

// order posts by year $posts_by_year;