أنثروبيك تفتح مصدر FlashProve لإثبات أي نموذج كتب الرد تشفيرياً

أبرز النقاط

1. نظام بحثي مفتوح المصدر يثبت رياضياً أن رداً صدر عن نموذج التزم به المزود، بسرعة نحو 110 رموز في الثانية
2. جرى الاختبار على Llama 4 Maverick بـ400 مليار معامل، بكلفة نحو 72 ضعف زمن وحدة المعالجة مقارنة بالتشغيل العادي
3. يتيح للمدققين والجهات التنظيمية والعملاء عبر خدمات التوجيه التحقق من أن النموذج المقدَّم هو نفسه الذي جرى اختباره

خبر:

يستطيع أي طرف يحمل التزاماً منشوراً بأوزان نموذج، مع الطلب والرد، أن يتحقق على عتاد متواضع من أن هذا الرد صدر عن ذلك النموذج بعينه، بحسب نظام FlashProve الذي نشرته أنثروبيك بحثاً مفتوح المصدر في 2 نوفمبر. ويعالج النظام مشكلة أن المستخدم لا يملك عادة وسيلة للتأكد من هوية النموذج الذي أجابه، سواء بدّلته خدمة توجيه أو عبث مهاجم بتدفق الرموز.

تفصيل:

• آلية العمل: ينشر المزود مرة واحدة التزاماً تشفيرياً بأوزان النموذج في مرحلة غير متصلة، ثم يولّد لكل طلب برهاناً من نوع zkSNARK يثبت أن النموذج الملتزَم به ينتج رموز الرد المعطاة لذلك الطلب. ويتحقق أي طرف من البرهان من دون الاطلاع على الأوزان ومن دون وحدة معالجة رسومية.
• الأرقام: على نموذج Llama 4 Maverick بـ400 مليار معامل، منها نحو 17 مليار نشطة لكل رمز، بلغت السرعة نحو 110 رموز في الثانية على وحدة H100 واحدة، وحجم البرهان نحو 19 ميغابايت لكل طلب من 1,024 رمزاً، وزمن التحقق نحو 17 ثانية على 24 خيطاً أو 21 ثانية على خيط واحد.
• الكلفة: يستهلك البرهان نحو 72 ضعف زمن وحدة المعالجة الرسومية مقارنة بمحرك vLLM لدفعة من 24 طلباً، ونحو 94 ضعفاً عند أعلى حمل اختُبر. وتستغرق المرحلة غير المتصلة نحو 39 دقيقة لكل نموذج، ويغطي الالتزام الواحد نحو 16 مليون طلب قبل الحاجة إلى التزام جديد.
• المقارنة بأعمال سابقة: تذكر أنثروبيك أن نظام zkLLM بلغ نحو 2.5 رمز في الثانية على نموذج بـ13 مليار معامل، وأن VerInf احتاج 14.3 ساعة لألف رمز على النموذج نفسه مع برهان بحجم 93.6 غيغابايت استغرق تحققه نحو يوم، وأن Attestable أبلغت عن 53 إلى 77 رمزاً في الثانية على نموذج كثيف بـ31 مليار معامل من دون شيفرة مفتوحة.
• الضمانات: يوفر النظام الاكتمال والسلامة والمعرفة الصفرية والإيجاز، فالبرهان لا يكشف الأوزان ولا القيم الوسيطة ولا الخبراء الذين عملوا، وتصفه أنثروبيك بأنه “لا يمكن تزويره”. وجرى تحديد الخصائص وإثباتها بلغة Lean، مع محقق أسرع بلغة C++ يتفق مع محقق Lean على كل براهين الاختبار من دون ضمان رسمي بذاته.
• ما نُشر: الشيفرة على غيت هاب برخصة Apache 2.0 وتضم المبرهِن ومحققين وبراهين Lean ومصوِّراً تفاعلياً، مع تقرير تقني ومواصفة بروتوكول تقول أنثروبيك إن Claude كتبها. والأوزان غير مشمولة، فعلى المستخدم الحصول على Llama 4 Maverick من Hugging Face برخصة ميتا، وتشغيل المثال الكامل يحتاج آلة بوحدة رسومية كبيرة.
• الحدود المعلنة: يغطي البرهان نسخة صحيحة من الأوزان مع فك ترميز جشع، فقد تتباعد المخرجات العائمة أو المعاينة عند موضع ما. والسياق محدود بـ1,024 رمزاً، وهجمات القنوات الجانبية خارج النطاق، والبنية المختلطة للخبراء مكشوفة. وتصف أنثروبيك العمل بأنه تقدم مرحلي لا أجندة بحثية مكتملة.
• الجمهور المستهدف: تعدّ أنثروبيك المزودين الراغبين في بناء ثقة العملاء، والمقيّمين المستقلين، والعملاء عبر خدمات توجيه خارجية، والمدققين والجهات التنظيمية التي تتحقق من الامتثال لمتطلبات الحوسبة واعتماد النماذج، والمطورين الذين يحتاجون إثباتاً بأن نموذجاً بعينه راجع عملهم. ولا يذكر المنشور إتاحة النظام عبر واجهة أنثروبيك البرمجية أو منتجاتها.