קלוד השלים את הפורמליזציה הראשונה של המשפט האחרון של פרמה

אנת'רופיק הודיעה ב-4 בספטמבר שקלוד השלים את הפורמליזציה הממוחשבת המלאה הראשונה של המשפט האחרון של פרמה: 13 מיליון שורות קוד Lean שנכתבו ב-11 ימים בלבד, ברובן באופן אוטונומי לחלוטין. הקהילה המתמטית העריכה שמשימה כזו תדרוש שנים של עבודה אנושית מתואמת. בדרך הוכיח המודל 29,500 משפטים מתמטיים ביניים.

01מה בדיוק קרה, ומה לא קרה

נתחיל בהבהרה חשובה: קלוד לא גילה מתמטיקה חדשה ולא פתר בעיה פתוחה. המשפט האחרון של פרמה, החידה שהמתינה 358 שנים לפתרון, הוכח על ידי אנדרו ויילס עוד ב-1995. מה שקלוד עשה הוא משהו אחר: הוא תרגם את ההוכחה, על כל שרשרת הטיעונים המורכבת שלה, לקוד פורמלי בשפת Lean, כך שמחשב יכול לאמת כל צעד וצעד ללא שום הסתמכות על אמון בבני אדם.

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

02למה מתמטיקאים דווקא נרגשים

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

• אימות בקנה מידה: ספרות מתמטית שלמה יכולה לעבור בדיקת מכונה במקום להסתמך על סוקרים אנושיים עמוסים
• רשת ביטחון להוכחות AI: כשמודלים מייצרים הוכחות חדשות, פורמליזציה היא הדרך היחידה לסמוך עליהן
• תשתית לעתיד: 29,500 המשפטים שהוכחו בדרך הופכים ללבנים שאפשר לבנות עליהן פרויקטים הבאים
• תקדים לסוכנים ארוכי טווח: הוכחה שמודל מסוגל לנהל פרויקט הנדסי ענק לאורך ימים כמעט ללא פיקוח

03מעבר למתמטיקה: אבן דרך לסוכנים אוטונומיים

הסיפור הזה הוא לא רק חדשות למתמטיקאים. 13 מיליון שורות קוד שנכתבות, נבדקות ומתוקנות באופן אוטונומי לאורך 11 ימים הן הדגמה חיה של מה שהתעשייה מכנה long-horizon agency: היכולת של מודל להחזיק משימה מורכבת לאורך זמן, להתאושש מכישלונות ולשמור על קוהרנטיות. וכאן יש יתרון מבני לעולם ההוכחות: מאמת ה-Lean נותן למודל פידבק בינארי ומיידי על כל צעד, כך שאין מקום להזיות. או שההוכחה עוברת קומפילציה, או שלא.

04הזווית הישראלית: מה לומדים מזה בהייטק המקומי

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

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

05מה הלאה

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