סוכן הבינה המלאכותית של טנסנט פתר בעיה מתמטית בת 50 שנה

הסוכן שרץ 24 שעות והחזיר הוכחה

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

משקולות פתוחות, לא קוד פתוח

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

וריפיקציה ב-Lean 4 עם GPT-5.6 Sol

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

הגבול העליון אופטימלי, נקודה

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

מה זה אומר לפרקטיקה

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