proof-pile
קוד פתוחhoskinson-centerapache-2.02022-08-08
מאגר שמחבר טקסטים מתמטיים לא פורמליים לצד קוד הוכחות פורמלי. הוא מיועד למי שרוצה לאמן מודל שמבין מתמטיקה לעומק ולא רק מדקלם שאלות מילוליות.
- 2,353הורדות בחודש
- 68לייקים
מה זה
הנתונים מורכבים משני סוגי מקורות עיקריים: מתמטיקה לא פורמלית הכתובה באנגלית ובפורמט LaTeX, וספריות של הוכחות פורמליות. החלק הלא פורמלי כולל כעשרה ג'יגה בייט מתוך arXiv, לצד שניים וחצי ג'יגה בייט מקהילות Math Overflow ו־Math Stack Exchange, מאמרי ויקיפדיה, ספרי לימוד חופשיים ומאגר MATH. החלק הפורמלי שוקל כחצי ג'יגה בייט וכולל קוד בשפות הוכחה שונות כמו Lean 3, Isabelle, Coq, HOL Light, Metamath ו־Mizar.
הסינון משתנה לפי המקור. במאמרי arXiv שמרו רק קובצי tex באנגלית, זרקו קבצים עם גרפיקת gnuplot, חתכו ביבליוגרפיות והערות, והסירו טקסטים קצרים מ־280 תווים או כאלה שחסרי חלוקה לפרקים. בדיונים מתוך Stack Exchange השאירו אך ורק שאלות עם תשובה שקיבלו לפחות חמישה הצבעות חיוביות, וסידרו את השרשור בפורמט אחיד עם כמות ההצבעות של כל הודעה.
מתאים ל
- אימון מקדים להבנה מתמטית
לימוד מודל שפה על מאמרים ודיונים טכניים ב־LaTeX כדי לחזק יכולת פתרון בעיות כמותיות.
- הוכחת משפטים פורמלית
אימון מודלים לייצור קוד ובדיקת הוכחות בשפות מתמטיות קשיחות כמו Lean, Isabelle ו־Coq.
- חיפוש סמנטי במתמטיקה
בניית אינדקס לאיתור הגדרות ומשפטים מתוך ספריות קוד והסברים טקסטואליים חופשיים.
- אוטופורמליזציה
תרגום של ניסוחי משפטים מתמטיים מפסקה באנגלית ומבנה LaTeX לקוד הוכחה מובנה.
איפה זה נופל
אין כאן שום מילה בעברית, כל הטקסטים הרגילים הם באנגלית בלבד והשאר הוא קוד פורמלי. בנוסף, מי שבונה על הערכה מול NaturalProofs לא יכול להשתמש במאגר כי מקורות כמו ProofWiki ו־Stacks Project כבר נמצאים באימון ויובילו לדליפת נתונים. המאגר פורסם באוגוסט 2022, גרסת Lean שמורה על קומיט מסוים, ומאמרי arXiv סוננו לפי יוריסטיקות פשוטות שלא מנקות לחלוטין שגיאות קידוד או מבנים שבורים של LaTeX.
שאלות
נפוצות
האם המאגר מתאים לפרויקטים מסחריים?
הרישיון המדווח הוא apache-2.0, מה שמאפשר שימוש מסחרי באימון מודלים. עם זאת, התוכן מורכב מטקסטים שנאספו מאתרים כמו Stack Exchange, ויקיפדיה ו־arXiv. אם המוצר שלכם רגיש לזכויות יוצרים על נתוני האימון המקוריים, צריך לבדוק את תנאי המקורות האלה בנפרד.
כמה מקום צריך בשביל לעבוד איתו?
המאגר כולו שוקל 13 ג'יגה בייט ומכיל 8.3 מיליארד טוקנים לפי הטוקנייזר של gpt-neox. רוב הנפח מגיע ממאמרי arXiv שתופסים עשרה ג'יגה בייט, והשאר מתחלק בין דיונים ברשת לקוד הוכחות פורמלי.
האם יש במאגר תוכן בעברית?
אין במאגר עברית בכלל. כל הטקסט הלא פורמלי מסונן כך שיכלול אנגלית בלבד באמצעות כלי זיהוי שפה, ושאר הנתונים הם תחביר מתמטי או שפות תכנות ייעודיות להוכחות.
איך אפשר להעריך מודל שאומן על המאגר?
החוקרים שמרו פיצול ייעודי לבדיקה עבור Metamath והחליפו עשרה אחוזים מההוכחות בסימן שאלה. בנוסף, המאגר מכיל רק את סט האימון של MATH, ואפשר לבדוק ביצועים על הוכחות Lean שנוצרו אחרי קומיט 6313863 של mathlib.
איך טוענים
המאגר פתוח לחלוטין ואינו דורש אישור גישה מיוחד. בתוך המאגר ישנם 33 קבצים, כולל סקריפטים לטעינה כמו proof-pile.py וקבצי נתונים דחוסים בפורמט jsonl.gz המחולקים לפי פיצולים של פיתוח ובדיקה. כל רשומה כוללת את הטקסט המלא, אך חשוב לזכור שהנתונים מגיעים מכמה מערכות שונות לחלוטין, כך שהפורמט הפנימי של פוסט מפורום שונה מקובץ הוכחה של Lean או ממאמר מדעי.
from datasets import load_dataset
ds = load_dataset("hoskinson-center/proof-pile")הרישיון
המאגר מופץ תחת רישיון apache-2.0, שמתיר שימוש חופשי כולל אימון מודלים למטרות מסחריות, שינוי והפצה. החובה העיקרית היא מתן קרדיט ושמירה על תנאי הרישיון וכתבי הוויתור בקוד המקור. חשוב לזכור שהמאגר כולל ספריות וטקסטים שנאספו ממקורות שונים ברשת, כך שלמרות הגדרת החבילה הכוללת, האחריות על זכויות היוצרים של הטקסטים המקוריים נשארת אצלכם.
- שימוש מסחרי
- שינוי הקוד
- הפצה מחדש
- שימוש בפטנטים