theorem-search-dataset
קוד פתוחuw-math-aicc-by-sa-4.02026-02-04
מעל מיליון משפטים מתמטיים ממאמרים אמיתיים עם ניסוח תמציתי באנגלית פשוטה לכל משפט. זה מיועד למי שרוצה לאמן חיפוש סמנטי ברמת המשפט הבודד ולא ברמת המאמר השלם.
- 253הורדות בחודש
- 24לייקים
מה זה
המאגר מחולק לארבעה קבצי Parquet שמקושרים ביניהם באמצעות מזהים ייחודיים. הקובץ המרכזי מכיל 1,341,083 משפטים מתמטיים בפורמט LaTeX שחולצו בעיקר ממאמרי arXiv, לצד מקורות כמו Stacks Project ו־ProofWiki. החילוץ נעשה ברובו באמצעות כלי בשם plasTeX, ומשפטים פחות סטנדרטיים חולצו דרך רישום בזמן הידור TeX או בעזרת ביטויים רגולריים. ניקוי המידע כלל פתיחת מאקרואים שכותבי המאמרים הגדירו בעצמם וסינון של טקסטים קטומים שקצרים משמונה תווים.
לצד המשפטים עצמם, קובץ נפרד כולל סלוגנים באנגלית שנכתבו עבור כל משפט באמצעות DeepSeek-V3.1 בטמפרטורה נמוכה של 0.2, במטרה לתאר את התוצאה המתמטית במילים ללא סימולציה כבדה. המטא-דאטה של 209,777 המאמרים שמתוכם נשלפו המשפטים יושב בקובץ נוסף עם שמות כותבים, קטגוריות וכמות ציטוטים. יש כאן גם סט בדיקה קטן של 110 שאילתות שנכתבו בידי ארבעה מתמטיקאים כדי לבחון יכולות אחזור.
מתאים ל
- אימון מודלי שיקוע למתמטיקה
התאמת מודלי embedding לחיבור בין ניסוח חופשי באנגלית לבין נוסחאות LaTeX מדויקות.
- חיפוש סמנטי למאגרי מחקר
בניית מנוע אחזור שמאפשר לחוקרים למצוא תוצאות קיימות מבלי לסרוק מאמרים שלמים ידנית.
- עוזרי הוכחה מבוססי סוכנים
חיבור המאגר דרך ממשק ייעודי כדי לאפשר לסוכני בינה מלאכותית לאמת משפטים מתמטיים.
איפה זה נופל
הנתונים כולם באנגלית ומבוססים על תחומים ספציפיים מאוד. קובץ הבדיקה מוטה בכבדות לגיאומטריה אלגברית, אנליזה ותורת המידה הגיאומטרית, כך שאינו מייצג את כל ענפי המתמטיקה. בנוסף, המאגר מייצג רק כ־15% מהמשפטים שנאספו במקור במחקר, משום שרק מאמרים בעלי רישיונות מתירניים נכנסו לכאן. מי שמפתח כלי חיפוש צריך לקחת בחשבון שהסלוגנים נוצרו על ידי מודל שפה, ולכן עלולים להכיל אי-דיוקים מתמטיים דקים שלא קיימים בטקסט המקורי.
שאלות
נפוצות
האם מותר להשתמש בדאטהסט הזה במוצר מסחרי?
כן, הרישיון מאפשר שימוש מסחרי, אך כולל דרישה לשיתוף זהה (ShareAlike). המשמעות היא שאם אתם משנים או בונים מאגר נתונים חדש שמבוסס עליו ומפיצים אותו, אתם חייבים להפיץ אותו תחת אותו הרישיון בדיוק.
כמה שוקל הדאטהסט ואיך הוא מגיע?
נפח קבצי הנתונים בפורמט Parquet מסתכם בכ־602 מגה-בייט. הקובץ הגדול ביותר הוא theorem.parquet ששוקל 265 מגה-בייט, לצד קובץ הסלוגנים ששוקל 192 מגה-בייט וקובץ פרטי המאמרים שנפחו 145 מגה-בייט.
האם יש בדאטהסט תמיכה בעברית?
לא. כל הטקסטים, תקצירי המאמרים והסלוגנים שנוצרו על ידי המודל כתובים באנגלית בלבד, לצד ביטויים מתמטיים בפורמט LaTeX.
איך חילצו את המשפטים המתמטיים מהמאמרים?
החילוץ התבצע ממקורות TeX באמצעות plasTeX עבור רוב המשפטים, לצד תהליך רישום בעת קומפילציית TeX וביטויים רגולריים למקרים מורכבים יותר. שאר 43 המשפטים הוכנסו ידנית, וכל משפט קצר משמונה תווים נמחק מהמאגר.
מדוע המאגר מכיל רק חלק קטן ממה שמופיע במאמר המדעי?
המחקר המקורי אסף מעל 9.2 מיליון משפטים, אך כ־85% ממאמרי arXiv אינם מאפשרים הפצה חוזרת לפי תנאי האתר. כדי לעמוד בדרישות החוקיות, היוצרים פרסמו רק את המשפטים שמגיעים ממאמרים בעלי רישיונות חופשיים כמו CC BY ו־CC0.
איך טוענים
טוענים את הנתונים ישירות דרך ספריית datasets באמצעות מזהה המאגר, ללא צורך באישור גישה מראש. נפח הקבצים העיקריים יחד עומד על כ־602 מגה-בייט, מתוכם קובץ המאמרים שוקל 145 מגה-בייט, קובץ המשפטים 265 מגה-בייט, וקובץ הסלוגנים 192 מגה-בייט. החיבור בין המשפטים לסלוגנים דורש הצלבה פשוטה לפי theorem_id, וקישור לפרטי המאמר נעשה לפי paper_id.
from datasets import load_dataset
ds = load_dataset("uw-math-ai/theorem-search-dataset")הרישיון
המאגר מופץ תחת רישיון cc-by-sa-4.0. מותר להשתמש בו לצרכים מסחריים ומחקריים, אך חובה לתת קרדיט ליוצרים. הכלל המשמעותי כאן הוא שיתוף זהה, שדורש מכל מי שמפיץ נגזרת של המאגר או שינוי שלו לשחרר את התוצאה תחת אותו רישיון בדיוק. אם אתם רק מאמנים מודל על הנתונים הללו ולא מפיצים את המשקלים מחדש, הדרישה הזו בדרך כלל לא כובלת את התוצר הסופי, אך כדאי לבחון את ההשלכות המשפטיות לפני שילוב במערכת סגורה.
- שימוש מסחרי
- שינוי הקוד
- חובת שיתוף באותו רישיון