מיקרוסופט מציגה את EuClean: צעד חשוב לאיחוד הוכחות מתמטיות, בינה מלאכותית וגיאומטריה
מחקר חדש של Microsoft Research מציג מסגרת לאוטומציה של ניסוח בעיות גיאומטריה בתוך Lean ו-mathlib. מעבר להישג הטכני, EuClean מסמן כיוון אסטרטגי חשוב: בניית מערכות AI המסוגלות לחשוב מתמטית בסביבה מאומתת, אחידה וניתנת להרחבה.
למה גיאומטריה עדיין קשה לבינה מלאכותית
בשנים האחרונות מערכות היסק פורמלי החלו להתקרב לרמות ביצוע שבעבר נחשבו נחלתם של מתמטיקאים מצטיינים בלבד, כולל פתרון בעיות ברמת אולימפיאדה. אבל מאחורי ההתקדמות המרשימה מסתתרת בעיה תשתיתית: תחומי מתמטיקה שונים מיוצגים בכלים שונים. אלגברה ותורת המספרים נשענות יותר ויותר על Lean ועל ספריית mathlib, בעוד שגיאומטריה נוטה להישען על שפות ייעודיות, בודקי תקפות חיצוניים ומערכות אקסיומות שאינן תמיד משתלבות עם הסטנדרט הרחב של עולם ההוכחות הפורמליות.
רוצה להישאר מעודכן ב-AI?
הירשם לדיוור השבועי שלנו וקבל עדכונים, המלצות על כלים, חדשות ודוחות מיוחדים
לפי דף הפרסום של Microsoft Research, המסגרת החדשה EuClean נועדה לשבור את הפיצול הזה באמצעות ניסוח אוטומטי של בעיות גיאומטריה ישירות בתוך Lean ובתוך mathlib. המשמעות אינה רק תרגום טכני של משפטים לשפה פורמלית, אלא ניסיון לבנות שכבת אמון אחידה שבה גם הבעיה, גם ההנחות וגם ההוכחה חיות באותו מרחב מתמטי מאומת.
מה EuClean עושה אחרת
הקושי המרכזי בגיאומטריה הוא שהרבה מהמידע נמצא בתרשים ולא בטקסט. תלמיד או מתמטיקאי מבין באופן כמעט מיידי שנקודות אינן חופפות, שקווים נחתכים בסדר מסוים, או שמשולש אינו מנוון. מערכת פורמלית, לעומת זאת, אינה מניחה דבר. אם ההנחות הללו אינן נכתבות במפורש, ההוכחה עלולה להיות חסרת בסיס.
EuClean מטפלת בכך באמצעות תהליך רב שלבי: חשיפת אילוצים סמויים, עיגון התצורה הגיאומטרית, מיפוי למבנים הקיימים ב-mathlib ותיקון איטרטיבי של ניסוחים שגויים. זו נקודה קריטית, משום ש-mathlib אינה ספריית גיאומטריה ייעודית בלבד, אלא תשתית מתמטית כללית המתפתחת במהירות. התאמה אליה דורשת הבנה עמוקה של האופן שבו מתמטיקה מודרנית מיוצגת בקוד.
החוקרים בנו שני מאגרים משמעותיים: OMNI-Geometry עם 768 בעיות תחרותיות, ו-Numina-Geometry עם 177,597 בעיות. בקנה המידה של הוכחות פורמליות, מדובר בקפיצה גדולה במיוחד. מערכי נתונים קודמים בתחום הגיאומטריה ב-Lean היו קטנים בהרבה, ולכן התאימו פחות לאימון מודלים עצביים גדולים.
ההשלכה העסקית והטכנולוגית
הנתון המעניין ביותר אינו רק דיוק הניסוח האנושי, שהגיע ל-48.89 אחוז ב-TOP1 ול-73.33 אחוז ב-TOP5, אלא השיפור באימון מודל Goedel v2: שיעור הצלחת ההוכחות עלה מ-13.6 אחוז ל-15.1 אחוז. זה אולי נשמע שיפור מתון, אך בתחום ההוכחה הפורמלית כל עלייה עקבית מצביעה על איכות נתונים גבוהה ועל פוטנציאל להרחבה.
עבור תעשיית ה-AI, EuClean מייצגת מעבר חשוב ממודלים שמייצרים תשובות משכנעות למודלים שמסוגלים לפעול בתוך מערכות אימות קשיחות. בטווח הארוך, אותה גישה עשויה להשפיע לא רק על מתמטיקה, אלא גם על אימות תוכנה, תכנון שבבים, בטיחות מערכות אוטונומיות ופיתוח הנדסי שבו טעות לוגית אחת עלולה לעלות מיליונים.
מעבר ממבחני ראווה לתשתית אמון
המרוץ סביב AI מתמטי אינו עוסק רק בפתרון חידות אולימפיאדה. הוא עוסק בשאלה רחבה הרבה יותר: האם ניתן לבנות מערכות שמסבירות, מוכיחות ומוודאות את עצמן באופן שניתן לבדיקה. EuClean אינה פותרת את הבעיה כולה, אך היא מצמצמת את הפער בין אינטואיציה גיאומטרית אנושית לבין פורמליזם מכונה. אם מגמה זו תימשך, Lean עשויה להפוך לאחת התשתיות המרכזיות של הדור הבא של בינה מלאכותית אמינה.