FlashProve: اثبات رمزنگاری‌شده اینکه جواب از کدوم مدل اومده
هوش مصنوعیخلاصهٔ کامل‌تر
Anthropic همراه چند پژوهشگر از EPFL و MIT سیستمی به اسم FlashProve رو منتشر کرده. مشکلی که حل می‌کنه ساده‌ست: امروز وقتی از یه مدل هوش مصنوعی سؤال می‌پرسی، هیچ راهی نداری بفهمی جواب واقعاً از همون مدل اومده یا یه سرویس واسط برای صرفه‌جویی یه مدل ارزون‌تر جاش گذاشته، یا حتی یه مهاجم وسط راه توکن‌ها رو عوض کرده.
راه‌حل یه ابزار رمزنگاری به اسم zkSNARK هست، یعنی یه اثبات کوتاه که نشون می‌ده یه محاسبه درست انجام شده، بدون اینکه چیزی از جزئیاتش لو بده. روند کار دو مرحله داره: اول ارائه‌دهنده یه commitment (یعنی یه اثرانگشت کوتاه از وزن‌های مدل) منتشر می‌کنه. بعد برای هر جواب یه فایل اثبات می‌سازه که می‌گه «همین مدل ثبت‌شده، با این پرامپت، دقیقاً همین توکن‌ها رو تولید می‌کنه». هر کسی که commitment و پرامپت و جواب رو داشته باشه می‌تونه چکش کنه.
عددها برای مدل Llama 4 Maverick (یه مدل Mixture-of-Experts با ۴۰۰ میلیارد پارامتر که برای هر توکن حدود ۱۷ میلیاردش فعال میشه) با وزن‌های ۴ بیتی اینطوریه: یه H100 حدود ۱۱۰ توکن در ثانیه اثبات می‌سازه و هر اثبات برای یه درخواست ۱۰۲۴ توکنی حدود ۱۹ مگابایته. چک کردنش روی CPU با ۲۴ رشته حدود ۱۷ ثانیه طول می‌کشه و GPU لازم نداره. هزینه‌ش تقریباً ۷۰ تا ۹۵ برابر زمان GPUی اجرای خود مدل با vLLM هست.
به گفتهٔ نویسنده‌ها این پیشرفت خیلی بزرگیه: VerInf، تنها اثبات قبلی همین مدل، برای ۱۰۰۰ توکن ۱۴.۳ ساعت وقت گذاشته بود و یه اثبات ۹۳.۶ گیگابایتی ساخته بود. یکی از ترفندهای اصلی اینه که کار prover فقط به اندازهٔ expertهایی هست که واقعاً اجرا شدن، درخواست‌ها دسته‌ای و بعد از اجرا اثبات می‌شن، و وزن‌ها از رم معمولی به GPU استریم می‌شن تا همه‌چیز روی یه GPU هشتاد گیگی جا بشه.
کاربردهایی که مقاله می‌گه: ناظر می‌تونه مطمئن بشه سخت‌افزار واقعاً برای inference استفاده میشه، شرکت می‌تونه بفهمه سرورش هک نشده یا مدل دیگه‌ای جای مدل اصلی ننشسته، و مشتری می‌تونه مطمئن بشه همون مدلی که پولشو داده جوابش رو داده. برای اینکه بشه به کد اعتماد کرد، ویژگی‌های امنیتی (completeness، soundness و zero-knowledge) با Lean، یعنی یه زبان اثبات رسمی ریاضی، اثبات شدن و یه verifier کند ولی اثبات‌شده هم به Lean کنار verifier سریع C++ اومده.
نویسنده‌ها محدودیت‌ها رو هم صادقانه گفتن: این فعلاً یه نمونهٔ پژوهشیه، کد سریع C++ تضمین رسمی نداره، اثبات روی نسخهٔ عدد صحیح مدل با greedy decoding هست و نه sampling، و ساختار مدل (برخلاف وزن‌ها) مخفی نمی‌مونه. کد، اثبات‌های Lean و مستندات با لایسنس Apache 2.0 منتشر شدن.
نکات کلیدی:
- FlashProve روی Llama 4 Maverick با یه H100 حدود ۱۱۰ توکن در ثانیه اثبات می‌سازه.
- حجم هر اثبات برای درخواست ۱۰۲۴ توکنی حدود ۱۹ مگابایته و چکش روی CPU حدود ۱۷ ثانیه طول می‌کشه.
- هزینهٔ اثبات حدود ۷۰ تا ۹۵ برابر اجرای عادی مدل با vLLM هست.
- اثبات چیزی از وزن‌ها لو نمی‌ده ولی معماری مدل مخفی نمی‌مونه.
- هر commitment حدود ۱۶ میلیون درخواست اعتبار داره و ساختنش حدود ۳۹ دقیقه طول می‌کشه.
- کد و اثبات‌های Lean با لایسنس Apache 2.0 متن‌باز شدن.
