צוות ה-Frontier Red Team של Anthropic פרסם ב-2 בנובמבר מחקר שמראה איך ספק AI יכול להוכיח מתמטית שהתשובה שקיבלתם באמת נוצרה מהמודל שהוא הבטיח. השיטה, FlashProve, מפיקה הוכחות קריפטוגרפיות בדיעבד, על אצוות של בקשות שכבר נענו ולא בזמן אמת, והקוד שלה שוחרר בקוד פתוח. לפי Anthropic, את השיפורים במערכת פיתח ובנה Claude עצמו, והוא גם כתב את מסמך המפרט של הפרוטוקול. החברה התחייבה בפומבי לבנות עד 30 בספטמבר 2026 אב-טיפוס של הסקה ניתנת להוכחה, ולדבריה עמדה ביעד דרך פרויקט נפרד שחותם על תעבורת ההסקה שלה ומחשב אותה מחדש בשרת מהימן. FlashProve היא דרך אחרת לאותה מטרה. היא עדיין רחוקה ממוצר, אבל היא עונה על שאלה שרוב המשתמשים בכלל לא שואלים: איך אתם יודעים מה רץ בצד השני?
מה זה FlashProve של Anthropic?
FlashProve היא מערכת להסקה ניתנת להוכחה (provable inference). אחרי שהמודל עונה, השרת אוסף את הבקשות לאצווה ומפיק עבורן בדיעבד הוכחות מסוג zkSNARK שמאשרת שהתשובה חושבה עם משקולות ספציפיות שהספק התחייב אליהן מראש. כל אחד יכול לבדוק את ההוכחה במחשב רגיל, בלי לראות את המשקולות ובלי לסמוך על הספק.
המחקר פורסם בבלוג המחקר של Anthropic, ו-TechCrunch סיקר אותו יום אחר כך. הניסוי לא נעשה על Claude אלא על Llama 4 Maverick של Meta, מודל MoE עם כ-400 מיליארד פרמטרים, שמתוכם בערך 17 מיליארד פעילים בכל טוקן, בגרסה מכווצת של 4 ביט. החוקרים בחרו במודל פתוח כדי שכל אחד יוכל לשחזר את התוצאות.
בין מחברי המאמר יש חוקרים מ-EPFL ומ-StarkWare, החברה הישראלית שבנתה את שמה על הוכחות קריפטוגרפיות מהסוג הזה בעולם הבלוקצ'יין. זה לא מקרי: הטכנולוגיה שנולדה כדי לאמת עסקאות בלי לחשוף אותן מגיעה עכשיו למודלי שפה.
למה צריך להוכיח איזה מודל ענה לכם?
כי היום אין לכם דרך לבדוק. כשאתם משלמים לספק API על מודל גדול, הוא יכול להריץ בשקט גרסה מכווצת וזולה יותר, לשנות הגדרות או להחליף מודל בעומס. התשובה תיראה דומה, והחשבונית תישאר אותו דבר. הוכחה קריפטוגרפית הופכת את ההבטחה של הספק לדבר שאפשר לבדוק.
הבעיה הזאת מוכרת לכל מי שעובד עם מודלים פתוחים דרך ספקי אירוח. אותו מודל מוצע אצל עשרות ספקים, במחירים שונים מאוד, ואין דרך פשוטה לדעת מי חתך פינות. FlashProve מציעה בדיקה מתמטית במקום ניחושים ובדיקות מדגמיות.
יש לזה גם צד של בטיחות. מודל שעבר בדיקות בטיחות שווה משהו רק אם הוא זה שרץ בפועל. לחברה שכבר פרסמה דוח הנפקה עם סעיפי סיכון ארוכים, זה נושא עסקי לא פחות ממחקרי.
כמה זה עולה בחישוב ובזמן?
הרבה. אצווה של 24 בקשות לוקחת לכרטיס H100 אחד כ-223 שניות, כלומר כ-110 טוקנים בשנייה, וזה בערך פי 70 עד 95 מזמן ה-GPU שנדרש להרצה רגילה ב-vLLM. ההוכחה לבקשה של 1,024 טוקנים שוקלת כ-19 מגה-בייט, והבדיקה שלה לוקחת כ-17 שניות במעבד רגיל עם 24 תהליכונים.
| נתון | FlashProve, לפי Anthropic |
|---|---|
| מודל בניסוי | Llama 4 Maverick, 4 ביט |
| קצב הפקת הוכחות | כ-223 שניות לאצווה של 24 בקשות על H100 אחד (כ-110 טוקנים בשנייה) |
| מתי נוצרת ההוכחה | בדיעבד, באצוות, לא בזמן אמת |
| תוספת חישוב | פי 70 עד 95 מזמן GPU של vLLM |
| גודל הוכחה | כ-19 MB לבקשה של 1,024 טוקנים |
| זמן בדיקה | 17 שניות ב-24 תהליכונים, 21 שניות בתהליכון אחד |
| התחייבות למשקולות | כ-6.5 MB, שלב מקדים של 39 דקות, תקפה לכ-16 מיליון בקשות |
המספרים האלה נשמעים כבדים, וזה כי הם כבדים. אבל ההשוואה למחקרים קודמים מסבירה למה החוקרים מתלהבים. שיטה קודמת בשם VerInf נזקקה ל-14.3 שעות כדי להוכיח 1,000 טוקנים. כאן מדובר על שניות. המעבר משעות לשניות הוא מה שהופך את הרעיון ממאמר אקדמי לדבר שאפשר לדמיין בשירות אמיתי.
יש גם פתרון מסחרי מתחרה, Attestable, שמגיע ל-53 עד 77 טוקנים בשנייה על Gemma 4 31B, מודל קטן בהרבה. הוא לא בקוד פתוח, כך שקשה להשוות אחד לאחד.
מה FlashProve לא יודעת לעשות?
היא מוגבלת להקשר של עד 1,024 טוקנים, עובדת רק עם פענוח חמדני (greedy) על מודל בייצוג של מספרים שלמים, ולא מסתירה את הארכיטקטורה של המודל. התקפות ערוץ צד נמצאות מחוץ לתחום. Anthropic עצמה כותבת שמדובר בהתקדמות ביניים ולא בתוכנית מחקר שהושלמה.
המגבלה של 1,024 טוקנים היא המשמעותית ביותר למשתמש רגיל. שיחה עם מסמך מצורף, או סוכן קוד שקורא מאגר שלם, עוברים את זה בקלות. גם פענוח חמדני אומר שאין דגימה אקראית (temperature), כלומר לא כך רוב הצ'טבוטים עונים בפועל. ומכיוון שההוכחות נוצרות בדיעבד, אחרי כמה דקות ולא ברגע התשובה, השיטה מתאימה יותר לביקורת על ספק מאשר לבדיקה של כל שיחה בזמן שהיא קורית.
ונקודה שקל לפספס: לפי TechCrunch, אין כרגע תוכנית להפעיל את השיטה ב-Anthropic או במעבדה אחרת. אז אם אתם משתמשים ב-Claude או במודל אחר דרך API, שום דבר לא משתנה אצלכם היום.
הוכחה כזאת מאשרת שהתשובה חושבה עם משקולות מסוימות. היא לא אומרת שהתשובה נכונה, בטוחה או חסרת הטיות. מודל שרץ בדיוק כפי שהובטח עדיין יכול להמציא עובדות.
מה זה אומר למפתחים ולחברות בישראל?
בטווח הקצר, בעיקר ידע. הקוד שוחרר ברישיון Apache 2.0, יחד עם הוכחות פורמליות ב-Lean ובודק הוכחות ב-C++. צוותים שעובדים עם ספקי אירוח של מודלים פתוחים יכולים ללמוד ממנו, ולשאול את הספקים שלהם מה הם עושים כדי להוכיח שהם מריצים את מה שהם מוכרים.
לחברות ישראליות בתחום הקריפטוגרפיה והאבטחה זה גם כיוון עסקי. הניסיון המקומי בהוכחות אפס ידע, שהגיע מעולם הבלוקצ'יין, רלוונטי פתאום לשוק ה-AI. ולמי שבונה מוצרים על מודלים זולים, כמו Claude Haiku 5.5 או מודלים פתוחים אצל ספקי צד שלישי, זו תזכורת שהמחיר הנמוך לא תמיד מספר את כל הסיפור.
אם אתם קונים גישה למודל פתוח מספק אירוח, הריצו מדי פעם סט קבוע של שאלות בדיקה והשוו לתשובות של הספק הרשמי או להרצה מקומית. זה לא הוכחה קריפטוגרפית, אבל זה יתפוס החלפה גסה של מודל. ובתוך הארגון, כדאי לדעת קודם כל באילו כלים העובדים משתמשים בכלל. על הסיכון הזה כתבנו במדריך ל-Shadow AI במקום העבודה.
שאלות נפוצות
מה זה zkSNARK במילים פשוטות?
הוכחה קריפטוגרפית קצרה יחסית שמאפשרת לצד אחד לשכנע צד אחר שחישוב בוצע נכון, בלי לחשוף את כל הנתונים שהשתתפו בו. במקרה של FlashProve, הנתונים המוסתרים הם משקולות המודל.
האם Claude כבר משתמש ב-FlashProve?
לא. הניסוי נעשה על Llama 4 Maverick, ולפי TechCrunch אין תוכנית להפעיל את השיטה ב-Anthropic או במעבדה אחרת בשלב הזה.
אפשר להוריד את הקוד?
כן. Anthropic שחררה אותו ברישיון Apache 2.0, כולל הוכחות פורמליות בשפת Lean ובודק הוכחות שכתוב ב-C++. הקישור נמצא במאמר המחקר שלה.
האם ההוכחה מבטיחה שהתשובה נכונה?
לא. היא מוכיחה רק שהתשובה חושבה עם המשקולות שהספק התחייב אליהן. נכונות, בטיחות והטיות הן שאלות נפרדות לגמרי.
השורה התחתונה
FlashProve לא תשנה את החוויה שלכם מול צ'טבוט מחר בבוקר. היא כן מראה שאפשר להוכיח איזה מודל ענה, בזמן של שניות ולא שעות, על מודל בגודל אמיתי. הדרך לשירות מסחרי עוד ארוכה: הקשר קצר, עלות חישוב גבוהה ואין לקוח ראשון. אם המונחים כאן חדשים לכם, מילון הבינה המלאכותית שלנו הוא נקודת התחלה טובה.
מקורות
