עשר התקדמויות במתמטיקה ובמדעי המחשב התאורטיים

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

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

אנחנו מציגים תוצאות חדשות לבעיות הבאות. התוצאות הושגו באמצעות גרסה פנימית של Astra, המודל הגדול הבא שלנו. העלות הכוללת של הטוקנים שנדרשו למציאת פתרונות לבעיות הללו הייתה מסתכמת בכ-2,000 דולר לפי תעריפי ה-API של Sol. לאחר מכן, אנשים ערכו את הטיעונים הללו למאמרים בסיוע אותו מודל. בהמשך, המודל ניסח כל טיעון באופן פורמלי בתעודת הוכחה ב-Lean⁠(נפתח בחלון חדש). לכל פתרון אנחנו מפרסמים גם תיאור של תהליך החשיבה, כפי שנכתב בידי מודל.

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

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

3. חבורות לא-סופיות (non-sofic). בנייה המוכיחה את קיומן של חבורות לא-סופיות (non-sofic), ונותנת מענה לשאלה פתוחה מרכזית בתורת החבורות.

4. השערת הקשיחות של קון. הפרכת השערה ותיקה שלפיה חבורות מסוימות נקבעות באופן יחיד על ידי אלגברות פון נוימן שלהן.

5. סיבוכיות של מעגלים אריתמטיים. חסמים תחתונים חדשים לחישוב הפרמננט באמצעות מעגלים ונוסחאות אריתמטיים, ובהם חסם תחתון מסדר גודל n⁴/log n עבור נוסחאות אריתמטיות.

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

7. בעיית הווקטור הקרוב ביותר. קושי קירוב עד כדי גורם פולינומי לבעיית הווקטור הקרוב ביותר, שאלת יסוד בתורת הסריגים הקשורה לקריפטוגרפיה פוסט-קוונטית.

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

9. מספרי רמזי רב-צבעיים. חסם תחתון על-מעריכי למספרי רמזי רב-צבעיים של משולשים, הפותר את בעיית ארדש 183.

10. השערות על מספרים קיצוניים. תוצאות בנוגע להשערות הקומפקטיות והניוון בתורת הגרפים הקיצונית, הפותרות את בעיות ארדש 146 ו-180.

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

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