Nemotron-Math-Proofs-v1
קוד פתוחnvidiacc-by-sa-4.02025-12-14
nvidia עומדים גם מאחורי NVIDIA AI, ויש עליו סקירה כאן.
מאגר ענק של הוכחות מתמטיות בשפה טבעית ובשפת Lean 4. הוא מתאים למי שמאמן מודלים להוכחת משפטים פורמלית וצריך פתרונות שעברו הידור אמיתי.
- 821הורדות בחודש
- 125לייקים
מה זה
המאגר מכיל כ־580 אלף בעיות מתמטיות מילוליות שנאספו מקהילות AoPS, Math StackExchange ו־MathOverflow. הצוות של אנבידיה סינן כ־40% מהחומר המקורי באמצעות הסרת כפילויות סמנטיות ומניעת זליגה של מבחני ביצועים מקובלים. מתוך הבעיות האלה תורגמו כ־550 אלף משפטים לקוד Lean 4 בעזרת מודל ייעודי, ונבחנו בלולאות בדיקה של הידור ותרגום חוזר לאנגלית עם שיפוט אוטומטי.
בנוסף נוצרו כ־900 אלף מסלולי חשיבה ופתרונות מלאים באמצעות המודל Goedel-Prover-V2-32B. כל פתרון עבר בדיקה מול המהדר של Lean 4, תוך סבבי תיקון עצמי שבהם שגיאות המהדר הוזנו חזרה למודל כדי שישפר את הקוד עד שהוא מתקמפל ללא שימוש בהנחות עזר ריקות.
מתאים ל
- אימון מודלי שפה ל־Lean 4
לימוד מודלים לכתוב הוכחות פורמליות מלאות שעוברות קומפילציה תקינה.
- פיתוח מנגנוני תיקון שגיאות
אימון מערכות שמקבלות משוב ממהדר ומתקנות קוד פגום על בסיס הודעות השגיאה.
- מחקר על תרגום פורמלי
בדיקת שיטות להמרת מתמטיקה חופשית באנגלית למבנים מדויקים של משפטים לוגיים.
איפה זה נופל
אין כאן איזון ברמת הקושי של התרגילים, והמאגר כולו מוטה לכיוון בעיות שהמודלים הצליחו לתרגם ולקמפל בהצלחה. חלק מההוכחות מכילות שורות מיותרות או אזהרות מהדר על משתנים שלא נעשה בהם שימוש. יש גם מקרים שבהם המודל השתמש בהגדרות טריוויאליות ריקות כדי לעקוף את ההוכחה במקום להסתמך על הספרייה המתמטית הרשמית, כך שחובה לסנן את החומר לפי אקסיומות הבסיס לפני שמסתמכים עליו.
אותה משפחה
Nemotron-Math-Proofs יצא ב־2 גרסאות שיש להן עמוד כאן. אלה האחרות, לפי כמה מורידים אותן.
שאלות
נפוצות
האם מותר להשתמש במאגר לפיתוח מוצר מסחרי?
כן, הרישיון מתיר שימוש מסחרי מפורש. יחד עם זאת, סעיף ה־ShareAlike מחייב שכל נגזרת תופץ תחת אותו הרישיון, מה שעשוי להגביל שימוש במודלים סגורים.
האם יש במאגר שאלות או הוכחות בעברית?
לא. כל הבעיות המתמטיות כתובות באנגלית, וההוכחות הפורמליות כתובות בקוד Lean 4 בלבד.
כמה מקום בדיסק צריך בשביל לעבוד איתו?
נפח האחסון הכולל של המאגר הוא כ־28 גיגה בייט. הקבצים מגיעים במבנה JSONL רגיל.
איך אנבידיה וידאה שההוכחות נכונות?
כל הוכחה עברה הידור בסביבת ריצה מבודדת של Lean 4. המערכת פסלה הוכחות עם שגיאות או כאלה שהשתמשו במילות מפתח שמדלגות על הוכחה מלאה.
איך טוענים
הנתונים מגיעים בקובץ JSONL יחיד בשם data/lean.jsonl, שתופס כ־28 גיגה בייט בדיסק. אין צורך לבקש אישור גישה מיוחד כדי להוריד אותו מ־Hugging Face. הרשומות כוללות את שדות הבעיה המקורית, מקור השאלה, הצהרת המשפט הפורמלית, והיסטוריית ההודעות שמכילה את ניסיונות ההוכחה המוצלחים בפורמט שיחה.
from datasets import load_dataset
ds = load_dataset("nvidia/Nemotron-Math-Proofs-v1")הרישיון
המאגר מופץ ברישיון CC BY-SA 4.0 שמתיר שימוש מסחרי, אך דורש מתן קרדיט ושיתוף של כל יצירה נגזרת תחת אותו הרישיון בדיוק. אימון מודל עלול לחייב אתכם לשחרר את משקולות המודל או את הנתונים המעובדים תחת אותו רישיון פתוח.
- שימוש מסחרי
- שינוי הקוד
- חובת שיתוף באותו רישיון