proof-pile-2
קוד פתוחEleutherAIרישיון לא דווח2023-10-12
מאגר ענק של 55 מיליארד טוקנים שמרכז טקסטים מתמטיים וקוד מדעי. מי שרוצה ללמד מודל שפה לפתור משוואות או לכתוב הוכחות פורמליות ימצא כאן את הבסיס הכי ממוקד שיש כרגע ברשת.
- 20,106הורדות בחודש
- 231לייקים
מה זה
המאגר מחולק לשלושה חלקים עיקריים שמרכיבים יחד את החומר שממנו אימנו את מודלי Llemma. החלק הראשון הוא תת המאגר של ArXiv מתוך RedPajama, שמכיל 29 מיליארד טוקנים של מאמרים מדעיים. החלק השני מגיע מתוך OpenWebMath, עם 15 מיליארד טוקנים של טקסט מתמטי שנאסף וסונן מרחבי האינטרנט, כולל ניקוי של מסמכים קצרים במיוחד בגרסה המעודכנת.
החלק השלישי הוא AlgebraicStack, מאגר חדש של 11 מיליארד טוקנים שמוקדש לקוד מתמטי ומדעי. הוא כולל חישובים נומריים, אלגברה ממוחשבת והוכחות פורמליות. הצוות סינן את הקוד באמצעות היוריסטיקות ייעודיות לכל שפת תכנות כדי להבטיח שרק קבצים עם תוכן מתמטי אמיתי ייכנסו פנימה. פייתון תופסת שם את הנתח הגדול ביותר עם מעל 6 מיליארד טוקנים, לצד שפות הוכחה כמו Isabelle, Lean ו־Coq, וקבצי TeX, Fortran ו־C++.
מתאים ל
- אימון מודלים להוכחות
אימון מקדים או המשך אימון של מודלי שפה לכתיבת הוכחות במערכות כמו Lean, Isabelle ו־Coq.
- פתרון בעיות מתמטיות
לימוד מודלים להבנה ופתרון של בעיות מדעיות מורכבות על בסיס טקסטים מאומתים מ־ArXiv.
- יצירת קוד מדעי
שיפור יכולות קידוד בספריות נומריות ואלגבריות בפייתון, C++, Julia ו־Fortran.
איפה זה נופל
המאגר כולו באנגלית ובשפות קוד, כך שאין בו שום תוכן בעברית או ייצוג למתמטיקה בשפות אחרות. הסינון של חלק הקוד נשען על היוריסטיקות ידניות, מה שאומר שחלק מהקבצים עלולים להכיל קוד כללי שלא באמת קשור למתמטיקה, או לפספס ספריות רלוונטיות שלא עמדו בכללים שהוגדרו. לפני שמשלבים את המידע באימון, חשוב לקחת בחשבון שהאיכות תלויה לחלוטין במקורות החיצוניים כמו מאמרי ArXiv ודפי אינטרנט ציבוריים, על כל הניסוחים והשגיאות שיכולים להופיע בהם במקור.
שאלות
נפוצות
האם מותר להשתמש במאגר לפיתוח מוצר מסחרי?
אין לכך תשובה חד משמעית כי המאגר לא מפורסם תחת רישיון כולל. היוצרים מצהירים שהם לא שינו את הרישיונות המקוריים של המקורות, מה שאומר שחלק מהחומרים עשויים להיות תחת מגבלות שימוש לא מסחריות או רישיונות קוד פתוח מגבילים. לחברות שרוצות לאמן מודל מסחרי מומלץ לבדוק את הרישיונות של כל מקור בנפרד.
האם יש במאגר טקסטים בעברית?
לא, המאגר מוגדר רשמית כמאגר בשפה האנגלית בלבד. כל המאמרים, דפי הרשת וההערות בקוד מבוססים על אנגלית לצד שפות תכנות ומערכות הוכחה פורמליות.
מה ההבדל בין המאגר הזה לבין RedPajama הרגיל?
המאגר הזה לוקח רק את חלק ה־ArXiv מתוך RedPajama, ומחבר אותו למאגר טקסט מתמטי מהרשת ולאוסף קוד ייעודי. התוצאה היא ריכוז גבוה של טקסטים וקוד מדעיים, לעומת תערובת טקסט כללית לאימון מודלים רחבים.
האם אפשר להוריד רק את הקוד בלי המאמרים?
כן, אפשר להשתמש בספריית הטעינה ולהעביר את שם תת המאגר שרוצים. במקום להוריד את כל 55 מיליארד הטוקנים, אפשר למשוך רק את algebraic-stack שמכיל את הקוד, או את arxiv בלבד.
איך טוענים
טוענים את המאגר דרך ספריית datasets בפקודת load_dataset רגילה של פייתון, בלי צורך בבקשת גישה מיוחדת. הנתונים שמורים בקובצי jsonl.zst דחוסים, כאשר כל רשומה כוללת שני שדות בלבד: text עם תוכן המסמך, ו־meta שמכיל מחרוזת JSON עם המטא-דאטה בהתאם למקור שממנו הרשומה נלקחה. אפשר להוריד את המאגר כולו או להגדיר תת מאגר ספציפי כמו arxiv כדי לחסוך זמן ואחסון.
from datasets import load_dataset
ds = load_dataset("EleutherAI/proof-pile-2")הרישיון
היוצרים לא הגדירו רישיון אחיד למאגר וציינו שהם לא משנים את תנאי הרישיון המקוריים של הנתונים שנאספו. המשמעות היא שאין פה היתר גורף לשימוש מסחרי. כל חלק, ממאמרי ArXiv דרך דפי הרשת ועד קוד המקור מפרויקטים שונים, כפוף לרישיון המקורי של מי שכתב אותו, ואי אפשר להניח שמותר לאמן עליו מוצר מסחרי בלי בדיקה משפטית של המקורות.