معرفی Prover V2
شرکت توسعه هوش مصنوعی چینی DeepSeek مدل جدید متنباز با وزن آزاد (open-weight) خود را منتشر کرد. این شرکت مدل جدید Prover V2 را در تاریخ ۳۰ آوریل در سرویس هاستینگ Hugging Face بارگذاری کرد. این نسخه جدید که تحت مجوز آزاد MIT عرضه شده، با هدف بررسی و تأیید اثباتهای ریاضی توسعه یافته است.
ویژگیها و حجم مدل
Prover V2 دارای ۶۷۱ میلیارد پارامتر است و بهطور قابلتوجهی بزرگتر از نسخههای قبلی خود Prover V1 و Prover V1.5 است که در اوت ۲۰۲۴ منتشر شدند. مقاله همراه نسخه اول توضیح میداد که این مدل برای تبدیل مسائل رقابتهای ریاضی به منطق صوری با استفاده از زبان برنامهنویسی Lean ۴ — ابزاری رایج در اثبات قضایا — آموزش داده شده بود. سازندگان میگویند Prover V2 دانش ریاضی را در قالبی فشرده ذخیره میکند تا بتواند اثباتها را تولید و تأیید کند و بدینترتیب به تحقیق و آموزش کمک کند.
چالشهای سختافزاری
بهطور کلی، در فضای هوش مصنوعی به مدلها بهصورت غیررسمی «وزنها» گفته میشود؛ منظور فایل یا مجموعه فایلهایی است که امکان اجرای محلی یک AI را بدون تکیه بر سرورهای خارجی فراهم میکنند. مدلهای پیشرفته نیاز به سختافزارهایی دارند که اکثر افراد به آن دسترسی ندارند، زیرا این مدلها دارای تعداد پارامتر زیادی هستند که در نتیجه حجم فایلها و نیاز به RAM یا VRAM و قدرت پردازش بالایی دارند.
فشردهسازی با کوانتیزاسیون
مدل جدید Prover V2 حدود ۶۵۰ گیگابایت حجم دارد و انتظار میرود از RAM یا VRAM اجرا شود. برای رسیدن به این اندازه، «وزن»های Prover V2 با دقت ممیز شناور ۸ بیتی کوانتیزه شدهاند؛ بدین معنی که هر پارامتر تقریباً نصف فضای معمول ۱۶ بیتی را اشغال میکند و در عمل حجم مدل را نصف میکند.
نسخ قبلی Prover
Prover V1 بر پایه مدل DeepSeekMath با هفت میلیارد پارامتر ساخته شده و روی دادههای مصنوعی آموزش دیده بود. دادههای مصنوعی به دادههایی گفته میشود که برای آموزش مدلهای هوش مصنوعی خود توسط مدلهای AI تولید شدهاند و معمولاً دادههای تولیدشده توسط انسان منبعی گرانبها و کمیاب برای دادههای با کیفیت بالاتر محسوب میشوند. در نسخه Prover V1.5 با بهینهسازی مراحل آموزش و اجرا دقت بالاتری در بنچمارکها به دست آمد.
نحوه ارتباط با مدل R1
تا زمان نگارش این مقاله، اطلاعات دقیقی درباره بهبودهای Prover V2 منتشر نشده است، اما تعداد پارامترهای آن نشان میدهد که احتمالاً مبتنی بر مدل R1 شرکت باشد. وقتی R1 برای اولین بار عرضه شد، عملکردی برابر با بهترین مدل آن زمان یعنی o1 از OpenAI داشت.
بحثهای دسترسی آزاد و امنیت
انتشار عمومی وزنهای LLM موضوعی بحثبرانگیز است. از یک سو دسترسی آزاد را تسهیل میکند و به کاربران امکان میدهد بدون تکیه بر زیرساخت شرکتهای خصوصی، AI را بهصورت محلی اجرا کنند. از سوی دیگر شرکتها نمیتوانند برای جلوگیری از سوءاستفاده از مدل محدودیتهایی اعمال کنند. انتشار R1 نگرانیهای امنیتی را برانگیخت و برخی از آن بهعنوان «لحظه اسپوتنیک چین» یاد کردند. طرفداران متنباز خوشحال بودند که DeepSeek ادامهدهنده راه Meta در انتشار سری LLaMA است و نشان داد AI متنباز رقیبی جدی برای AI بسته OpenAI است.
روشهای کمحجمسازی: Distillation و Quantization
دسترسی به مدلهای LLM اکنون آسانتر شده و حتی کاربرانی که به ابررایانههای گرانقیمت دسترسی ندارند، میتوانند مدلها را بهصورت محلی اجرا کنند. این امر عمدتاً مدیون دو تکنیک توسعه AI به نامهای distillation و quantization است. Distillation به معنای آموزش یک شبکه کوچکتر «دانشجو» برای تقلید رفتار یک مدل بزرگتر «معلم» است تا بیشترین عملکرد حفظ شود و همزمان پارامترها کاهش یابند. Quantization شامل کاهش دقت عددی وزنها و فعالسازیها (activations) برای کاهش حجم و افزایش سرعت اجرا با کمترین افت دقت است. مثال آن کوانتیزاسیون Prover V2 از ۱۶ به ۸ بیت است، اما با نصف کردن تعداد بیتها میتوان بیشتر حجم را کاهش داد. هر دو تکنیک تأثیراتی بر عملکرد مدل دارند، ولی معمولاً مدل را تا حد زیادی عملیاتی نگه میدارند.
نسخههای کوچکتر R1
نسخه R1 DeepSeek با distillation به مدلهای مبتنی بر LLaMA و Qwen با پارامترهای ۷۰ میلیارد تا ۱.5 میلیارد پارامتر تبدیل شد. کوچکترین این مدلها حتی روی برخی دستگاههای موبایل نیز قابل اجرا هستند.