Lean-Github

מה זה

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

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

מתאים ל

• אימון מודלים להוכחה פורמלית

  אימון או כוונון עדין של מודלי שפה על קוד Lean 4 אמיתי שעבר הידור.

• השלמת צעדי הוכחה ב־Lean

  בניית מנוע עזר שמציע את הטקטיקה הבאה בהוכחת משפטים מתמטיים.

• הערכת יכולות הסקה מתמטית

  בדיקת הדיוק של מודלים קיימים בכתיבת הוכחות פורמליות מתוך מאגר מגוון.

איפה זה נופל

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

איך טוענים

טוענים את הקובץ ישירות דרך ספריית datasets באמצעות המזהה internlm/Lean-Github. הנתונים שמורים בקובץ lean-github.parquet, ללא צורך בהרשאת גישה מיוחדת או באישור ידני. מכיוון שהכרטיס לא מפרט את שמות השדות המדויקים, צריך לטעון דגימה ראשונה ולבדוק את מבנה העמודות לפני שמתחילים לכתוב פייפליין אימון מלא.

from datasets import load_dataset

ds = load_dataset("internlm/Lean-Github")

הרישיון

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

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

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