זיהוי שגיאות ואימות פורמלי של למידה מבוססת חיזוקים

ברכות לאור רג'יניאנו ואליה ברונשטיין, סטודנטיות שנה ד' במסלול להנדסת מחשבים, שפרויקט הגמר שלהן, "זיהוי שגיאות ואימות פורמלי של למידה מבוססת חיזוקים", התקבל כהרצאה בכנס pycon. הכנס יתקיים במרכז וואהל, ליד בר-אילן, בתאריכים 29-28 ליוני 2022, והוא עוסק בשפת התכנות פייתון וגישות חדשות בה.

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

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