פרויקטי גמר - הנדסת מחשבים - תואר ראשון - רשתות וחישוב תשפ"ד

הרקע לפרויקט:

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

1. בניית מערכת התוכנה
2. עיסוק ברשתות למידה עבור וידאו וקבלת החיזוי

מטרת הפרויקט:

מהות הפרויקט הוא בנייה של מערכת תוכנה כולל מסכים, ממשקים ולוגיקה.

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

על הסרטון תופעל רשת למידה עמוקה אשר תוצאתה חיזוי של הפעולות שבוצעו הסרטון + אלגוריתם לשיפור החיזוי.

בשלב א - יופעלו רשתות סטנדרטיות ובשלב ב - כולל אלגוריתם השיפור והשוואתו למודל תהליך לזיהוי פערים.

הפלט יהיה רשימת הפעולות שקרו בסרטון והשוואה למודל התהליך.

תכולת הפרויקט:

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

קורסי קדם:

יש לקחת קורס מידול וכריית תהליכים, קורס מבוא ללמידת מכונה (יכול להיות במקביל)

דרישות נוספות:

ידע טוב בתכנות, אם לא נלמד בפקולטה - יש לקחת קורס למידה עמוקה בפלטפורמת אונליין.

מקורות:

https://ceur-ws.org/Vol-2938/paper-PROBLEMS-51.pdf
https://arxiv.org/pdf/2208.03775.pdf

הרקע לפרויקט:

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

מטרת הפרויקט:

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

תכולת הפרויקט:

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

קורסי קדם:

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

דרישות נוספות:

יכולת תכנות גבוהה

מקורות:

https://drive.google.com/file/d/1WAOVDmMDfXpxZ0X0IXu6LAzFKJSVMLrQ/view

הרקע לפרויקט:

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

מטרת הפרויקט:

להצליח להראות תרומה של כלי אימות פורמלי עבור בעיות RL המשלבות רשתות נוירונים עמוקות.

תכולת הפרויקט:

בנייה ותכנון של בעיות המשתמשות ב-DRL, שניתן להשתמש עבורן בכלי אימות פורמלי על מנת לייצב את הלמידה ולאפשר לה להתכנס.

קורסי קדם:

למידה מבוססת חיזוקים, אימות פורמלי וסינטזה

דרישות נוספות:

יכולת תכנות גבוהה

מקורות:

https://drive.google.com/file/d/1WAOVDmMDfXpxZ0X0IXu6LAzFKJSVMLrQ/view

הרקע לפרויקט:

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

מטרת הפרויקט:

מטרת פרויקט זה היא לפתח חבילה בשפת פיית׳ון המאפשרת קידוד ופענוח מהיר של מידע. קימות מספר חבילות עבור קודים מסוג Reed-Solomon אך בפרוייקט זה המטרה היא לפתח קוד מהיר במיוחד אשר ניתן לקידוד ופענוח בזמן לינארי [1]. נרצה לפתח ספריית תוכנה (package) אשר תאפשר קידוד ופענוח של הודעות בגדלים שונים עם פרמטרי קוד שונים. החבילה צריכה להיות ממוקמת בrepository סטנדרטי כך שניתן יהיה להתקינה ע״י מתקין חבילות סטנדרטי כמו pip.

תכולת הפרויקט:

שלבי הפרויקט הם: (1) הבנת אלגוריתם פעולת הקוד שבמאמר [1], (2) מימוש אלגוריתם קידוד ופענוח להודעות עבור מספר רב של פרמטרים ואורכי הודעה. (3) עטיפת ספרית הקוד כחבילת פיית׳ון (package) הניתנת להורדה והתקנה ע״י כלל משתמשי פיית׳ון (4) ביצוע בדיקות תקינות, והשוואת מהירות קידוד/פענוח מול קודי תיקון-שגיאות אחרים (חבילות פית׳ון קיימות).

קורסי קדם:

תכנות פייתון או הנדסת תוכנה
מבוא לתורת הצפינה

דרישות נוספות:

פרוייקט זה מצריך יכולת הבנה מתמטית גבוהה ויכולת התמדה בקריאת מאמר אלגוריתמי והבנתו לעומק (כולל אלגוריתמי המשנה).

מקורות:

1. “Linear Time Encodable and List Decodable Codes”, V. Guruswami and P. Indyk, STOC 2003. https://people.eecs.berkeley.edu/~venkatg/pubs/papers/linear-ld.pdf

הרקע לפרויקט:

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

מטרת הפרויקט:

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

תכולת הפרויקט:

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

1. היכולת ליצור רשתות בגודל משתנה (עד אלפי מחשבים מקבילים). יכולת מתן מידע שונה למכשירים שונים (למשל, ID או מידע על טופולוגיית הרשת).
2. סימולציה של תקשורת סינכרונית בין המחשבים.
3. הזרקת שגיאות בתקשורת.
4. אפשור כשלים בחלק מהמכשירים (למשל: הדמית מחשב שנתקע והשפעתו על שאר הרשת).
5. מימוש אלגוריתם שנלמד כחלק מהקורס חישוב מבוזר.
6. מימוש סביבת בדיקות וגילוי טעויות מימוש באלגוריתמים.
7. ויזואליזציה של הרשת והתנהגותה, זיהוי צווארי בקבוק. ועוד ועוד.

קורסי קדם:

• הנדסת תוכנה
• חישוב מבוזר

מקורות:

1. David Peleg, DISTRIBUTED COMPUTING A Locality-Sensitive Approach, 2000 SIAM
2. Attiya and Welch, Distributed Computing Fundamentals, Simulations and Advanced Topics, 2nd ed, JOHN WILEY &SONS, INC., 2004

הרקע לפרויקט:

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

מטרת הפרויקט:

בפרויקט זה נפתח מערכת המלצה לבתי קפה. קפה איכותי הוא קפה שמיוצר ע״י מכונת קפה מקצועית (כזו שטוחנים בה את הפולים, למשל), ולא ע״י מכונה אוטומטית או חלילה, קפה שנשמר בתרמוס. מערכת ההמלצה של גוגל-מפות משתמשת בדירוגי כלל המשתמשים (שלא תמיד מבינים בקפה). מערכת זו אינה מתאימה לאוהבי הקפה, שמעדיפים קפה שהוכן ביד מקצועית, במכשור הנכון ובמיומנות הנדרשת. הפרוייקט יכלול מערכת תוכנה שתסרוק את התמונות שמעלים המשתמשים בgoogle map ותנסה לזהות בתי קפה ״איכותיים״. הקושי כאן הוא להגדיר מהו בית קפה איכותי ואיך ניתן לזהות זאת מהתמונות / טקסטים שהעלו הממליצים. התוכנה תשתמש במערכות למידת מכונה ML על מנת לזהות מהתמונות מאפיינים המגדירים קפה איכותי (למשל: מכונה מקצועית, או דירוג לפי צילומי כוסות הקפה שהוכנו). המערכת תשקלל את הגורמים הללו ליצירת המלצה המתאימה לחובבי קפה.

תכולת הפרויקט:

שלבי הפרויקט יכילו : (1) הגדרת התוכנה ויכולותיה לפי הרעיון לעיל (2) איסוף תמונות וסיווגן, אימון מערכת למידה ממוחשבת ML למתן ציון מתאים (3) פיתוח מלא של אתר/אפליקציה המממש את המערכת ומשקלל את תוצאות הML עם שאר הציונים. (4) בדיקת המערכת על בתי קפה בעולם.

קורסי קדם:

הנדסת תוכנה
מבוא ללמידת מכונה

מקורות:

n/a

הרקע לפרויקט:

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

מטרת הפרויקט:

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

תכולת הפרויקט:

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

קורסי קדם:

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

מקורות:

1. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
2. A. Pnueli and R. Rosner "On the synthesis of a reactive module". POPL '89 Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, Pages 179-190, 1989.
3. Boyan Yordanov, Sara-Jane Dunn, Colin Gravill, Hillel Kugler, Christoph M Wintersteiger
4. An SMT-Based Framework for Reasoning About Discrete Biological Models. ISBRA’22, LNCS Springer 2022.

הרקע לפרויקט:

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

מטרת הפרויקט:

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

תכולת הפרויקט:

במהלך הפרויקט הסטודנטים ירכשו ידע בשיטות אימות פורמלי וסינתזה (Formal Verification and Synthesis) פיתוח רשתות ביולוגיות עבור בעיות NP קשות, תיאור הרשתות בעזרת כלי אימות ושימוש בכלים אלה על מנת לנתח את המעגלים. נשתמש בכלים שהם state of the art בתחום אימות פורמלי של חומרה.

קורסי קדם:

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

מקורות:

1. Nicolau, Dan V., et al. "Parallel computation with molecular-motor-propelled agents in nanofabricated networks." Proceedings of the National Academy of Sciences, 2016.
2. Michelle Aluf-Medina, Till Korten, Avraham Raviv, Dan V. Nicolau Jr. and Hillel Kugler. Formal Semantics and Verification of Network-Based Biocomputation Circuits, VMCAI’21. https://link.springer.com/chapter/10.1007/978-3-030-67067-2_21
3. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995).
4. Pradheebha Surendiran, Christoph Robert Meinecke, Aseem Salhotra Georg Heldt
5. Georg Heldt, Jingyuan Zhu, Alf Månsson, Stefan Diez, Danny Reuter, Hillel Kugler, Heiner Linke, and Till Korten. Solving Exact Cover Instances with Molecular-Motor-Powered Network-Based Biocomputation. (2022).