Nemotron-Math-Proofs-v2
קוד פתוחnvidiacc-by-4.02026-06-01
nvidia עומדים גם מאחורי NVIDIA AI, ויש עליו סקירה כאן.
המאגר כולל עקבות של הוכחות מתמטיות, אימותים ובדיקות אימות שנוצרו על בסיס בעיות מאתר AoPS. הוא מתאים למי שרוצה לאמן מודלים שגם מנמקים מתמטית וגם בודקים לעצמם את התוצאה צעד אחר צעד.
- 1,563הורדות בחודש
- 21לייקים
מה זה
המאגר מכיל 82,737 דוגמאות שנבנו סביב 5,752 בעיות מתמטיות ייחודיות שמקורן בקהילת AoPS, כפי שנאספו במקור בגרסה הקודמת של הפרויקט. הבעיות הן שאלות הוכחה באנגלית, ועבור כל אחת מהן יוצרו פתרונות ועקבות בדיקה באמצעות DeepSeek-V4-Pro במצב הסקה מקסימלי, לפי סגנון הפרומפטים של DeepSeekMath-V2.
כל המידע מרוכז בפיצול אימון יחיד המחולק לשלושה תתי-סוגים. יש בו 24,696 הוכחות, 28,865 בדיקות אימות שבוחנות את נכונות הטיעונים, ו־29,176 רשומות של מטא-אימות שמבקרות את תהליך הבדיקה עצמו. הרשומות מובנות במבנה שיחה סטנדרטי של משתמש ועוזר המיועד לאימון מודלי שפה.
מתאים ל
- אימון מודלים להוכחות
לימוד מודלי שפה לייצר הוכחות מתמטיות קפדניות צעד אחר צעד באנגלית.
- פיתוח מאמתי טיעונים
בניית מנגנוני ביקורת לזיהוי פערים וטעויות שלביות בהנמקה מתמטית.
- מחקר על הנמקה עצמית
בדיקת דיוק של מודלי אימות ומטא-אימות במערכות להוכחת משפטים.
איפה זה נופל
כל הטקסטים והבעיות במאגר הם באנגלית בלבד, כך שאימון עליו לא ילמד את המודל שלכם לנסח הוכחות או לבדוק אותן בעברית. בנוסף, מדובר בנתונים סינתטיים שנוצרו על ידי מודל שפה, ולא בהוכחות שנבדקו ישירות על ידי מומחה אנושי עבור כל פלט, כך שעלולים להסתנן כשלים לוגיים סמויים. המאגר גם לא כולל רשומות של עידון ותיקון הוכחות, אלא רק יצירה ואימות, ומבוסס כולו על סגנון הבעיות התחרותי של AoPS.
אותה משפחה
Nemotron-Math-Proofs יצא ב־2 גרסאות שיש להן עמוד כאן. אלה האחרות, לפי כמה מורידים אותן.
שאלות
נפוצות
האם מותר להשתמש במאגר לפיתוח מוצר מסחרי?
כן. המאגר מפורסם תחת רישיון CC BY 4.0 וכרטיס המאגר מציין במפורש שהוא מוכן לשימוש מסחרי ולא מסחרי. החובה היחידה שלכם היא לתת קרדיט הולם לבעלי המאגר.
האם יש במאגר נתונים בעברית?
לא. שפת המאגר המוגדרת היא אנגלית בלבד, וכל הבעיות מבוססות על שאלות שנלקחו מאתר AoPS. אם אתם מכוונים למערכת שמנמקת בעברית, תצטרכו לתרגם את המידע או להשתמש במקור אחר.
כמה מקום המאגר תופס בדיסק?
הגודל הכולל של הנתונים בדיסק הוא 15.95 GiB. הוא מורכב מ־82,737 דוגמאות המכילות יחד 5,000,839,123 טוקנים, ולכן הוא דורש משאבי חישוב וטעינה משמעותיים.
כיצד נוצרו ההוכחות והאימותים?
נקודת המוצא היא 5,752 בעיות מתמטיות שנאספו מקהילת AoPS עבור גרסה 1 של הדאטהסט. על בסיס השאלות האלו, המודל DeepSeek-V4-Pro ייצר באופן סינתטי הוכחות, עקבות אימות ועקבות מטא-אימות לפי שיטת הפרומפטים של DeepSeekMath-V2.
איך טוענים
הנתונים מגיעים בקובץ JSONL פתוח להורדה בשם data/train.jsonl ואינם דורשים אישור גישה מיוחד מ־NVIDIA. נפח הקובץ בדיסק הוא 15.95 GiB ומספר הטוקנים הכולל עומד על 5,000,839,123, כך שתצטרכו מקום אחסון ורוחב פס מתאימים. השדות החשובים לעבודה הם messages שמכיל את תוכן ההוכחות והבדיקות, ו־subset שמגדיר אם הדוגמה היא הוכחה, אימות או מטא-אימות.
from datasets import load_dataset
ds = load_dataset("nvidia/Nemotron-Math-Proofs-v2")הרישיון
המאגר מופץ תחת רישיון CC BY 4.0 שמתיר שימוש מסחרי ומחקר ללא תשלום תמלוגים. אתם רשאים לאמן עליו מודלים, לשנות את הנתונים ולשלב אותם במערכות שלכם, בתנאי שתתנו ייחוס מתאים ליוצרים כנדרש ברישיון. הרישיון אינו דורש שיתוף תחת אותו רישיון עבור תוצרים נגזרים.
- שימוש מסחרי
- שינוי הקוד
- חובת ייחוס