FineProofs-SFT
קוד פתוחlm-proversapache-2.02026-02-04
מאגר לאימון מודלים להוכחות מתמטיות ברמת אולימפיאדה, עם שרשראות חשיבה מפורטות. הוא מתאים למי שרוצה לאמן מודל להנמקה מתמטית כבדה וזקוק לפתרונות מלאים עם ציוני איכות וקושי מובנים.
- 211הורדות בחודש
- 43לייקים
מה זה
המאגר מכיל 7,777 דוגמאות שנשענות על 4,300 בעיות ייחודיות מתוך תחרויות מתמטיקה כמו IMO, APMO ופורום AoPS. כל רשומה כוללת את נוסח הבעיה, עקבות חשיבה פנימיים שחולצו מתגי think, הוכחה סופית בפורמט LaTeX, קטגוריה ופרטי התחרות המקורית. הפתרונות חולצו באמצעות זיקוק מהמודל DeepSeek-Math-V2 בהקשר של 128 אלף תווים.
הסינון הראשוני העיף בעיות עם שרטוטים, תרגילים טריוויאליים ותחרויות קלות מדי, לצד בדיקות איכות שביצע GPT-5-Nano כדי לאתר פערים לוגיים. בנוסף, כל פתרון מגיע עם ציון מודל שופט על סקאלה של 0 עד 7 מבית Gemini-3-Pro, ומדד קושי שחושב על ידי 128 דגימות מהמודל Qwen3-4B-Thinking-2507 ונבדק מול openai/gpt-oss-20b.
הנתונים מחולקים לשתי גרסאות. הגרסה שנקראת default מחזיקה את 4,300 הבעיות הייחודיות בלבד לאחר ניקוי כפילויות, והגרסה שנקראת all מחזיקה את כל 7,777 הדוגמאות, כולל כמה פתרונות שונים לאותה בעיה.
מתאים ל
- אימון SFT להוכחות
זיקוק יכולות חשיבה מורכבות למודלים קטנים באמצעות שרשראות חשיבה מפורטות ב־LaTeX.
- למידת חיזוק מונחית
בניית מסלול אימון מדורג באלגוריתם כמו GRPO בעזרת ציוני הקושי והתגמול המוכנים מראש.
- אימון מודל שופט
שימוש בציוני Gemini המדורגים מאפס עד שבע כדאטה להערכת איכות של פתרונות מתמטיים.
איפה זה נופל
החומר כולו באנגלית בלבד וכולל בעיות טקסטואליות בלבד. כל בעיה שדרשה תרשים או שרטוט גיאומטרי הוסרה לחלוטין בתהליך הסינון. בנוסף, הפתרונות שנוצרו על ידי מודל המקור לא סוננו לפי ציוני הנכונות, ולכן המאגר מכיל בכוונה גם הוכחות שגויות או חלקיות. אם תאמנו עליו בלי סינון ציונים מוקדם, המודל שלכם יספוג שגיאות לוגיות.
הציונים עצמם מגיעים ממודלים שופטים ולא מבדיקה אנושית, מה שעלול לייצר סטיות בהערכה. בעיה נוספת היא נטייה של מודלים שהתאמנו עליו לייצר פתרונות ארוכים באופן מוגזם, אלא אם מאזנים אותם בלמידת חיזוק.
שאלות
נפוצות
האם מותר להשתמש במאגר לפיתוח מוצר מסחרי?
כן. הרישיון המוגדר הוא apache-2.0, שמתיר שימוש מסחרי מלא, שינוי הנתונים ושילובם במוצרים סגורים. התנאי העיקרי הוא שמירה על הצהרת הרישיון המקורית והקרדיט למפתחים.
האם יש במאגר שאלות או פתרונות בעברית?
לא. המאגר מוגדר וכתוב כולו באנגלית בלבד. לא קיימים בו תרגומים, כך שאם אתם מכוונים למתמטיקה בעברית תצטרכו לתרגם את השאלות וההוכחות בעצמכם.
מאיפה הגיעו הנתונים והפתרונות שבפנים?
הבעיות נאספו ממאגרי אולימפיאדות קיימים של פרויקט Numina ומאתר AoPS. הפתרונות ותהליכי החשיבה נוצרו באמצעות הסקת מסקנות של המודל DeepSeek-Math-V2, והציונים חושבו באמצעות Gemini-3-Pro ומודל Qwen ייעודי.
באיזו תצורה כדאי להשתמש, default או all?
תצורת default כוללת 4,300 בעיות ייחודיות ללא כפילויות, ויוצרי המאגר דיווחו שאימון עליה הניב תוצאות טובות יותר באימון זיקוק. תצורת all מחזיקה 7,777 דוגמאות עם מספר פתרונות שונים לאותה שאלה, ומתאימה יותר למחקרי חיזוק או השוואה.
איך טוענים
טוענים את הנתונים ישירות דרך ספריית datasets בפייתון באמצעות load_dataset על lm-provers/FineProofs-SFT, בלי צורך בבקשת גישה מיוחדת או אישור. המאגר שמור בקובצי parquet סטנדרטיים ומחולק לשתי תצורות שונות לבחירה, default או all, שתיהן על ספליט של train.
אם אתם מאמנים מודלי שיחה, שדה ה־messages כבר מסודר במבנה שיחה סטנדרטי שכולל את תגי ה־think של תהליך החשיבה. שימו לב שבאימון המקורי של QED-Nano עבדו עם אורך רצף מקסימלי של 45,056 תווים, כך שצריך חומרה עם זיכרון משמעותי.
from datasets import load_dataset
ds = load_dataset("lm-provers/FineProofs-SFT")הרישיון
המאגר מופץ תחת רישיון apache-2.0. הרישיון מאפשר שימוש חופשי, שינוי, הפצה ומסחור מלא של הנתונים, בתנאי ששומרים על הודעת זכויות היוצרים והרישיון המקורי. אין חובה לשתף את השינויים או את המודלים שתאמנו תחת אותו הרישיון.
- שימוש מסחרי
- שינוי הקוד
- הפצה מחדש
- שימוש בפטנטים