DeepSeek-Prover-V1
קוד פתוחdeepseek-aiother2024-08-16
מאגר נתונים סינתטי להוכחת משפטים מתמטיים בשפת Lean 4. הוא מתאים למי שרוצה לאמן מודלים על הוכחות פורמליות של בעיות מתמטיות מתקדמות.
- 796הורדות בחודש
- 74לייקים
מה זה
המאגר מכיל מידע שנועד לפתור את המחסור בדאטה לאימון מודלים של שפה בהוכחות פורמליות. הנתונים מתבססים על בעיות מתמטיות מרמת תיכון ועד רמת תחרויות אקדמיות לתואר ראשון. התהליך כלל תרגום של הבעיות משפה טבעית לטענות פורמליות בקוד, סינון של טענות באיכות נמוכה, ויצירת הוכחות מתאימות כדי לבנות סט נתונים סינתטי רחב היקף.
לפי התיעוד שפורסם, הסט שימש לאימון המודל DeepSeekMath 7B וכולל שמונה מיליון טענות פורמליות יחד עם ההוכחות שלהן. המטרה המרכזית שלו היא לאפשר יצירת הוכחה מלאה עבור מערכות אימות כמו Lean 4, והוא הציג ביצועים שנבדקו מול מבחני miniF2F ובעיות אולימפיאדה מורכבות.
מתאים ל
- אימון מודלים להוכחות
אימון מודלי שפה על יצירת הוכחות פורמליות מלאות בשפת Lean 4 מתוך בעיות מתמטיות.
- הערכת ביצועים במתמטיקה
בדיקת יכולות הסקת מסקנות ופתרון תחרויות מתמטיות מתקדמות על מערכות אוטומטיות.
- מחקר בתרגום פורמלי
מחקר על תרגום אוטומטי של שאלות בשפה טבעית לקוד פורמלי של עוזרי הוכחה.
איפה זה נופל
כל המאגר מורכב מנתונים סינתטיים שתורגמו משפה טבעית וסוננו באופן אוטומטי, מה שאומר שעלולות להופיע שגיאות לוגיות עדינות או עיוותים שמודלים מייצרים. אין כאן עברית בכלל, וההוכחות תקפות אך ורק לסביבת Lean 4. אם אתם עובדים עם מערכות הוכחה אחרות כמו Coq או Isabelle, הנתונים האלה לא יעזרו לכם בלי המרה מורכבת. מעבר לזה, הכרטיס לא מפרט את אופן חלוקת השדות המדויק בתוך קובץ הנתונים.
שאלות
נפוצות
האם מותר להשתמש בדאטהסט הזה למטרות מסחריות?
התיעוד בעמוד מציין תמיכה בשימוש מסחרי, אך הרישיון הרשמי מוגדר כ־other. כדאי לקרוא את קובץ LICENSE המצורף כדי לוודא שאין הגבלות ספציפיות על אימון מודלים מסחריים.
האם הדאטהסט כולל שאלות או הוכחות בעברית?
לא, אין כאן עברית כלל. התוכן מבוסס על בעיות מתמטיות בשפה האנגלית ותרגום פורמלי לשפת הקוד Lean 4 בלבד.
איך נאספו הנתונים שבמאגר?
היוצרים אספו בעיות מתמטיות מתחרויות של בתי ספר תיכוניים ואוניברסיטאות ותרגמו אותן לשפה פורמלית. לאחר מכן הם סיננו טענות לא איכותיות ויצרו הוכחות מלאות באופן סינתטי.
מה הפורמט שבו הנתונים מגיעים ואיך טוענים אותם?
הנתונים מגיעים בקובץ dataset.jsonl יחיד שניתן לקריאה ישירה. אפשר לעבוד איתו באמצעות פייתון רגיל או למשוך אותו בעזרת ספריית datasets ללא צורך בהרשאות מיוחדות.
איך טוענים
הנתונים מוגשים בקובץ dataset.jsonl פשוט שנמצא ישירות במאגר, לצד קובצי הרישיון וההסברים. אין צורך באישור גישה מיוחד, ואפשר להוריד את הקובץ ישירות או לטעון אותו בעזרת ספריית datasets הסטנדרטית. המאגר כולל ארבעה קבצים בסך הכל. שדות המפתח מייצגים את הטענות הפורמליות ואת ההוכחות המותאמות לסביבת Lean 4, כך שצריך לוודא שהפייפליין שלכם יודע לפרסר שורות jsonl שמכילות קוד מתמטי ומבני הוכחה.
from datasets import load_dataset
ds = load_dataset("deepseek-ai/DeepSeek-Prover-V1")הרישיון
הרישיון המוגדר במערכת הוא other, אך בעמוד המאגר מצוין כי הקוד תחת MIT והמודלים תחת הסכם שימוש ייעודי. בנוסף נכתב במפורש כי הכלי תומך בשימוש מסחרי. עם זאת, בגלל ההגדרה הכללית יש לבדוק היטב את תנאי קובץ הרישיון המצורף לפני שמשלבים את המידע באימון מסחרי.