OpenAI פרסמה ב-6 באוקטובר מאגר ציבורי ב-GitHub עם 722 כתבי יד מתמטיים שנוצרו על ידי מודל פנימי שאינו זמין לציבור. החומר מאורגן ב-372 משפחות תוצאות ומופץ ברישיון Apache-2.0.
לפי ה-README של המאגר, המודל קיבל כ-4,000 בעיות, ו-OpenAI בחרה את הפלטים שהעריכה כמשמעותיים. לחלק מהתוצאות מצורפות הוכחות פורמליות ב-Lean וסיכומים מקוצרים של דרך החשיבה של המודל.
הסייג המרכזי: לא לכל כתב יד יש הוכחת Lean, ו-OpenAI עצמה מזהירה שתוצאות ללא פורמליזציה עלולות להכיל שגיאות. לא נמסרה הערכה בלתי תלויה של נכונות האוסף כולו, ומתמטיקאים עדיין יצטרכו לבדוק אותו. החברה מתייעצת עם קבוצת הייעוץ למתמטיקה ובינה מלאכותית ב-Institute for Advanced Study לגבי אופן השיתוף.
₿ אהבת את הפוסט?
אפשר לשלוח לי ביטקוין ישירות לכתובת שלי. סרקו את הקוד, או העתיקו את הכתובת:
bc1qsn043qmlv4ejxydeknkfm9u6e93e6tegmq9x85
שימו לב: העברה on-chain כרוכה בעמלת רשת שאינה תלויה בסכום, ולכן סכומים קטנים מאוד אינם כדאיים.
