חברת הבינה המלאכותית Anthropic הציגה הישג בולט בתחום המתמטיקה הממוחשבת, לאחר שמערכת הבינה המלאכותית שלה, Claude, השלימה תהליך ניסוח מחדש ואימות אוטונומי מלא של הוכחת המשפט האחרון של פרמה. התהליך, שמומחים ומתמטיקאים מעריכים כי אמור היה להימשך מספר שנים בשיטות עבודה קודמות, הושלם על ידי מודל המחקר הפנימי של החברה בתוך 11 ימים בלבד של עבודה רציפה וכמעט ללא פיקוח אנושי.
תוצר העבודה של המודל הוא הוכחה ממוחשבת בהיקף של 13 מיליון שורות קוד, שנכתבו בשפת התכנות הייעודית Lean. מדובר בקוד מורכב הגדול פי חמישה ויותר מספריית ההוכחות המתמטיות המרכזית של הקהילה המדעית, Mathlib.
מנייר לקוד: ההמרה הממוחשבת של ההוכחה ההיסטורית
המשפט האחרון של פרמה הוצג לראשונה כהשערה מתמטית על ידי המתמטיקאי הצרפתי פייר דה פרמה בשנת 1637, ועמד פתוח במשך מאות שנים. רק בשנת 1995 הצליח המתמטיקאי אנדרו ויילס להציג לראשונה הוכחה מתמטית אנושית מלאה למשפט, אשר השתרעה על פני 129 עמודים.
משמעות המושג "פורמליזציה" (Formalization) של הוכחה מתמטית היא המרה מלאה של הטיעונים וההיגיון המתמטי לקוד מחשב בשפה פורמלית. תהליך זה מאפשר לתוכנת מחשב לבדוק ולאמת את תקפות ההוכחה באופן אוטומטי, באופן מוחלט וללא שום צורך בסיוע או בבדיקה של גורם אנושי.
לפני שהגיעה לפריצת הדרך הנוכחית, ביצעה Anthropic מספר ניסיונות קודמים להשגת הפורמליזציה של המשפט. ניסיונות מוקדמים אלו לא ירדו לטמיון, והם תרמו בסופו של דבר כ-7% משורות הקוד הפעילות (בניכוי קוד תבניתי אוטומטי) שנכללו בהוכחה הסופית שנכתבה.
11 ימים, 30,000 משפטים והנחיה אנושית מוגבלת
העבודה האוטונומית של Claude נמשכה 11 ימים ברציפות. לאורך כל פרק הזמן הזה, המעורבות האנושית בתהליך הייתה מוגבלת למתן הנחיות כלליות ברמת מקרו בלבד, ללא כתיבת קוד ישירה או התערבות תכנותית מעשית מצד החוקרים.
במהלך ימי העבודה, סוכני הבינה המלאכותית של המודל הוכיחו באופן עצמאי כ-30,300 משפטי משנה נפרדים (Theorems). מתוך סך המשפטים הללו, בחר המודל לשלב ולהשתמש ב-29,500 משפטים בגרסה הסופית והמלאה של ההוכחה.
בחברה הסבירו כי ההצלחה הושגה לאחר שניתנה ל-Claude גישה לתוכנת קוד פתוח בשם Prove2Me, אשר פותחה על ידי שותפים ומשתפי פעולה חיצוניים. תוכנה זו מסייעת לסוכני ה-AI לבחור את הצעד הבא והיעיל ביותר במהלך זרימת עבודה מחקרית מורכבת ורב-שלבית, ובמקביל תורמת לצמצום עלויות החישוב של המודל.
"הישג האוטו-פורמליזציה היוצא מן הכלל הזה... מוכיח את המשפט האחרון של פרמה ללא הנחות מלבד האקסיומות של המתמטיקה", אמר קווין באזארד, מתמטיקאי מאימפריאל קולג' בלונדון. "לאורך הדרך אנו רואים אוטו-פורמליזציה של אלגברה, אנליזה הרמונית, גיאומטריה ותורת המספרים, ואנו לומדים שתוצרי האוטו-פורמליזציה של בינה מלאכותית יציבים כעת מספיק כדי לבנות עליהם; ההוכחה היא רב-שכבתית."
התרחבות המרוץ לפיתוח מתמטיקה באמצעות AI
השלמת הפורמליזציה של משפט פרמה מגיעה חודש בלבד לאחר ש-Anthropic פרסמה פרטים על פריצת דרך נפרדת שביצעה, אשר נגעה לפונקציית הזטא של רימן (Riemann zeta function). פונקציה זו עומדת במרכזה של השערת רימן, שנחשבת לאחת הבעיות המתמטיות הבלתי פתורות הקשות ביותר בעולם.
התחרות בתחום זה הולכת ומתהדקת: גם מעבדת הבינה המלאכותית המתחרה, OpenAI, משקיעה מאמצים דומים בפתרון בעיות מתמטיות מורכבות. OpenAI משתמשת במודל החדש שלה, Astra, כדי לפתור מספר בעיות קלאסיות שהציב המתמטיקאי פול ארדש (Erdős problems), ולפי דיווחים הצליחה לצמצם שאלות פתוחות וותיקות בתחום מדעי המחשב התיאורטיים.
בעקבות ההישג, הודיעה Anthropic כי היא מרחיבה את הגישה החינמית ואת קרדיטי המחקר הניתנים למתמטיקאים העוסקים בפרויקטים של פורמליזציה, לצד מענקים כספיים מוגדלים בתחום. לצד זאת, בחברה הדגישו כי פרק הזמן בן 11 הימים מראה כי תהליך פורמליזציה מלא נותר משימה עתירת עבודה ומשאבים, גם כאשר עושים שימוש במערכות הבינה המלאכותית המתקדמות ביותר שקיימות כיום.
למה זה חשוב לך
הישג כזה מראה עד כמה בינה מלאכותית יכולה לקצר תהליכי מחקר מדעי ומתמטי מורכבים, מה שעשוי להשפיע גם על תעשיות ישראליות מבוססות מו"פ, כמו הייטק, סייבר וביומד, הנשענות על יסודות מתמטיים ואלגוריתמיים. לחברות ולחוקרים ישראלים המתחרים בזירה הגלובלית, קצב ההתפתחות הזה מדגיש את הצורך להשתלב מוקדם בכלים דומים כדי לא להישאר מאחור. בנוסף, כלים כמו Lean ו-Prove2Me עשויים בעתיד לסייע גם לסטארטאפים מקומיים בתחומי האבטחה והפורמליזציה של קוד קריטי.
התוכן בכתבה זו נועד לספק סקירה כללית בלבד ואינו מהווה תחליף לייעוץ מקצועי פרטני. המערכת אינה אחראית לכל נזק או הפסד שייגרם כתוצאה מהסתמכות על המידע המוצג.
קראו גם: מרוץ ה-AI מעלה הילוך: Crusoe מגייסת 3.9 מיליארד דולר לתשתיות מחשוב · מיקרוסופט משחררת בקוד פתוח את TauGrid: פלטפורמה אחודה לניהול עומסי AI בקוברנטיס
