Astra של OpenAI פתר 10 בעיות מתמטיות פתוחות באימות Lean
מודל Astra של OpenAI פתר 10 בעיות פתוחות שעמדו עשור לפחות — מתורת החבורות ועד קריפטוגרפיית סריגים — באימות פורמלי מלא ב-Lean ובעלות כ-2,000 דולר.
OpenAI פרסמה ב-1 באוגוסט דוח שלפיו המודל הבא שלה, המכונה פנימית Astra, הפיק תוצאות חדשות בעשר בעיות מתמטיות פתוחות שמתמטיקאים לא הצליחו להתקדם בהן במשך עשור לפחות. המודל עדיין לא זמין לציבור, אבל הפתרונות כבר אומתו פורמלית ב-Lean, וזה בדיוק מה שהופך את הסיפור הזה לשונה מכל שיא בנצ'מארק שראינו עד כה.
מה בדיוק פתר Astra
לפי הדוח, עשר התוצאות משתרעות על פני תחומים שונים לחלוטין במתמטיקה: גאומטריה רב-ממדית, תורת הקודים, תורת החבורות, סיבוכיות קוונטית וקריפטוגרפיית סריגים. לא מדובר בשיפורים הדרגתיים של חסמים קיימים אלא בפתרונות מלאים לשאלות שנחשבו תקועות.
ההישג הבולט מכולם הוא בנייה מפורשת של חבורה לא-סופית (non-sofic group). השאלה האם קיימת חבורה כזו עמדה פתוחה מאז שמיכאיל גרומוב הגדיר את מושג הסופיות ב-1999, והעסיקה כמה מהחוקרים הבכירים בתורת החבורות הגאומטרית. Astra לא רק טען שקיימת חבורה כזו, אלא בנה אותה במפורש.
- 10 בעיות פתוחות שלא נרשמה בהן התקדמות במשך עשור לפחות
- פתרונות מלאים, לא שיפורים הדרגתיים, שאומתו פורמלית ב-Lean
- התוצאה המרכזית: חבורה לא-סופית, שאלה פתוחה מאז 1999
- עלות חישוב כוללת של כ-2,000 דולר לכל עשרת הפתרונות
- אף תוצאה טרם עברה ביקורת עמיתים מלאה
למה האימות ב-Lean משנה את כללי המשחק
עד היום, כשמודל שפה טען שפתר בעיה מתמטית, הדרך היחידה לוודא זאת הייתה שמתמטיקאי אנושי יעבור על ההוכחה שורה אחר שורה. מודלים ידועים כמייצרים הוכחות שנראות משכנעות אך מכילות פערים לוגיים. Lean, מערכת אימות פורמלית שבה כל צעד לוגי נבדק על ידי מחשב, סוגרת את הפרצה הזו: הוכחה שעוברת קומפילציה ב-Lean נכונה מתמטית, נקודה.
המשמעות היא ש-OpenAI לא מבקשת מאיתנו לסמוך על המודל. מי שרוצה יכול להריץ את הקוד ולבדוק בעצמו. עדיין נדרשת ביקורת עמיתים כדי לוודא שהניסוח הפורמלי אכן תואם את הבעיה המקורית כפי שהקהילה המתמטית מבינה אותה, וזה שלב שאף אחת מעשר התוצאות טרם עברה. אבל הפער בין 'המודל טוען' ל'המודל הוכיח' הצטמצם דרמטית.
ההבדל בין ציון גבוה בבנצ'מארק לבין הוכחה מאומתת ב-Lean הוא ההבדל בין תלמיד שמצטיין במבחן לבין חוקר שמפרסם תגלית. כאן חצו את הקו הזה
2,000 דולר לעשור של מתמטיקה תקועה
הנתון שאולי הכי קשה לעכל בדוח הוא העלות: כ-2,000 דולר של חישוב עבור כל עשרת הפתרונות יחד. לשם השוואה מחשבתית, כל אחת מהבעיות הללו העסיקה חוקרים ודוקטורנטים במשך שנים, עם עלויות מצטברות של משכורות, מענקים וכנסים שגבוהות בסדרי גודל.
אם היחס הזה בין עלות לתפוקה מחזיק מעמד גם בבעיות אחרות, מדובר בשינוי מבני באופן שבו מחקר מתמטי מתנהל: מתמטיקאים עשויים לעבור מתפקיד של מוכיחים לתפקיד של מנסחי בעיות, בודקי ניסוחים פורמליים ומפרשי תוצאות. השאלות הטובות הופכות למשאב היקר, לא ההוכחות.
חשוב לזכור: אף אחת מעשר התוצאות טרם עברה ביקורת עמיתים. האימות ב-Lean מבטיח שההוכחה תקפה לוגית, אבל הקהילה המתמטית עוד צריכה לוודא שהניסוח הפורמלי אכן לוכד את הבעיה המקורית. Astra עצמו גם אינו זמין לציבור, וללא תאריך השקה ידוע.
הזווית הישראלית: מקריפטוגרפיה ועד האקדמיה
לתוצאות יש נגיעה ישירה לישראל בכמה מישורים. ראשית, קריפטוגרפיית סריגים היא הבסיס לתקני ההצפנה הפוסט-קוונטיים שגם ארגונים ישראליים, מבנקים ועד מערכת הביטחון, נערכים לאמץ. מודל שמסוגל להפיק תוצאות חדשות דווקא בתחום הזה מחייב את קהילת הסייבר המקומית לעקוב מקרוב: אותה יכולת שמוכיחה משפטים יכולה באופן עקרוני גם לחשוף חולשות במבנים קריפטוגרפיים.
שנית, ישראל היא מעצמה יחסית בתורת החבורות הגאומטרית ובמתמטיקה תאורטית בכלל, עם קבוצות מחקר חזקות במכון ויצמן, בטכניון ובאוניברסיטאות המחקר. חוקרים ישראלים צפויים להיות בין הראשונים שיבחנו את ההוכחות הללו לעומק, והשאלה איך משלבים כלים כמו Astra בעבודת מחקר שוטפת תגיע לסמינרים בארץ מהר מאוד. לסטודנטים לתארים מתקדמים זו שאלה קיומית כמעט: אילו כישורים שווה לפתח כשמכונה פותרת בעיות פתוחות בעלות של ארוחת ערב זוגית בתל אביב.
מה הלאה
הצעד הבא הוא ביקורת עמיתים: מתמטיקאים יצטרכו לעבור על הניסוחים הפורמליים ולאשר שהם נאמנים לבעיות המקוריות. במקביל, יהיה מעניין לראות האם OpenAI תאפשר גישה ל-Astra לקבוצות מחקר אקדמיות, והאם מעבדות מתחרות יציגו יכולות דומות. אם התוצאות יחזיקו מעמד, אוגוסט 2026 עשוי להיזכר כרגע שבו AI עבר מלפתור מבחנים לייצר מדע.
שאלות נפוצות
מה זה Astra של OpenAI?
Astra הוא שם פנימי למודל הבא של OpenAI, שעדיין לא זמין לציבור. לפי דוח שפרסמה החברה ב-1 באוגוסט 2026, המודל הפיק פתרונות מלאים לעשר בעיות מתמטיות פתוחות שלא נרשמה בהן התקדמות במשך עשור לפחות.
איך יודעים שהפתרונות של Astra נכונים?
כל עשרת הפתרונות אומתו פורמלית במערכת Lean, שבודקת ממוחשבת כל צעד לוגי בהוכחה. עם זאת, התוצאות טרם עברו ביקורת עמיתים שתוודא שהניסוח הפורמלי תואם את הבעיות המקוריות.
כמה עלה ל-Astra לפתור את הבעיות המתמטיות?
לפי הדוח של OpenAI, עלות החישוב הכוללת לכל עשרת הפתרונות הייתה כ-2,000 דולר בלבד. זהו סכום זניח לעומת שנות עבודה של חוקרים שהבעיות הללו העסיקו.
דרגו את הכתבה
הדירוג עוזר לנו לדעת מה שווה לכם.
תגובות