Lean-Workbook
קוד פתוחinternlmapache-2.02024-06-06
המאגר מרכז בעיות מתמטיות מתחרויות שעברו פורמליזציה לשפת לין 4. הוא מתאים למי שבונה מודלים להוכחת משפטים אוטומטית או תרגום ממתמטיקה מילולית לקוד פורמלי.
- 3,387הורדות בחודש
- 58לייקים
מה זה
בפנים יש בעיות מתמטיקה ברמת תחרויות, כאשר כל רשומה כוללת את הניסוח המילולי בשפה טבעית, את התשובה הסופית, את הניסוח הפורמלי בלין 4, וגם הוכחה פורמלית מלאה אם היא קיימת.
הנתונים מחולקים לשני חלקים עיקריים. החלק הראשון נקרא לין וורקבוק וכולל 57,231 בעיות. החלק השני נקרא לין וורקבוק פלוס והוא מרחיב את האוסף ל־82,893 בעיות. מעבר לציון העובדה שמדובר בשאלות מתחרות, כרטיס המאגר לא מפרט באילו תחרויות מדובר, מהיכן בדיוק נאספו הטקסטים המקוריים, או באיזה אופן בוצע הסינון והתרגום לפורמט הפורמלי.
מתאים ל
- אימון תרגום פורמלי
לימוד מודלים לתרגם שאלות מילוליות במתמטיקה לקוד מוגדר היטב בלין 4.
- חיפוש הוכחות אוטומטי
אימון והערכה של סוכנים שמנסים לייצר הוכחות מתמטיות שלמות באופן עצמאי.
- מבחן ביצועים למודלי שפה
בדיקת יכולת ההסקה הלוגית והדיוק התחבירי של מודלים מול שפת הוכחה קשיחה.
איפה זה נופל
המאגר כולו באנגלית ובשפת לין 4, כך שאין כאן שום תוכן בעברית או תמיכה בריבוי שפות. הוכחות פורמליות לא קיימות עבור כל הרשומות אלא רק בחלקן, והכרטיס לא מציין לכמה בעיות באמת הוצמדה הוכחה מלאה. בנוסף, חסר פירוט על שיטת איסוף הבעיות ועל אימות הנכונות שלהן, והתלות בגרסה ספציפית מאוד של לין ומתליב עלולה להכשיל הידור מול גרסאות חדשות יותר.
שאלות
נפוצות
האם מותר להשתמש במאגר לפיתוח מוצר מסחרי?
כן, הרישיון שדווח הוא אפאצ'י 2.0 שאינו מגביל שימוש מסחרי. מותר לאמן מודלים, לשלב אותם במערכות מסחריות ולהפיץ תוצרים, כל עוד מקפידים על מתן הקרדיט הנדרש.
האם כל בעיה במאגר כוללת הוכחה מלאה?
לא. לפי הכרטיס, הוכחה פורמלית מסופקת רק אם היא הייתה זמינה עבור אותה בעיה. חלק גדול מהרשומות כולל רק את ניסוח השאלה והטענה הפורמלית ללא הוכחה.
האם יש במאגר שאלות או הסברים בעברית?
לא, המאגר מסומן כשפה אנגלית בלבד לצד קוד לין 4. אין בו תרגום לעברית או נתונים מתמטיים מקומיים.
באילו גרסאות של לין השתמשו המפתחים?
הבדיקות של יוצרי המאגר נערכו מול גרסת לין v4.8.0-rc1 יחד עם גרסה תואמת של מתליב 4. אם תריצו את הקוד על גרסאות שונות, ייתכנו שגיאות תחביר או תאימות בספרייה.
איך טוענים
אתם מושכים את הקבצים ישירות דרך ספריית הדאטהסטס בלי צורך בבקשת אישור גישה, והמאגר פתוח לגמרי להורדה. הנתונים מגיעים בקובצי פרקט כמו wkbk_1009.parquet וכן בקובץ ג'ייסון. השדות המרכזיים שתרצו לבדוק בעיבוד הם הניסוח המילולי, הטענה הפורמלית, וההוכחה הפורמלית, כאשר סביבת הבדיקה המקורית הוגדרה מול גרסת לין v4.8.0-rc1 וספריית מתליב 4 התואמת לה.
from datasets import load_dataset
ds = load_dataset("internlm/Lean-Workbook")הרישיון
הרישיון הוא אפאצ'י 2.0. מותר להשתמש בנתונים למטרות מסחריות, לשנות אותם ולאמן עליהם מודלים בלי הגבלה כזו. החובה העיקרית היא מתן קרדיט מתאים ושמירה על תנאי הרישיון המקוריים בהפצה של הקבצים.
- שימוש מסחרי
- שינוי הקוד
- הפצה מחדש
- שימוש בפטנטים