FlashProve: מה הוכחת הסקה משאירה למוצר

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

זו סקירת מקורות מ-5 בנובמבר 2026. לא הידרתי את המאמת, לא הרצתי הוכחה ולא שכרתי GPU. המאגר מגדיר עצמו כתוצר מחקר לא מתוחזק שאינו מקבל תרומות. לא הייתי בוחר בו כתלות ייצור עם תמיכה.

איזה מודל ההתחייבות מזהה?

פרסום המחקר מתאר הוכחת הסקה בלי לחשוף משקלים. הספק מפרסם התחייבות לקבוצת משקלים, GPU מפיק הוכחה ו-CPU מאמת אותה מול הבקשה וההתחייבות הצפויות.

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

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

מדיניות הקבלה משנה את הטענה

התאמה מדויקת בודקת טוקנים של המודל השלם המוגדר. מדיניות clipped gap מקלה מקבלת עלויות טוקנים בתוך גבולות שנבחרו. היא אינה מוכיחה שכל טוקן הוא הבחירה המדויקת של המודל.

קבלה מדויקת ו-WITHIN LIMITS יכולות שתיהן להסתיים בקוד אפס. ממשק שהופך כל אפס לתג "תשובת מודל נכונה" משליך מידע חשוב. הפרויקט אינו ממליץ על גבולות מוכנים; סף שמקבל תשובות רגילות עדיין דורש בדיקה מול החלפות משמעותיות.

התחייבות צפויה + בקשה + כיסוי + מדיניות
                         |
                    אימות הוכחה
                         |
              תוצאה לפי המדיניות הזאת

נכונות עובדתית, רשות והשלמת משימה
דורשות ראיות נפרדות.

המשפט אינו כל התוכנית

מדריך התכונות המוכחות מתאר הוכחות Lean עבור מאמת Lean והגדרות הפרוטוקול תחת הנחות מוגדרות. מאמת C++ ומוכיח CUDA נכתבו לפי הפרוטוקול ונבדקים מולו, אך לא הוכחה שקילות פורמלית שלהם להגדרות Lean.

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

מה מספר המהירות סופר?

מדריך הביצועים מסביר את כ-110 הטוקנים בשנייה: prefill יציב, הקשר של 1,024 טוקנים, 24 בקשות באצווה ו-H100 אחד. כל הוכחה במדידות האלה מתייחסת לטוקן הבא. אתחול, יצירת התחייבות ואימות מעטפת השירות אינם נכללים במספר הראשי.

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

רישום בדיקה צנוע

זהו JSON הסברי, לא פורמט בקשה של FlashProve ולא מאמת עובד:

{
  "expected_commitment": "reviewed-registry-entry",
  "request_fixture": "synthetic-question-07",
  "expected_output_positions": [0, 1, 2],
  "acceptance_policy": "exact-match",
  "proof_status": "not-run",
  "factual_answer_check": "separate-fixture-required",
  "external_action_permission": "none"
}

הבדיקה המוצעת משנה התחייבות או בקשה ודורשת דחייה. כיסוי מקוצר צריך להציג אי-התאמה ברורה. מדיניות לא מוכרת נשארת לא נתמכת; פסק זמן אינו קבלה. הבדיקות האלה לא הורצו כאן.

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

Apache 2.0 חלה על הפרויקט; למשקלים ולרכיבים תנאים משלהם. קוד פתוח אינו מבטל עלויות GPU והנדסה. הדרישה שלי ממוצר היא להציג את המדיניות והכיסוי בלי להפוך אותם להבטחה כללית של אמת או משימה שהושלמה.