Anthropic FlashProve: sun'iy intellektda kriptografik isbotlash tizimi

Anthropic kompaniyasi bir qator nufuzli universitetlar va tashkilotlar tadqiqotchilari bilan hamkorlikda katta til modellari uchun kriptografik xulosalarni isbotlash yo'nalishida muhim qadam tashladi. Yangi taqdim etilgan FlashProve tizimi foydalanuvchilarga sun'iy intellekt javoblarining aynan qaysi model tomonidan yaratilganini tekshirish imkonini beradi.

• FlashProve yirik til modellari uchun mo'ljallangan ochiq va samarali zkSNARK prototipidir.
• Sinovlar 400 milliard parametrli Llama 4 Maverick modeli va 4-bitli kvantlash asosida o'tkazildi.
• Bitta H100 GPU 1024 ta tokendagi so'rov uchun sekundiga 110 ta token va ~19 MB hajmda isbot yaratadi.
• Barcha kod, Lean rasmiy isbotlari va hujjatlar Apache 2.0 litsenziyasi ostida ommaga taqdim etildi.

Nima uchun xulosalarni isbotlash muhim

Foydalanuvchi sun'iy intellekt modeli bilan muloqot qilganda, javob haqiqatan ham o'zi tanlagan modeldan kelganiga yoki xarajatlarni tejash uchun boshqasiga almashtirilmaganiga amin bo'la olmaydi. Kriptografik usullar bu muammoni hal qilib, provayderga modelni oldindan belgilash va har bir javob aynan o'sha modeldan chiqqanini isbotlash imkonini beradi.

zkSNARK texnologiyasi yordamida provayder javob bilan birga qisqa isbot yuboradi va foydalanuvchi uni oddiy protsessorda qisqa vaqt ichida tekshirishi mumkin. Bunda foydalanuvchi model og'irliklari va arxitekturasi haqida hech qanday maxfiy ma'lumotga ega bo'lmasa ham, natijaning to'g'riligiga ishonch hosil qiladi.

Flashprove unumdorligi va texnik xususiyatlari

Kriptografik isbotlarni yaratish juda ko'p resurs talab etsa-da, FlashProve yordamida yuqori tezlikka erishildi. Llama 4 Maverick arxitekturasidagi 400 milliard parametrli model uchun bitta H100 GPU sekundiga taxminan 110 ta token tezligida isbotlarni shakllantiradi.

Har 1024 ta tokendan iborat so'rov uchun isbot hajmi atigi 19 megabaytni tashkil qiladi. Bu ochiq manbali vLLM kutubxonasiga nisbatan GPU vaqtini 70-95 barobar ko'proq talab qilsa-da, avvalgi ochiq tizimlarga qaraganda solishtirib bo'lmaydigan darajada tezdir.

Ochiq kod va kelajakdagi imkoniyatlar

Tadqiqotchilar murakkab tizimlardagi xatolarni kamaytirish uchun Lean rasmiy verifikatsiya tilida yuqori darajadagi auditoqli bayonotlarni tayyorladilar. Loyiha dasturiy ta'minoti, C++ tilidagi tezkor verifikator va Lean isbotlari boshqa tadqiqotchilar uchun ochiq e'lon qilindi.

Ushbu ishlanma kelgusida mustaqil auditorlar va regulyatorlar uchun sun'iy intellekt xavfsizligini ta'minlash hamda uning rivojlanish sur'atlarini nazorat qilishda muhim vosita bo'lishi kutilmoqda. Apache 2.0 litsenziyasi boshqalarga tizimni yanada takomillashtirish imkonini beradi.