proofnet

מה זה

המאגר מכיל 371 דוגמאות מרמת תואר ראשון במתמטיקה עיונית, מתחומים כמו אלגברה לינארית ומופשטת, טופולוגיה, ואנליזה ממשית ומרוכבת. המקורות הם ספרי לימוד אקדמיים מוכרים, ללא פירוט ספציפי של שמות הספרים בכרטיס.

כל רשומה בנויה מארבעה שדות מרכזיים: מזהה ייחודי, ניסוח המשפט בשפה טבעית, הוכחה מלאה בשפה טבעית עם קוד לאטך, וניסוח המשפט בקוד של שפת ההוכחה לין שלוש. בנוסף יש שדה שמכיל את כותרת הקובץ הנדרשת כדי להריץ את הקוד, כולל ייבוא של הגדרות מקומיות. הנתונים מחולקים לקובצי ג'ייסון עבור אימות ומבחן.

מתאים ל

• בדיקת תרגום לשפה פורמלית

  מדידת הדיוק של מודל שמתרגם ניסוח של משפט מתמטי באנגלית לקוד לין שלוש.

• תרגום קוד לשפה טבעית

  בדיקה של יכולת המודל לקחת משפט פורמלי ולהסביר אותו במילים פשוטות באנגלית.

• הערכת מודלי שפה על מתמטיקה

  בנצ'מרק של הבנת מתמטיקה עיונית מורכבת ברמה של תואר ראשון.

איפה זה נופל

זה לא מאגר לאימון מודלים מאפס אלא מבחן ביצועים ממוקד מאוד וקטן עם שלוש מאות שבעים ואחת דוגמאות בלבד. כל הטקסטים וההוכחות כתובים באנגלית בלבד, ואין כאן עברית כלל. מעבר לזה, הקוד מבוסס על גרסה ישנה, לין שלוש, ולא על לין ארבע שהפכה לסטנדרט הנוכחי. שדה ההוכחה הפורמלית לא קיים פה, יש רק את ניסוח המשפט הפורמלי לצד הוכחה מילולית, מה שמגביל את סוג המשימות שאפשר לבדוק.

איך טוענים

אין צורך לבקש אישור גישה מיוחד כדי להוריד את הקבצים. המאגר כולל קובצי ג'ייסון אל וסקריפט טעינה בפייתון, כך שאפשר לקרוא אותם ישירות. כדי לבדוק או להריץ את הניסוחים המתמטיים, חובה להוריד ידנית קובץ הגדרות בשם קומון נקודה לין ולהניח אותו באותה תיקייה לצד הקוד שבודקים.

from datasets import load_dataset

ds = load_dataset("hoskinson-center/proofnet")

הרישיון

הרישיון הוא רישיון אם אי טי. מותר להשתמש בנתונים לצרכים מסחריים, לשנות אותם ולשלב אותם בפרויקטים סגורים או פתוחים, כל עוד שומרים על הודעת זכויות היוצרים של היוצרים המקוריים. אין חובה לשתף מודלים שתאמנו או מוצרים שתפתחו תחת אותו רישיון.

• שימוש מסחרי
• שינוי הקוד
• הפצה מחדש

הרישיון המלא ב־Hugging Face ↗