כיצד נדע אם אפשר לסמוך על מכונית ללא נהג או מטוס ללא טייס? בוגר מכון ויצמן פיתח שיטה לבדיקת מהימנות תוכנות שנכתבו על ידי מחשבים
חיינו עשויים להיות תלויים ביכולת לבדוק את החישובים של המכונות שלנו. פעולות כגון נהיגה במכונית או הטסת מטוס מחייבות הערכה מהירה של המצב וקבלת החלטות תוך שברירי שנייה. אולם, ייתכן כי יום יבוא, ומי ש”יכתוב” את האלגוריתמים המתוחכמים המאפשרים להפוך מכונות לאוטונומיות – למשל, מכונית שתיסע ללא נהג, רובוט שיניע את עצמו, או אפילו מטוס שיטיס את עצמו – יהיו מחשבים. זאת ועוד, לעיתים קרובות, סוג חדש זה של תוכנה, הנדרש למשימות מורכבות במיוחד, עולה בביצועיו על התוכנה שבני אדם מסוגלים לכתוב. אך האם נוכל לשים את מבטחנו בתוכנות אלה?
ד”ר גיא כץ, בוגר מכון ויצמן אשר עומד להצטרף לסגל בית הספר להנדסה ולמדעי המחשב על-שם רחל וסלים בנין באוניברסיטה העברית, פיתח שיטה שיכולה לאמת את מידת הדיוק של תוכנות מסוימות ש”כתבו” מכונות. אלה תוכנות הידועות כ”רשתות עצביות עמוקות”, בשל הדמיון בין המבנה שלהן לבין זה של תאי עצב במוח, והן מיוצרות בדרך של “למידת מכונה”, אשר מחקה את תהליך הלמידה האנושית. “הבעיה היא”, מסביר ד”ר כץ, שערך את מחקר הדוקטורט שלו במעבדה של פרופ’ דוד הראל מהמחלקה למדעי המחשב ומתמטיקה שימושית, “שהתוכנות מהוות מעין קופסה שחורה”.
רשת עצבית מורכבת בעיקר ממתגים רבים, שכל אחד מהם עשוי להיות באחד משני מצבים – “הפעל” או “כַּבֵּה” (on/off). לתוכנית שֶיֵש בה 300 מתגים, יש 2300 תצורות אפשריות. לכאורה, כדי לדעת אם תוכנה תפעל כראוי בכל פעם, היה צריך לבדוק כל אחת מהתצורות האפשריות, וברור שזו בעיה: כיצד ניתן לבדוק משהו כה מורכב? ולא זו בלבד, אלא שבדיקות מוקדמות של מכוניות אוטונומיות כבר לימדו, כי תמיד יתרחשו אירועים בלתי-צפויים בנהיגה בעולם האמיתי.
כץ הצליח לצמצם את מספר התצורות שיש לבדוק – מ-2300 לכמיליון. מיליון אולי נשמע הרבה, אבל מספר זה נמצא בגבולות היכולת החישובית של מחשב
במחקר הבתר-דוקטוריאלי שלו באוניברסיטת סטנפורד עבד ד”ר כץ עם תוכנה המיועדת למנוע התנגשויות של מטוסים שמפתחת רשות התעופה הפדרלית בארצות הברית, ה-FAA. הוא חיפש דרך לצמצם את מספר התצורות האפשריות שצריך לבדוק, באמצעות יצירת שיטה לקביעת אילו מבין המצבים האפשריים הרבים לא יוכלו להתרחש בפועל. יחד עם קלארק בארט, דייוויד דיל, קייל ג’וליאן ומייקל קוקנדרפר, כולם מאוניברסיטת סטנפורד, הצליח כץ לצמצם את מספר התצורות שיש לבדוק – מ-2300 לכמיליון. מיליון אולי נשמע הרבה, אבל מספר זה נמצא בגבולות היכולת החישובית של מחשב, בעוד שמספר האפשרויות הכולל הוא הרבה מעבר לטווח של המחשב החזק ביותר.
כאשר צוות המחקר בדק את התוכנה שמפתחת רשות התעופה הפדרלית, בתהליך הידוע כ”אימות”, הם גילו שכל התכונות שנבדקו עמדו בבדיקה, מלבד אחת, אשר תוקנה בהמשך. מאמר המתאר תוצאות אלו יתפרסם במסגרת הכנס Computer Aided Verification) CAV) שיתקיים השנה.
ד”ר כץ מתכוון להמשיך ולחקור אמצעים לאימות הפונקציונליוּת של תוכנות שנכתבות באמצעות למידת מחשב. מלבד רשות התעופה הפדרלית, ד”ר כץ והצוות מסטנפורד עובדים עם חברת “אינטל” על פרויקט של רכב אוטונומי. פרויקט זה, הוא אומר, גדול בכמה דרגות מזה שכבר השלימו: “למרות המשותף לכל המערכות המשתמשות ברשתות עצביות עמוקות, יש גם חלקים ייחודיים לכל מערכת. אנו פועלים בשיתוף פעולה הדוק עם המהנדסים והמומחים המפתחים מערכות אלו, על מנת להבין אילו תכונות צריכות להיבדק, וכיצד ניתן להאיץ את הבדיקה. תחום זה עדיין מצריך מעורבות של בני-אדם”.
ראו עוד בנושא באתר הידען:
