Combining Machine Learning and Verification for uncovering GRNs of Kidney Cells

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

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

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

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

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

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

קורסי קדם:

83670 Biological Computation

מקורות:

1. B. Yordanov S-J Dunn, H. Kugler, A. Smith, G. Martello and S. Emmott. A method to identify and analyze biological programs through automated reasoning. Nature Systems Biology and Applications, 2016.
2. Manna, Zohar, and Amir Pnueli. "Temporal verification of reactive systems: safety." Springer (1995). https://www.nature.com/articles/s41556-023-01131-x