אנתרופיק משחררת FlashProve: הוכחה קריפטוגרפית לזהות המודל שענה
כששולחים שאלה למודל שפה, התשובה מגיעה מהר, אבל כמעט אין דרך לדעת איזה מודל באמת ענה. אנתרופיק, החברה שמאחורי Claude, מציגה אב-טיפוס בקוד פתוח בשם FlashProve שמנסה לסגור את הפער הזה: לכל תשובה מצורפת הוכחה מתמטית שהטקסט יצא ממודל מסוים, בלי לחשוף את המשקולות, כלומר את המספרים הפנימיים שמגדירים איך המודל פועל ונחשבים לנכס היקר ביותר של כל מעבדה.
הרעיון קרוב לחתימה דיגיטלית על דואר. בשלב ראשון הספק מפרסם טביעת אצבע קצרה, התחייבות קריפטוגרפית שמקבעת סט מדויק של משקולות. בשלב שני, לכל בקשה, השרת מפיק קובץ הוכחה שמראה שהמודל שהתחייב אליו הוא שייצר את הטקסט. מי שמחזיק בטביעת האצבע, בשאלה ובתשובה יכול לבדוק את ההוכחה על מעבד רגיל בתוך שניות, בלי גישה למודל עצמו.
לשוק יש סיבה ברורה לעניין. ספקי בינה מלאכותית מוכרים גישה למודלים במחירים שונים, ומפעילי ניתוב ושירותי ביניים מחליטים לעתים באיזה מודל להשתמש בפועל. ספק יכול להחליף בשקט מודל יקר במודל זול כדי לחסוך בעלויות מחשוב, או להפך להריץ מודל חזק יותר במבחני ביצועים כדי לשפר תוצאות. גם מעבדה שמפעילה את המודל שלה עצמה נמצאת באותו מצב, והמערכת נועדה לעבוד גם מולה. במקביל, הוכחה כזו עשויה לשמש חברות שמצהירות שהקוד שלהן נסרק במודל סייבר מתקדם, או רגולטורים שרוצים לוודא שגוף מסוים עובד עם מודל מאושר.
המספרים מבהירים שמדובר עדיין במחקר. אנתרופיק בדקה את המערכת על Llama 4 Maverick של מטא, מודל פתוח בהיקף של כ-400 מיליארד פרמטרים, בגרסת 4 ביט. מעבד גרפי בודד מדגם H100 של אנבידיה מפיק הוכחות בקצב של כ-110 טוקנים בשנייה, וקובץ ההוכחה לבקשה של עד 1,024 טוקנים שוקל כ-19 מגה-בייט. זמן העיבוד הגרפי גבוה פי 70 עד 95 מזמן הרצת המודל עצמו בספרייה פתוחה נפוצה. במדידה על אצווה של 24 בקשות נדרשו כ-223 שניות, והאימות על מעבד רגיל ארך כ-17 עד 21 שניות. המערכת עובדת עם גרסה במספרים שלמים ועם פענוח דטרמיניסטי, ונשענת על ארכיטקטורת תערובת מומחים. שירות מסחרי רגיל משתמש בדרך כלל בהגדרות אחרות, כך שהדרך לשימוש שוטף עוד ארוכה.
ועדיין, הפער מול מערכות קודמות גדול. מערכות פתוחות קודמות להוכחת הסקה, שמבוססות על הוכחות אפס ידע מסוג zkSNARK, היו איטיות בסדרי גודל, עם הוכחות של עשרות גיגה-בייט וזמני אימות של שעות. באנתרופיק מציינים ש-Claude עצמו השתתף בפיתוח השיפורים, ושהצוות הוסיף הצהרות אבטחה מאומתות בשפת האימות הפורמלי Lean. בעבודה השתתפו גם חוקרים מהאקדמיה ומתעשיית הקריפטוגרפיה. הקוד והמפרט פורסמו ב-GitHub תחת רישיון Apache 2.0, והחברה מדגישה שאין כרגע תוכנית להטמיע את המערכת במוצרים שלה או אצל מעבדות אחרות.
למערכת יש גם גבולות שהחוקרים עצמם מסמנים. היא מוכיחה שהמודל שהתחייב אליו הפיק את הטקסט, אבל המשתמש צריך לקבל את מזהה ההתחייבות ממקור אמין ולא מהשרת שאת התשובה שלו הוא בודק, אחרת השרת יכול להציג הוכחה תקינה למודל אחר. היא מסתירה את המשקולות ולא את ארכיטקטורת המודל, ואינה מגינה מפני דליפת מידע דרך זמני תגובה. אורך ההקשר בבדיקות מוגבל ל-1,024 טוקנים, מרחק גדול מחלונות ההקשר של מודלים מסחריים.
המשמעות העסקית נוגעת גם לענן ולתחרות. לקוחות ארגוניים רבים ניגשים למודלים דרך פלטפורמות של אמזון ושל אלפאבית, ומשלמים לפי רמת המודל. אם הוכחות כאלה יהפכו לסטנדרט, אפשר יהיה לדרוש מספק הבינה המלאכותית הוכחה למה ששולם עליו, במקום להסתפק בהצהרה. אותו כלי עשוי לשמש גם לפיקוח על הקצאת כוח מחשוב, כלומר לאמת שחישובי הסקה מסוימים אכן בוצעו, אם כי ההוכחה אינה מעידה שאותה חומרה לא שימשה במקביל גם לאימון מודלים.
הפרסום מגיע בתקופה שבה אנתרופיק נמצאת בזרקור גם בצד הפיננסי, לקראת הנפקה צפויה ועם התחייבויות ענק לרכישת כוח מחשוב. להרחבה: יותר מ-100 אלף דולר בחודש לעובד: כמה עולים לאנתרופיק 5,300 העובדים שלה. ובמקביל: אנתרופיק מזהירה בתשקיף: ייתכן שאנחנו קרובים לבינה מלאכותית שמאיצה את הפיתוח של עצמה. בין המשקיעות הגדולות בחברה נמנות אמזון ואלפאבית, שמפעילות גם את פלטפורמות הענן שדרכן לקוחות רבים ניגשים למודלים. אם גישה כזו תתפוס, שקיפות הזהות של המודל עשויה להפוך לחלק מתנאי הרכישה של שירותי AI, בדיוק כמו SLA על זמינות או על מחיר לטוקן.
