במחקר חדש שהובילה קבוצת חוקרים מאוניברסיטת פקינג בסין נטען כי מערכת בינה מלאכותית הצליחה לפתור באופן עצמאי בעיה מתמטית פתוחה שהוצגה לראשונה בשנת 2014 על ידי המתמטיקאי האמריקאי דן אנדרסון.
לפי הדיווח שפורסם בעיתון סאות׳ צ׳יינה מורנינג פוסט, מדובר בצעד משמעותי בדרך לאוטומציה של מחקר מתמטי.
החוקרים ציינו כי המערכת פעלה כמעט ללא התערבות אנושית, תוך ניתוח עשרות שנות מחקר ושילוב בין חשיבה בשפה טבעית לבין אימות פורמלי של הוכחות. לדבריהם, “המערכת הצליחה לפתור בעיה פתוחה באלגברה קומוטטיבית ולנסח את ההוכחה באופן פורמלי כמעט ללא התערבות אנושית”.
המערכת מבוססת על שני רכיבי בינה מלאכותית: סוכן לחשיבה לא פורמלית בשם “רתלאס”, שמייצר אסטרטגיות והוכחות אפשריות, וסוכן לאימות פורמלי בשם “ארכון”, שממיר את ההוכחות לגרסה מתמטית מדויקת באמצעות כלים כמו לין 4. החוקרים ציינו כי “השילוב בין חשיבה אינטואיטיבית לאימות פורמלי מאפשר פתרון יעיל של בעיות מתמטיות אמיתיות”.
לפי המאמר, הבינה המלאכותית אף ביצעה משימות במהירות גבוהה מזו של מתמטיקאים אנושיים, כולל כאלה שבדרך כלל דורשות שיתוף פעולה בין מומחים. עם זאת הודגש כי “דיוק מוחלט הוא קריטי, והוכחות של בינה מלאכותית עדיין עלולות להכיל טעויות”, ולכן פיקוח אנושי נותר חשוב. החוקרים הוסיפו כי “הכוונה של מתמטיקאי יכולה להאיץ את התהליך”, אף שהמערכת מסוגלת לפעול גם לבדה.
הפתרון המלא, כולל האימות הפורמלי, הושלם בתוך כ־80 שעות, כאשר תפקיד האדם הצטמצם בעיקר לגישה לקבצים חיצוניים. החוקרים מסכמים כי “העבודה שלנו מדגימה כיצד ניתן לפתור חלקים משמעותיים מהמחקר המתמטי באמצעות בינה מלאכותית”.
0 תגובות