DeepTheorem

מה זה

המאגר מרכז 121,000 זוגות של משפטים והוכחות לא פורמליות ברמת IMO, בתחומים כמו אלגברה, גיאומטריה ותורת המספרים. כל רשומה כוללת את המשפט, הוכחות שנוצרו או אומתו על ידי המודל o3-mini, ערך אמת שמציין אם המשפט נכון או שגוי, דירוג רמת קושי ושיוך לתחום מתמטי.

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

מתאים ל

• אימון מודלים עם חיזוקים

  אימון אלגוריתמים כמו RL-Zero באמצעות וריאציות של משפטים לבדיקת יציבות ההסקה.

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

  בדיקת יכולת המודל לייצר הוכחות לא פורמליות ברמת אולימפיאדה באלגברה וגיאומטריה.

• בדיקת ערכי אמת

  אימון מודלים לזיהוי האם טענה מתמטית מורכבת נכונה או שגויה לפי הוכחה נתונה.

איפה זה נופל

ההוכחות וערכי האמת מבוססים על המודל o3-mini, ולכן שגיאות או הזיות של המודל הזה עשויות לחלחל ישירות לתוך הנתונים. המאגר מוגבל לשפה האנגלית ומתמקד אך ורק במתמטיקה תחרותית ברמה גבוהה מאוד, כך שהוא לא יעזור בחישובים יומיומיים או במשימות שפה כלליות. בנוסף, קובצי הבדיקה FIMO, HMMT ו־Putnam אינם חלק ממאגר זה ונמצאים בקישור נפרד.

איך טוענים

טוענים את המאגר ישירות דרך הספרייה של Hugging Face מהמזהה Jiahao004/DeepTheorem, ללא צורך בהרשאות גישה מיוחדות. הנתונים מחולקים לשלושה קובצי Parquet תחת תיקיית data, וקיימים גם בפורמט Arrow. השדות המרכזיים לעבודה הם טקסט המשפט, ההוכחות של o3-mini, ערך האמת, קטגוריית התחום, דרגת הקושי והווריאציות המצורפות.

from datasets import load_dataset

ds = load_dataset("Jiahao004/DeepTheorem")

הרישיון

המאגר מופץ תחת רישיון MIT. הרישיון מתיר שימוש מסחרי, שינוי והפצה, ומחייב רק מתן ייחוס ליוצרים המקוריים ושמירה על תנאי הרישיון. מודלים שתאמנו על הנתונים אינם מחויבים להיפתח בקוד פתוח.

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

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