doubleAI שיפרה חסם בן 38 שנה — אבל ההוכחה עדיין חייבת ביקורת

ב דיווח CTech מ־8 באוקטובר 2026 תוארה טענתה של doubleAI לשיפור הראשון זה 38 שנה בחסם בתורת הגרפים: מערכת Double Agent בנתה, לדברי החברה, משפחה של גרפים רגולריים שמעלה את מקדם ה־girth מ־4/3 ל־8/5. החברה הציגה גם הוכחה שנוסחה ב־Lean. פרסום הבנייה וההוכחה מאפשר לבחון את הטענה, אך עדיין אינו שקול לקבלתה כתוצאה מוסכמת בקהילה המתמטית.

ב הצגת התוצאה של doubleAI מופיע החסם 8/5 כפול הלוגריתם של מספר הקודקודים בבסיס התלוי בדרגת הגרף, ולצדו הפניות למאמר ולהוכחת Lean. החברה מייחסת ל־Double Agent את מציאת הבנייה עצמה, ולא רק את ניסוח ההוכחה. השאלה המכרעת כעת היא אם הגדרות המשפט הפורמלי, תנאי הבנייה וההסבר המתמטי מתארים בדיוק את אותו שיפור.

השיפור נוגע למחזור הקצר ביותר בגרף

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

המספרים 4/3 ו־8/5 הם מקדמים של גודל לוגריתמי, ולכן ההשוואה ביניהם דורשת לשמור על אותם תנאים לגבי דרגת הגרף וגודלו. במונחים חשבוניים, המעבר מ־4/3 ל־8/5 מגדיל את המקדם בחמישית. הוא אינו אומר שכל גרף קיים קיבל מחזור ארוך יותר. המשמעות היא שלפי הבנייה החדשה אפשר להבטיח למשפחות המתאימות חסם טוב יותר מזה שהושג בבניות המפורשות הקודמות.

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

מה בודקת הוכחת Lean

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

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

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

הוויכוח על תוצאות OpenAI מחדד את הדרישה לביקורת

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

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

המבחן הבא של הבנייה

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

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

קראו גם:

• Revolut מגייסת בישראל לתפקידי אשראי — אבל מועד ההשקה עדיין חסר
• Dots של OpenAI עובדים בין השיחות — ההשקה עדיין מוגבלת
• Gemini מתחבר ל־monday.com — אבל כרגע הוא רק קורא