NuminaMath-LEAN
קוד פתוחAI-MOapache-2.02025-07-31
מאגר של מאה אלף בעיות מתמטיות מתחרויות עם הצרנה בשפת לין 4. המטרה העיקרית שלו היא אימון והערכה של מודלים להוכחת משפטים פורמלית.
- 1,837הורדות בחודש
- 61לייקים
מה זה
המאגר מכיל בעיות שנלקחו מגרסה קודמת בשם נומינה מאת 1.5, בדגש על תחרויות ברמה גבוהה כמו אימו ויוסאמו. היוצרים ניקו ממנו שאלות פשוטות של בתי ספר וסיננו החוצה תחומים כמו גיאומטריה וקומבינטוריקה, פשוט כי קשה מאוד להצרין אותם בצורה אוטומטית או ידנית. בנוסף הם אספו ישירות מתוך מסמכי פי די אף רשמיים של תחרויות את תת המאגר אולימפיאדס רף, כדי לכלול ניסוחים ופתרונות מלאים.
בתוך הרשומות תמצאו את נוסח השאלה, התשובה הסופית, והצרנה של הטענה בלין 4 שנכתבה בסגנון מיני אף שתיים אף. חלק מההצרנות נכתבו בידי מודל אוטומטי וחלק בידי אדם, כשיש גם הוכחות מלאות, הוכחות חלקיות שמכילות פקודות סורי, והוכחות שהמודל שלהם הצליח לייצר בזמן אימון למידת חיזוק. הנתונים כוללים גם סטטיסטיקות על מספר הניסיונות של המודל ואחוזי ההצלחה שלו בכל בעיה.
מתאים ל
- אימון מוכיחי משפטים
אימון מודלים לייצור הוכחות פורמליות בלין 4 מתוך נוסח הבעיה וההצרנה שלה.
- הערכת ביצועי מודל
בדיקת יכולת הפתרון של מודלים מתמטיים מול טענות פורמליות ברמת אולימפיאדה.
- אימון בלמידת חיזוק
שימוש בנתוני שיעור ההצלחה של המודל המקורי כנקודת ייחוס לאימון מודלים חדשים.
איפה זה נופל
היוצרים מודים בכמה בעיות מהותיות שצריך לקחת בחשבון. קודם כל, חלק מהצרנות הטענות שגויות, בעיקר אלו שנוצרו על ידי המודל האוטומטי ולא עברו בדיקה אנושית מקיפה. בנוסף, ישנן בעיות שבהן חילוץ התשובה המקורית מהמסמכים בוצע בצורה שגויה, וחסרים נתוני מטא דאטה רבים בחלק מהרשומות, כמו סוג השאלה. אין כאן בכלל שאלות בגיאומטריה או בקומבינטוריקה, השפה היחידה שקיימת בטקסטים היא אנגלית, ואין עברית כלל.
שאלות
נפוצות
האם מותר להשתמש במאגר לפיתוח כלי מסחרי?
כן, הרישיון הוא אפאצ'י 2.0 ומאפשר שימוש מסחרי מלא. צריך רק לשמור על הקרדיט וההודעה המקורית של הרישיון. אין חובה לחשוף את המודל או את הקוד שפיתחתם באמצעותו.
האם יש במאגר שאלות בעברית או תמיכה בשפות אחרות?
לא, כל הבעיות וההסברים כתובים באנגלית בלבד. ההצרנה וההוכחות כתובות כולן בשפת לין 4. אין שום תוכן או מקורות בעברית.
האם כל ההוכחות במאגר מלאות ומוכחות רשמית?
ממש לא, וזה משהו שחייבים לבדוק לפי שדה הסטטוס. חלק מההוכחות כוללות פקודות שמדלגות על שלבים, חלקן מכילות רק את הטענה עצמה בלי הוכחה, ורק חלק נכתבו ואומתו במלואן על ידי בני אדם.
מה מבדיל אותו מנומינה מאת הרגיל?
נומינה מאת המקורי הכיל בעיקר מתמטיקה בטקסט חופשי ובשפות טבעיות, כולל בעיות פשוטות מסין. כאן לקחו רק בעיות קשות ברמת תחרויות בין לאומיות, הוציאו גיאומטריה וקומבינטוריקה, והמירו את הכל לקוד פורמלי שמתקמפל במחשב.
איך טוענים
המאגר מגיע כקובץ פארקט יחיד בתיקיית המידע, ללא צורך בהרשאה מיוחדת או באישור גישה ידני. כדי לעבוד איתו צריך לטעון אותו בעזרת ספריית דאטהסטס ולוודא מראש שסביבת העבודה שלכם מוגדרת בדיוק מול לין 4 וספריית מתליב בגרסה 4.15.0. ללא התאמת גרסה מדויקת, חלק גדול מהקוד וההוכחות פשוט לא יתקמפלו. השדות העיקריים שתרצו לבדוק הם פורמל סטייטמנט, גראונד טרות טייפ כדי לדעת אם ההוכחה שלמה, ושדה המחבר שמבדיל בין עבודה אנושית להצרנה של מודל.
from datasets import load_dataset
ds = load_dataset("AI-MO/NuminaMath-LEAN")הרישיון
המאגר מופץ תחת רישיון אפאצ'י 2.0. הרישיון הזה מתיר שימוש מסחרי, שינוי של הנתונים, ושילוב שלהם במוצרים סגורים, כל עוד שומרים על הודעת זכויות היוצרים ומצרפים עותק של הרישיון. מודל שתאמנו על המידע הזה יכול לשמש לפרויקטים מסחריים או פנימיים בלי שתחויבו לפתוח את הקוד שלכם.
- שימוש מסחרי
- שינוי הקוד
- הפצה מחדש
- שימוש בפטנטים