חוויות ביצירת הוכחות פורמליות עם LLMs

▶︎ נושא: חוויות ביצירת הוכחות פורמליות עם LLMsבשנים האחרונות, AI/LLM התפתח במהירות, כשיש לו יכולת לייצר לא רק טקסט ודימויים אלא גם קוד יציב. לפני כמה חודשים, מודלים מתקדמים כמו GPT 5.4 ו-Claude Opus 4.6 החלו לייצר הוכחות מתמטיות פורמליות יחסית מורכבות, אפילו עבור תיקונים מורכבים של ייצוג ביניים של קומפיילר, פשוט על ידי מתן "תבנית" הוכחה דומה ליצירת הוכחות פורמליות בצורה מתאימה.בהרצאה זו נחקור את החוויה של שימוש ב-GPT 5 סדרה ואגדא לכתיבת תוכניות עם סוגים תלויים ולהוכחות המשפטים הפורמליים, מדגימים כיצד מודלי השפה, באמצעות האמצעים של מוכיחי משפטים, מייצרים הוכחות מתמטיות מדויקות של כשירות שהן כמעט ללא פגם.▶︎ מציג: צ'ן ליאנג-טינג, חוקר משלים באקדמיה סיניקה, נהנה לנסות דברים חדשים. תחומי העניין האחרונים שלו כוללים תיאוריה של סוגים, מודלים קטגוריאליים, והוכחות עם משמעות חישובית.*האירוע הפעם מתחיל מוקדם יותר! הוא מתחיל בשעה שבע!----------------האירוע חינם, וכל תרומה למקום g0v מתקבלת בברכה. פשוט תיכנסו.אתם מוזמנים להגיע ל交流、交朋友！