ڈيپ سيک (DeepSeek) نے پروور-V2 (Prover-V2) نامی ایک انقلابی اوپن سورس لارج لینگویج ماڈل (LLM) متعارف کرایا ہے، جو لین 4 (Lean 4) فریم ورک کے اندر رسمی تھیورم ثابت کرنے کے پیچیدہ ڈومین کے لیے بڑی احتیاط سے تیار کیا گیا ہے۔ یہ نیا ماڈل ڈيپ سيک کے جدید ترین ڈيپ سيک-V3 (DeepSeek-V3) فاؤنڈیشن ماڈل کی طاقت کو بروئے کار لاتے ہوئے، ایک تکراری تھیورم ثابت کرنے والے پائپ لائن کو استعمال کرتا ہے۔ لین 4، لین تھیورم پروور کا تازہ ترین ورژن ہے، جو مائیکروسافٹ ریسرچ (Microsoft Research) کے ذریعہ تیار کردہ ایک انٹرایکٹو پروف اسسٹنٹ ہے۔ یہ نفیس فنکشنل پروگرامنگ لینگویج اور انٹرایکٹو تھیورم ثابت کرنے کا نظام ریاضی دانوں اور کمپیوٹر سائنسدانوں کو بے مثال مشین چیکڈ تصدیق کے ساتھ رسمی ثبوت بنانے کی طاقت دیتا ہے۔
یہ پروجیکٹ رسمی اور غیر رسمی ریاضیاتی استدلال کے درمیان فرق کو ختم کرنے کی جانب ایک بڑا قدم ہے۔ جنرل پرپز ایل ایل ایمز کی موروثی صلاحیتوں سے فائدہ اٹھاتے ہوئے، یہ رسمی تھیورم ثابت کرنے کے انتہائی منظم ڈومین کو مؤثر طریقے سے حل کرنے کی کوشش کرتا ہے۔ ڈيپ سيک کی تحقیقی ٹیم کا دعویٰ ہے کہ ان کا اختراعی طریقہ کار انسانی ریاضی دانوں کے ثبوت تیار کرتے وقت استعمال ہونے والے علمی عمل کی عکاسی کرتا ہے، جس میں پیچیدہ تھیورمز کو زیادہ قابل انتظام اور قابل فہم اجزاء میں تقسیم کیا جاتا ہے۔
تشخیصي فريم ورک کو وسعت دينا: پروور بينچ کا تعارف
اپنی تحقیق کی سختی کو بڑھانے کے لیے ایک اہم اقدام میں، ڈيپ سيک ٹیم نے پروور بينچ (ProverBench) کے تعارف کے ساتھ اپنے تشخیصی فریم ورک کو نمایاں طور پر توسیع دی ہے، جو ایک بالکل نیا بینچ مارک مجموعہ ہے جسے خاص طور پر رسمی تھیورم ثابت کرنے کی صلاحیتوں کی جامع تشخیص کے لیے ڈیزائن کیا گیا ہے۔ یہ جامع مجموعہ رسمی ریاضی کے تناظر میں ایل ایل ایمز کی کارکردگی کا جائزہ لینے کے لیے ایک قیمتی وسیلہ کا کام کرتا ہے۔
محققین نے تفصیل سے بتایا کہ "روایتی بینچ مارکس سے آگے بڑھتے ہوئے، ہم اپنی تشخیص کے عمل کو تقویت دینے کے لیے 325 باقاعدہ مسائل کے ایک محتاط طریقے سے تیار کردہ مجموعہ پروور بینچ کو فخر سے متعارف کراتے ہیں۔ اس مجموعہ میں حالیہ امریکن انویٹیشنل میتھمیٹکس ایگزامینیشن (AIME) مقابلوں سے براہ راست حاصل کردہ 15 احتیاط سے منتخب کردہ مسائل شامل ہیں، خاص طور پر سال 24-25 سے۔"
پروور بینچ ڈیٹا سیٹ میں اے آئی ایم ای (AIME) کے مسائل کا شمولیت خاص طور پر قابل ذکر ہے، کیونکہ یہ چیلنجنگ اور اچھی طرح سے قائم ریاضیاتی مسائل کا ایک مجموعہ متعارف کراتا ہے جو математиاتی کمیونٹی میں بڑے پیمانے پر تسلیم شدہ ہیں۔ یہ ڈيپ سيک پروور-V2 کی کارکردگی کا جائزہ لینے اور اس کا دوسرے طریقوں سے موازنہ کرنے کے لیے ایک معیاری اور سخت بنیاد فراہم کرتا ہے۔
وعدہ کرنے والے ابتدائی نتائج: اے آئی ایم ای (AIME) کے مسائل سے نمٹنا
ان چیلنجنگ اے آئی ایم ای (AIME) مسائل پر سخت جانچ سے حاصل ہونے والے ابتدائی نتائج نے ان کے احتیاط سے ڈیزائن کردہ خصوصی تھیورم ثابت کرنے والے ماڈل سے غیر معمولی طور پر امید افزا کارکردگی کا انکشاف کیا ہے۔ ڈيپ سيک ٹیم نے فخر سے رپورٹ کیا کہ ڈيپ سيک پروور-V2 نے اسے پیش کردہ 15 اے آئی ایم ای (AIME) مسائل میں سے 6 کو کامیابی سے حل کرکے اپنی صلاحیت کا مظاہرہ کیا۔ اس کے مقابلے میں، جنرل پرپز ڈيپ سيک-V3 ماڈل (DeepSeek-V3 model) نے، جب اکثریتی ووٹنگ کی تکنیکوں کا استعمال کیا، 8 مسائل کو کامیابی سے حل کرنے میں کامیابی حاصل کی۔
یہ نتائج پیچیدہ ریاضیاتی مسائل سے نمٹنے میں خصوصی اور جنرل پرپز دونوں اقسام کے ایل ایل ایمز کی صلاحیت کو اجاگر کرتے ہیں۔ اگرچہ جنرل پرپز ماڈل نے اس خاص بینچ مارک میں قدرے زیادہ کامیابی کی شرح کا ثبوت دیا، خصوصی تھیورم ثابت کرنے والے ماڈل نے رسمی математиاتی استدلال میں اپنی مہارت کا مظاہرہ کیا۔
انسانی ثبوت کی تعمیر کی نقل تیار کرنا: ایک سلسلہِ فکر کا طریقہ
ڈيپ سيک ٹیم نے تفصیل سے بتایا کہ "جنرل پرپز ماڈلز کو مکمل لین ثبوت تیار کرنے کی کوشش کرتے وقت اکثر جن چیلنجوں کا سامنا کرنا پڑتا ہے، اس کے پیش نظر، ہم نے حکمت عملی کے ساتھ ڈيپ سيک-V3 کو صرف ایک اعلیٰ سطحی ثبوت خاکہ تیار کرنے کی ہدایت کی، جان بوجھ کر پیچیدہ تفصیلات کو خارج کر دیا۔ اس کے نتیجے میں فکر کا سلسلہ لین تھیورم پر منتج ہوتا ہے جو ہیو (have) بیانات کے ایک سلسلے پر مشتمل ہوتا ہے، ہر ایک کو بڑی احتیاط سے افسوس (sorry) کے پلیس ہولڈر کے ساتھ ختم کیا جاتا ہے، جو مؤثر طریقے سے ایک ذیلی مقصد کی نشاندہی کرتا ہے جسے حل کرنے کی ضرورت ہے۔ یہ اختراعی طریقہ انسانی انداز کے ثبوت کی تعمیر کو خوبصورتی سے پیش کرتا ہے، جس میں ایک پیچیدہ تھیورم کو بتدریج زیادہ قابل انتظام لیماز کے سلسلے میں کم کیا جاتا ہے۔"
اعلیٰ سطحی ثبوت خاکے تیار کرنے کا یہ اختراعی طریقہ اس بات سے ہم آہنگ ہے کہ математиisasi اکثر پیچیدہ ثبوتوں سے کیسے رجوع کرتے ہیں۔ مجموعی ساخت اور اہم مراحل پر توجہ مرکوز کرکے، ماڈل مؤثر طریقے سے ثبوت کی بعد میں تطہیر اور تکمیل کی رہنمائی کرسکتا ہے۔
ایک منظم حکمت عملی: ہر ثبوت کے جزو کو انفرادی طور پر مخاطب کرنا
پھر یہ نظام ثبوت کے ہر انفرادی جزو کو مخاطب کرنے کے لیے ایک باقاعدگی اور منظم حکمت عملی کو بڑی احتیاط سے استعمال کرتا ہے۔ یہ منظم طریقہ کار اس بات کو یقینی بناتا ہے کہ ثبوت کے ہر پہلو پر احتیاط سے غور کیا جائے اور اس کو منطقی اور مربوط انداز میں مخاطب کیا جائے۔ یہ نظام تھیورم ثابت کرنے کے لیے ایک انتہائی منظم طریقہ تیار کرتا ہے، پہلے سے قائم شدہ نتائج پر تعمیر کرتے ہوئے ہر بعد کے مرحلے کے لیے ایک ٹھوس بنیاد کو یقینی بناتا ہے۔
محققین نے تفصیل سے بتایا کہ "ڈيپ سيک-V3 کے ذریعہ تیار کردہ ذیلی مقاصد سے فائدہ اٹھاتے ہوئے، ہم ہر درمیانی ثبوت مرحلے کو منظم طریقے سے حل کرنے کے لیے ایک تکراری حل کرنے کی حکمت عملی اپناتے ہیں۔ ہم دیے گئے مسائل میں اصل مقاصد کے بدلے ذیلی مقصد کے اظہار کو ہیو (have) بیانات سے نکالتے ہیں اور پھر پچھلے ذیلی مقاصد کو بنیاد کے طور پر شامل کرتے ہیں۔ یہ تعمیر بعد کے ذیلی مقاصد کو پہلے مراحل کے درمیانی نتائج کا استعمال کرکے حل کرنے کے قابل بناتی ہے، اس طرح ایک زیادہ مقامی انحصار کی ساخت کو فروغ ملتا ہے اور آسان لیماز کی ترقی میں سہولت ملتی ہے۔"
تکراری حل کرنے کی حکمت عملی نظام کی پیچیدہ ثبوتوں کو سنبھالنے کی صلاحیت کا ایک اہم پہلو ہے۔ اس مسئلے کو چھوٹے، زیادہ قابل انتظام ذیلی مقاصد میں توڑ کر، یہ نظام ہر انفرادی جزو پر مؤثر طریقے سے اپنی استدلال کی صلاحیتوں کا اطلاق کرسکتا ہے۔
کمپیوٹیشنل وسائل کو بہتر بنانا: ایک خصوصی 7B پیرامیٹر ماڈل
کمپیوٹیشنل وسائل کو مؤثر طریقے سے بہتر بنانے اور موثر پروسیسنگ کو یقینی بنانے کے لیے، یہ نظام حکمت عملی کے ساتھ ٹکڑے ٹکڑے کیے گئے لیماز کو پروسیس کرنے کے لیے ایک چھوٹا، انتہائی خاص 7B پیرامیٹر ماڈل استعمال کرتا ہے۔ یہ نقطہ نظر وسیع ثبوت کی تلاش سے وابستہ computational مطالبات کو مؤثر طریقے سے منظم کرنے کے لیے بہت ضروری ہے، اس بات کو یقینی بناتے ہوئے کہ یہ نظام تلاش کی جگہ کی پیچیدگیوں سے مغلوب ہوئے بغیر موثر طریقے سے کام کرسکے۔ یہ نقطہ نظر بالآخر خود بخود اخذ کردہ مکمل ثبوت پر منتج ہوتا ہے جب تمام ٹکڑے ٹکڑے کیے گئے مراحل کامیابی سے حل ہوجاتے ہیں۔
محققین نے بیان کیا کہ "الگورتھمک فریم ورک دو الگ الگ مراحل میں کام کرتا ہے، جو دو تکمیلی ماڈلز سے فائدہ اٹھاتا ہے: لیما ٹکڑے ٹکڑے کرنے کے لیے ڈيپ سيک-V3 اور متعلقہ رسمی ثبوت کی تفصیلات مکمل کرنے کے لیے ایک 7B پروور ماڈل۔"
یہ دو مرحلوں والا نقطہ نظر نظام کو ایک بڑے جنرل پرپز ماڈل اور ایک چھوٹے خصوصی ماڈل دونوں کی طاقتوں سے فائدہ اٹھانے کی اجازت دیتا ہے۔ بڑا ماڈل اعلیٰ سطحی ثبوت خاکے تیار کرنے کے لیے استعمال ہوتا ہے، جب کہ چھوٹا ماڈل تفصیلات کو پُر کرنے اور رسمی ثبوت کو مکمل کرنے کے لیے استعمال ہوتا ہے۔
رسمی استدلال کے اعداد و شمار کو ترکیب دینا: ایک قدرتی راستہ
یہ احتیاط سے ڈیزائن کردہ فن تعمیر رسمی استدلال کے اعداد و شمار کو ترکیب کرنے کے لیے مؤثر طریقے سے ایک قدرتی اور بدیہی راستہ قائم کرتا ہے، اعلیٰ سطحی математиاتی استدلال کو باقاعدگی سے اور رسمی تصدیق کی سخت ضروریات کے ساتھ بغیر کسی رکاوٹ کے ضم کرتا ہے۔ یہ انضمام نظام کے نتائج کی وشوسنییتا اور قابل اعتماد کو یقینی بنانے کے لیے ضروری ہے۔
محققین نے وضاحت کی کہ "ہم مشکل مسائل کا ایک ذیلی مجموعہ تیار کرتے ہیں جو آخر سے آخر تک طریقے سے 7B پروور ماڈل کے ذریعہ حل نہیں ہوتے ہیں، لیکن جن کے لیے تمام ٹکڑے ٹکڑے کیے گئے ذیلی مقاصد کو کامیابی سے حل کیا گیا ہے۔ تمام ذیلی مقاصد کے ثبوت مرتب کرکے، ہم اصل مسئلے کے لیے ایک مکمل رسمی ثبوت تیار کرتے ہیں۔"
یہ نقطہ نظر نظام کو اپنی غلطیوں سے سیکھنے اور پیچیدہ مسائل کو حل کرنے کی اپنی صلاحیت کو بہتر بنانے کی اجازت دیتا ہے۔ ان مخصوص ذیلی مقاصد کی نشاندہی کرکے جو مشکلات کا باعث بن رہے ہیں، یہ نظام ان علاقوں میں اپنی کارکردگی کو بہتر بنانے پر اپنی کوششوں کو مرکوز کرسکتا ہے۔
خدشات اور چیلنجز: نفاذ کی تفصیلات زیرِ تفتیش
ڈيپ سيک پروور-V2 کے ذریعہ ظاہر کی گئی ناقابل تردید تکنیکی کامیابیوں کے باوجود، فیلڈ کے کچھ ماہرین نے نفاذ کی بعض تفصیلات کے بارے میں متعلقہ خدشات اٹھائے ہیں۔ Epoch AI میں ایک انتہائی معزز لیڈ математиisasi ایلیٹ گلیزر (Elliot Glazer) نے ممکنہ مسائل کی نشاندہی کی ہے جو مزید تحقیقات کا مطالبہ کرتے ہیں۔
ڈيپ سيک پروور-V2 پیپر کے بارے میں کچھ خدشات۔ ممکنہ طور پر غلط رسمی شکل دیئے گئے مثالیں، اور لین (Lean) zulip پر بحث سے پتہ چلتا ہے کہ پٹنم بینچ (PutnamBench) کے ثبوت بکواس ہیں اور ایک مضمر افسوس (sorry) (ممکنہ طور پر اپلائی؟ تدبیر میں پوشیدہ ہے) استعمال کرتے ہیں جس کی اطلاع ان کے پڑھنے-تشخیص-پرنٹ لوپ میں نہیں ہے۔
یہ خدشات باقاعدگی سے تصدیق کی جگہ میں شامل جاری چیلنجوں کو واضح طور پر اجاگر کرتے ہیں، جہاں حتیٰ کہ چھوٹی اور بظاہر غیر اہم نفاذ کی تفصیلات بھی نتائج کی مجموعی درستگی اور وشوسنییتا پر غیر متناسب طور پر بڑا اثر ڈال سکتی ہیں۔ باقاعدگی سے تصدیق کے عمل میں تفصیل پر غیر متزلزل توجہ اور قائم کردہ معیارات پر سخت عمل درآمد کی ضرورت ہوتی ہے۔
غلط رسمی شکل دیئے گئے مثالوں کا امکان اور پٹنم بینچ (PutnamBench) کے ثبوتوں میں پوشیدہ “افسوس” کی تدبیروں کا امکان تصدیق کے عمل کی سختی اور تکمیل کے بارے میں اہم سوالات اٹھاتا ہے۔ یہ خدشات نتائج کی مسلسل جانچ پڑتال اور آزادانہ تصدیق کی ضرورت پر زور دیتے ہیں۔
دستیابی اور وسائل: رسمی تھیورم ثابت کرنے تک رسائی کو جمہوری بنانا
ڈيپ سيک نے اپنے پروور-V2 کو دو مخصوص ماڈل سائز میں دستیاب کرایا ہے، جو کمپیوٹیشنل وسائل اور تحقیقی مقاصد کی متنوع رینج کو پورا کرتا ہے۔ پہلا ورژن ان کے پچھلے پروور-V1.5-بیس (Prover-V1.5-Base) پر بنایا گیا ایک 7B پیرامیٹر ماڈل ہے، جس میں 32K ٹوکنز تک کی توسیع شدہ سیاق و سباق کی لمبائی ہے۔ دوسرا ورژن ڈيپ سيک-V3-بیس (DeepSeek-V3-Base) پر تربیت یافتہ ایک نمایاں طور پر بڑا 671B پیرامیٹر ماڈل ہے۔ دونوں ماڈلز اب ہگنگ فیس (HuggingFace) پر آسانی سے دستیاب ہیں، جو مشین لرننگ ماڈلز کو بانٹنے اور ان پر تعاون کرنے کے لیے ایک معروف پلیٹ فارم ہے۔
ماڈلز کے علاوہ، ڈيپ سيک نے مکمل پروور بینچ ڈیٹا سیٹ (ProverBench dataset) بھی ہگنگ فیس (HuggingFace) پر دستیاب کرایا ہے، جس میں تشخیصی مقاصد کے لیے 325 احتیاط سے باقاعدہ شکل دیئے گئے مسائل ہیں۔ یہ جامع ڈیٹا سیٹ محققین اور ڈویلپرز کو اپنے ماڈلز کی کارکردگی کا جائزہ لینے اور ڈيپ سيک پروور-V2 سے ان کا موازنہ کرنے کے لیے ایک قیمتی وسیلہ فراہم کرتا ہے۔
ان وسائل کو مفت میں دستیاب کروا کر، ڈيپ سيک رسمی تھیورم ثابت کرنے والی ٹکنالوجی تک رسائی کو جمہوری بنا رہا ہے اور تحقیقی کمیونٹی میں تعاون کو فروغ دے رہا ہے۔ یہ اوپن سورس نقطہ نظر اس فیلڈ میں ترقی کو تیز کرنے اور خودکار استدلال اور تصدیق میں نئی پیش رفت کا باعث بننے کا امکان ہے۔
یہ ریلیز محققین اور ڈویلپرز کو اس ٹکنالوجی کی صلاحیتوں اور حدود میں جانے کے لیے درکار وسائل سے بااختیار بناتی ہے۔ ماڈلز اور پروور بینچ ڈیٹا سیٹ (ProverBench dataset) تک کھلی رسائی فراہم کرکے، ڈيپ سيک فیلڈ میں ماہرین کے اٹھائے گئے خدشات کو دور کرنے کے لیے مزید ریسرچ اور باہمی تعاون کی کوششوں کی حوصلہ افزائی کرتا ہے۔ باہمی تعاون کے اس نقطہ نظر میں رسمی تھیورم ثابت کرنے کی پیچیدگیوں کو کھولنے اور ان جدید پیش رفتوں کے اعتبار کو مستحکم کرنے کی کلید ہے۔