DeepSeek-ProverBench
קוד פתוחdeepseek-aiרישיון לא דווח2025-04-30
מאגר מבחן של 325 בעיות מתמטיות מנוסחות בשפת Lean 4 להוכחה פורמלית. הוא מתאים למי שרוצה לבדוק יכולות של מודלים בהוכחת משפטים ברמה אקדמית ובתחרויות.
- 598הורדות בחודש
- 47לייקים
מה זה
המאגר כולל 325 בעיות פורמליות שמיועדות להערכת מודלים של הוכחת משפטים אוטומטית. 15 בעיות מגיעות מתחרויות AIME של השנים 2024 ו־2025 ומתמקדות בתורת המספרים ובאלגברה ברמת תיכון תחרותית. שאר 310 השאלות לוקטו מדוגמאות בספרי לימוד ובחומרי הדרכה במתמטיקה ברמה אקדמית.
החלוקה הפנימית לפי תחומים מציגה 90 בעיות בחשבון אינפיניטסימלי, 50 באלגברה לינארית, 40 באלגברה מופשטת ו־40 בתורת המספרים. בנוסף יש 30 באלגברה בסיסית, 30 באנליזה ממשית, ו־10 בכל אחד מהתחומים הבאים: אנליזה מרוכבת, אנליזה פונקציונלית והסתברות. כל בעיה מנוסחת במבנה פורמלי המתאים לסביבת העבודה של Lean 4 לצד ניסוח השאלה המקורית.
מתאים ל
- בנצ'מרק למודלי הוכחה
הרצת בדיקות השוואתיות של מודלי שפה על הוכחת משפטים פורמליים ב־Lean 4 מול נתוני AIME וספרי לימוד.
- בדיקת תוכניות הוכחה
הערכת היכולת של מודל לייצר תוכנית פעולה ופירוק למטרות משנה לפני הפקת הקוד הפורמלי.
- אימות פתרונות אוטומטי
שילוב בקוד בדיקה מול סביבת Lean 4 לבחינת תקינות של פתרונות מתמטיים ברמת תואר ראשון.
איפה זה נופל
זהו מאגר מבחן קטן מאוד של 325 דוגמאות בלבד, כך שהוא אינו מתאים לאימון מודלים אלא רק להערכה. כל הבעיות מנוסחות אך ורק באנגלית ובקוד של Lean 4, ללא שפות אחרות או מערכות הוכחה מתחרות כמו Isabelle או Coq. בנוסף, רוב התוכן מגיע מספרי לימוד ידועים ומתחרויות ציבוריות, מה שמעלה סיכון ממשי של זליגת נתונים בזמן אימון מודלי שפה כלליים.
שאלות
נפוצות
האם מותר להשתמש בדאטהסט לפרויקט מסחרי?
לא מומלץ כרגע. בדף המאגר לא דווח רישיון רשמי עבור קובץ הנתונים עצמו, ולכן מבחינה משפטית אין היתר שימוש ברור לפיתוח מסחרי. כדאי להמתין לעדכון הרישיון מצד היוצרים לפני שמבססים עליו מוצר.
האם יש במאגר שאלות בעברית?
לא. כל הנתונים, הבעיות וההגדרות הפורמליות כתובים באנגלית בלבד ובשפת הקוד של Lean 4. אין במאגר שום ייצוג לעברית.
מאיפה הגיעו השאלות שמופיעות בקובץ?
15 שאלות נלקחו מתוך תחרויות המתמטיקה של AIME בשנים 2024 ו־2025 בתחומי אלגברה ותורת המספרים. שאר 310 הבעיות לוקטו מספרי לימוד ומחומרי הדרכה מתמטיים ברמה אקדמית.
מה ההבדל בין המאגר הזה למאגרים כמו miniF2F?
המאגר הזה מתמקד באופן משמעותי במתמטיקה ברמת תואר ראשון מספרי לימוד, עם דגש חזק על חשבון אינפיניטסימלי ואלגברה לינארית, ולא רק בשאלות מתחרויות תיכון. הוא מותאם במיוחד לסביבת Lean 4 העדכנית.
איך טוענים
המאגר כולל שלושה קבצים, והתוכן עצמו נמצא בתוך קובץ proverbench.jsonl. אין צורך באישור גישה מיוחד או בהרשמה מקדימה, אפשר פשוט להוריד את הקובץ ישירות מעמוד הדאטהסט ב־Hugging Face או לטעון אותו בעזרת ספריית datasets הרגילה של פייתון.
כל שורה מייצגת בעיה עצמאית שכוללת את הניסוח הפורמלי שלה ב־Lean 4. כדי לעבוד איתו צריך סביבת Lean 4 מותקנת ומקושרת לספריית Mathlib כדי לאמת את ההוכחות שהמודל שלכם מייצר על בסיס השדות שבקובץ.
from datasets import load_dataset
ds = load_dataset("deepseek-ai/DeepSeek-ProverBench")הרישיון
בעמוד הדאטהסט לא דווח רישיון כלל. המפרסמים צירפו קישורים לרישיונות הקוד והמודל במאגר הכללי של DeepSeek, אך עבור קובץ הנתונים הזה אין הגדרה משפטית רשמית. בלי רישיון מפורש, השימוש בו למטרות מסחריות או לפיתוח מוצרים סגורים מהווה סיכון משפטי ומוטב להגביל אותו למחקר פנימי.