پیشرفت آنتروپیک در توسعه روش‌های اثبات‌پذیر برای استنتاج مدل‌های زبانی بزرگ با FlashProve

با گسترش استفاده از مدل‌های زبانی بزرگ (LLM)، یکی از چالش‌های مهم پیش روی ارائه‌دهندگان و کاربران این فناوری، اطمینان از صحت هویت مدلی است که واقعاً درخواست‌ها را پردازش می‌کند. در شرایط فعلی، وقتی کاربر درخواستی را به یک مدل هوش مصنوعی ارسال می‌کند، راه مطمئنی برای اطمینان از اینکه پاسخ دریافتی دقیقاً توسط همان مدل انتخاب‌شده تولید شده است، وجود ندارد.

مسئله اعتماد به خروجی مدل‌های هوش مصنوعی

ممکن است یک سرویس مسیریابی درخواست (Routing Service) به دلایل کاهش هزینه، به‌جای مدل اصلی از مدلی ارزان‌تر استفاده کند. همچنین، مهاجمان سایبری یا عوامل مخرب داخلی می‌توانند جریان توکن‌های خروجی را تغییر دهند و پاسخ‌های دست‌کاری‌شده را به نام یک مدل معتبر به کاربران ارائه کنند. حتی کیفیت بالای پاسخ نیز نمی‌تواند اثبات کند که خروجی واقعاً از مدل ادعاشده تولید شده است.

این مسئله برای کاربردهای روزمره که کاربران بیشتر به محتوای پاسخ اهمیت می‌دهند، چندان محسوس نیست؛ اما در ارزیابی مستقل مدل‌ها، استفاده سازمانی، امنیت زیرساخت‌های هوش مصنوعی و نظارت قانونی اهمیت زیادی دارد. ارزیابان مستقل باید مطمئن باشند مدلی که پیش و پس از انتشار آزمایش می‌کنند، همان مدلی است که واقعاً در اختیار کاربران قرار می‌گیرد. همچنین، مشتریانی که از طریق واسطه‌ها به مدل‌ها دسترسی دارند، باید بتوانند تأیید کنند هزینه پرداخت‌شده برای استفاده از همان مدل موردنظرشان صرف شده است.

آنتروپیک برای پاسخ به این چالش، مفهوم «استنتاج اثبات‌پذیر» (Provable Inference را مطرح می‌کند. هدف این رویکرد آن است که کاربر بتواند بدون دسترسی به وزن‌های مدل و بدون برخورداری از توان محاسباتی گسترده، تأیید کند پاسخ دریافتی توسط مدل مشخصی تولید شده است.

استنتاج اثبات‌پذیر و نقش رمزنگاری

یکی از روش‌های پیاده‌سازی استنتاج اثبات‌پذیر، استفاده از فناوری رمزنگاری موسوم به «برهان فشرده دانش صفر» (zkSNARK) است. این فناوری به یک طرف اجازه می‌دهد با ارائه گواهی رمزنگاری‌شده‌ای کوتاه، طرف دیگر را متقاعد کند که یک محاسبه مشخص به‌درستی انجام شده است؛ بدون آنکه اطلاعات محرمانه مربوط به محاسبه افشا شود.

دو ویژگی اصلی zkSNARK آن را برای استنتاج اثبات‌پذیر مناسب می‌کند:

• دانش صفر (Zero-Knowledge): گواهی ارائه‌شده اطلاعاتی درباره وزن‌های مدل یا مقادیر میانی محاسبات افشا نمی‌کند. البته این ویژگی در سامانه موردبحث به معنای پنهان ماندن معماری مدل نیست.
• فشردگی (Succinctness): اندازه گواهی کوچک است و تأیید آن در مقایسه با اجرای مجدد محاسبات، به منابع محاسباتی بسیار کمتری نیاز دارد.

در این سازوکار، ارائه‌دهنده مدل ابتدا تعهد رمزنگاری‌شده‌ای نسبت به وزن‌های مشخص مدل ایجاد می‌کند. این تعهد مانند اثر انگشتی دیجیتال، یک مجموعه دقیق از وزن‌ها را مشخص می‌کند، بدون آنکه خود وزن‌ها در اختیار کاربر قرار بگیرند. سپس، همراه هر پاسخ، گواهی‌ای ارائه می‌شود که نشان می‌دهد توکن‌های خروجی با اجرای همان مدل متعهدشده روی ورودی مشخص تولید شده‌اند. به‌این‌ترتیب، کاربر می‌تواند با در اختیار داشتن تعهد مدل، ورودی و پاسخ، اعتبار خروجی را بررسی کند؛ بدون آنکه به وزن‌های مدل یا زیرساخت محاسباتی ارائه‌دهنده دسترسی داشته باشد.

چهار کاربرد اصلی استنتاج اثبات‌پذیر

استفاده از zkSNARKها می‌تواند به حل چند مسئله مهم در امنیت، حکمرانی و نظارت بر توسعه هوش مصنوعی کمک کند.

• نظارت بر منابع محاسباتی و سرعت توسعه هوش مصنوعی:
  برخی پیشنهادهای نظارتی برای مدیریت توسعه هوش مصنوعی بر پایش سخت‌افزار و نحوه استفاده از آن تمرکز دارند. برای مثال، ممکن است ارائه‌دهنده‌ای ملزم شود منابع محاسباتی خود را به اجرای استنتاج اختصاص دهد، نه آموزش یک مدل قدرتمندتر. استنتاج اثبات‌پذیر می‌تواند با الزام ارائه گواهی برای درخواست‌های پردازش‌شده، امکان بررسی این موضوع را فراهم کند. نهاد ناظر می‌تواند تأیید کند که درخواست‌ها واقعاً توسط مدل ادعاشده پردازش شده‌اند، بدون آنکه به زیرساخت پیچیده ارائه‌دهنده یا اطلاعات اختصاصی مدل دسترسی داشته باشد.
• شناسایی دست‌کاری و جایگزینی مدل‌ها:
  با افزایش ارزش مدل‌های هوش مصنوعی، سرورهای میزبان آن‌ها به اهداف جذاب‌تری برای حمله‌های سایبری تبدیل می‌شوند. مهاجم ممکن است به سرور استنتاج نفوذ کند، وزن‌های مدل را استخراج کند یا پاسخ‌های مخرب را در میان خروجی‌های معتبر به کاربران ارائه دهد. راهکار پیشنهادی این است که ارائه‌دهنده برای هر پاسخ، یک گواهی zkSNARK مطالبه کند. ازآنجاکه گواهی به تعهد مشخصی از وزن‌های مدل متصل است، صرفاً اجرای یک مدل دلخواه را تأیید نمی‌کند، بلکه نشان می‌دهد مدل موردنظر واقعاً پاسخ را تولید کرده است. در نتیجه، مهاجمی که سرور را به خطر انداخته یا مدلی را جایگزین مدل مجاز کرده باشد، نمی‌تواند بدون تولید گواهی معتبر برای وزن‌های موردانتظار، فعالیت خود را پنهان کند.
• اثبات منشأ و اعتبار محتوای تولیدشده:
  یکی دیگر از کاربردهای مهم این فناوری، تأیید منشأ محتوای تولیدشده توسط مدل‌هاست. با افزودن گواهی رمزنگاری‌شده به هر پاسخ، می‌توان اثبات کرد که خروجی موردنظر با استفاده از مدل ادعاشده و برای ورودی مشخص تولید شده است.
• اطمینان از استفاده از مدل‌های تأییدشده:
  در برخی چارچوب‌های نظارتی ممکن است ارائه‌دهندگان هوش مصنوعی ملزم شوند فقط مدل‌هایی را در اختیار کاربران قرار دهند که از نظر ایمنی تأیید شده‌اند. بااین‌حال، ارائه‌دهندگان ممکن است به دلایل اقتصادی یا رقابتی تمایل داشته باشند از مدل‌های ارزان‌تر یا قدرتمندتری استفاده کنند که هنوز تأییدیه لازم را دریافت نکرده‌اند. نهادهای ناظر می‌توانند با الزام ارائه گواهی zkSNARK برای پاسخ‌ها، استفاده از مدل‌های تأییدشده را کنترل کنند. ازآنجاکه گواهی به مدل مشخصی متصل است، در صورت استفاده از مدلی تأییدنشده، اعتبارسنجی انجام نخواهد شد. این روش به نهاد ناظر اجازه می‌دهد بدون اجرای مجدد درخواست‌ها، ادعاهای ارائه‌دهنده را بررسی کند.

معرفی FlashProve؛ سامانه‌ای برای اثبات استنتاج مدل‌های بزرگ

در راستای توسعه این رویکرد، آنتروپیک سامانه متن‌باز FlashProve را معرفی کرده است. این سامانه یک نمونه اولیه برای استنتاج اثبات‌پذیر مدل‌های زبانی بزرگ مبتنی بر معماری «آمیخته خبرگان» (Mixture of Experts) یا MoE است. FlashProve از دو طرف تشکیل شده است: ارائه‌دهنده مدل که نقش اثبات‌کننده (Prover) را دارد و کاربر که نقش تأییدکننده (Verifier) را ایفا می‌کند.

فرایند کار سامانه در دو مرحله انجام می‌شود:

• مرحله آفلاین: ارائه‌دهنده مدلی را که قرار است اجرا کند، با استفاده از یک تعهد رمزنگاری‌شده مشخص می‌کند. این تعهد اثر انگشتی کوتاه از وزن‌های مدل است که امکان شناسایی دقیق آن‌ها را فراهم می‌کند، بدون اینکه وزن‌ها افشا شوند.
• مرحله آنلاین: پس از دریافت درخواست کاربر، شامل پرامپت و توکن‌های خروجی، ارائه‌دهنده یک فایل اثبات تولید می‌کند. این فایل نشان می‌دهد مدل متعهدشده، در صورت اجرا روی ورودی مشخص، دقیقاً همان توکن‌های خروجی را تولید می‌کند.

هر فردی که تعهد مدل، ورودی و پاسخ را در اختیار داشته باشد، می‌تواند اعتبار گواهی را بررسی کند؛ حتی اگر هیچ اطلاعی از وزن‌های مدل نداشته باشد.

راستی‌آزمایی با Lean

یکی از چالش‌های مهم در توسعه سامانه‌های رمزنگاری، شکنندگی و احتمال خطا در پیاده‌سازی آن‌هاست. برای افزایش اطمینان به امنیت FlashProve، از زبان و ابزار اثبات رسمی Lean استفاده شده است. در این روش، پروتکل و ویژگی‌های امنیتی آن به‌صورت گزاره‌های ریاضی تعریف می‌شوند و صحت آن‌ها با اثبات‌هایی قابل‌بررسی توسط ماشین تأیید می‌شود.

بااین‌حال، راستی‌آزمایی رسمی به‌تنهایی تمام مشکلات اعتماد را برطرف نمی‌کند. نخست، باید به‌صورت دستی بررسی شود که گزاره‌های رسمی دقیقاً همان ویژگی‌های امنیتی موردنظر را بیان می‌کنند. برای تسهیل این کار، یک ابزار تعاملی برای مشاهده و بررسی قضیه‌های Lean ارائه شده است.

دوم، باید اطمینان حاصل شود که کد اجرایی دقیقاً با پروتکلی مطابقت دارد که ویژگی‌های امنیتی آن به‌صورت رسمی اثبات شده‌اند. برای این منظور، دو اعتبارسنج ارائه شده است؛ یک نسخه سریع با زبان C++ و یک نسخه رسمی مبتنی بر Lean. نسخه Lean کندتر است، اما تضمین می‌کند فقط گواهی‌هایی را بپذیرد که با قضیه‌های امنیتی اثبات‌شده سازگار هستند. نسخه C++ برای استفاده روزمره مناسب‌تر است، اما تضمین رسمی مشابهی ندارد. این دو نسخه در تمام گواهی‌های آزمایش‌شده نتایج یکسانی داشته‌اند.

محدودیت‌های FlashProve

با وجود نتایج امیدوارکننده، FlashProve همچنان یک نمونه اولیه پژوهشی است و محدودیت‌هایی دارد:

1. نبود تضمین رسمی برای کد اجرایی سریع: نسخه Lean و اثبات‌های رسمی ارائه شده‌اند، اما تطابق کامل کد سریع C++، مقاله فنی و نسخه رسمی Lean تضمین نشده است.
2. محدودیت در نوع محاسبات مدل: اثبات‌ها بر مبنای نسخه صحیح (Integer) وزن‌های منتشرشده و روش Greedy Decoding انجام می‌شوند. بنابراین، خروجی نسخه‌های مبتنی بر محاسبات ممیز شناور یا روش‌های نمونه‌گیری ممکن است در برخی موقعیت‌ها با محاسبات اثبات‌شده تفاوت داشته باشد.
3. پنهان‌نشدن معماری مدل: سامانه وزن‌های مدل را مخفی می‌کند، اما معماری آن را پنهان نمی‌کند. طراحی فعلی برای بهره‌گیری از ساختار MoE بهینه شده است. امکان توسعه روش‌هایی برای پنهان‌سازی هم‌زمان معماری و وزن‌ها نیز مطرح شده، اما در این نسخه پیاده‌سازی نشده است.
4. حملات کانال جانبی: اگرچه خود گواهی اطلاعاتی درباره وزن‌ها افشا نمی‌کند، اندازه‌گیری زمان تولید گواهی یا سایر ویژگی‌های جانبی فرایند ممکن است اطلاعاتی درباره مدل آشکار کند. مقابله با این نوع حملات خارج از محدوده انتشار فعلی است.
5. محدودیت طول پنجره زمینه: FlashProve در حال حاضر استنتاج را برای زمینه‌هایی تا ۱۰۲۴ توکن اثبات می‌کند. این مقدار در مقایسه با پنجره‌های زمینه‌ای مدل‌های پیشرفته که می‌توانند به صدها هزار یا میلیون‌ها توکن برسند، محدود است.

دسترسی به FlashProve

FlashProve گامی در جهت عملیاتی‌کردن استنتاج اثبات‌پذیر برای مدل‌های زبانی بزرگ محسوب می‌شود. این سامانه نشان می‌دهد می‌توان با استفاده از روش‌های رمزنگاری دانش صفر، بدون افشای وزن‌های مدل، صحت اجرای آن را برای درخواست‌های مشخص تأیید کرد. کاربردهای این فناوری از افزایش اعتماد مشتریان به ارائه‌دهندگان مدل‌ها تا شناسایی دست‌کاری سرورها، اثبات منشأ خروجی‌ها و فراهم‌کردن ابزارهای نظارتی برای ارزیابان و نهادهای تنظیم‌گر گسترش می‌یابد.

انتشار متن‌باز کد در گیت‌هاب، مستندات پروتکل و اثبات‌های رسمی Lean نیز با هدف فراهم‌کردن امکان بررسی، توسعه و بهبود این فناوری توسط پژوهشگران دیگر انجام شده است. بااین‌حال، محدودیت‌هایی مانند سربار محاسباتی، طول زمینه و پنهان‌نشدن معماری مدل نشان می‌دهند که FlashProve هنوز یک راهکار کامل و آماده استقرار گسترده نیست.

هدف اصلی این پژوهش، نشان‌دادن امکان‌پذیری فنی اثبات رمزنگاری‌شده استنتاج در مقیاس مدل‌های بزرگ و فراهم‌کردن زیرساختی برای توسعه نسل بعدی ابزارهای اعتماد، امنیت و نظارت در اکوسیستم هوش مصنوعی است.