ডিপসিক প্রোভার-ভি২: একটি ওপেন সোর্স এলএলএম বিপ্লব

ডিপসিক প্রোভার-ভি২: আনুষ্ঠানিক গাণিতিক প্রমাণে একটি ওপেন সোর্স এলএলএম বিপ্লব

ডিপসিক, DeepSeek-Prover-V2 அறிமுகப்படுத்தியுள்ளது, যা একটি গ্রাউন্ডব্রেকিং ওপেন-সোর্স বৃহৎ ভাষা মডেল (LLM)। এটি জটিল আনুষ্ঠানিক উপপাদ্য প্রমাণের জন্য লীন ৪ কাঠামোর মধ্যে বিশেষভাবে তৈরি করা হয়েছে। এই নতুন মডেলটি একটি রিকার্সিভ উপপাদ্য প্রমাণ পাইপলাইন ব্যবহার করে, যা ডিপসিকের অত্যাধুনিক ডিপসিক-ভি৩ ফাউন্ডেশন মডেলের শক্তিকে কাজে লাগায়। লীন ৪ হলো লীন উপপাদ্য প্রমাণকারীর সর্বশেষ সংস্করণ, যা মাইক্রোসফট রিসার্চ দ্বারা নির্মিত একটি ইন্টারেক্টিভ প্রমাণ সহকারী। এই অত্যাধুনিক ফাংশনাল প্রোগ্রামিং ভাষা এবং ইন্টারেক্টিভ উপপাদ্য প্রমাণ ব্যবস্থা গণিতবিদ ও কম্পিউটার বিজ্ঞানীদের অভূতপূর্ব মেশিন-চেকড যাচাইকরণের মাধ্যমে আনুষ্ঠানিক প্রমাণ তৈরি করতে সক্ষম করে।

এই প্রকল্পটি আনুষ্ঠানিক এবং অনানুষ্ঠানিক গাণিতিক যুক্তির মধ্যে ব্যবধান কমিয়ে আনার ক্ষেত্রে একটি গুরুত্বপূর্ণ পদক্ষেপ। সাধারণ উদ্দেশ্যে ব্যবহৃত এলএলএম-এর অন্তর্নিহিত ক্ষমতাকে কাজে লাগিয়ে, এটি আনুষ্ঠানিক উপপাদ্য প্রমাণের অত্যন্ত সুগঠিত ক্ষেত্রকে কার্যকরভাবে মোকাবেলা করতে চায়। ডিপসিক গবেষণা দলের মতে, তাদের উদ্ভাবনী পদ্ধতি মানুষের গণিতবিদদের প্রমাণ নির্মাণের সময় ব্যবহৃত জ্ঞানীয় প্রক্রিয়াগুলোকে প্রতিফলিত করে। যেখানে জটিল উপপাদ্যগুলোকে আরও সহজবোধ্য অংশে বিভক্ত করা হয়।

Evaluation Framework-এর বিস্তার: ProverBench-এর আত্মপ্রকাশ

ডিপসিক দল তাদের গবেষণার কঠোরতা বাড়ানোর জন্য একটি উল্লেখযোগ্য পদক্ষেপ নিয়েছে। তারা ProverBench নামে একটি নতুন বেঞ্চমার্ক কালেকশন চালু করেছে। এই কালেকশনটি বিশেষভাবে আনুষ্ঠানিক উপপাদ্য প্রমাণের ক্ষমতা মূল্যায়নের জন্য ডিজাইন করা হয়েছে। এই বিস্তৃত সংগ্রহটি আনুষ্ঠানিক গণিতের প্রেক্ষাপটে এলএলএম-এর কর্মক্ষমতা মূল্যায়নের জন্য একটি মূল্যবান উৎস হিসেবে কাজ করে।

গবেষকরা জানান, "ঐতিহ্যবাহী বেঞ্চমার্কের বাইরে, আমরা গর্বের সাথে ProverBench উপস্থাপন করছি। এটি ৩২৫টি আনুষ্ঠানিক সমস্যা নিয়ে গঠিত, যা আমাদের মূল্যায়ন প্রক্রিয়াকে সমৃদ্ধ করবে। এই সংগ্রহে আমেরিকান ইনভিটেশনাল ম্যাথমেটিক্স পরীক্ষার (AIME) থেকে ১৫টি সমস্যা নেওয়া হয়েছে, যা বিশেষভাবে ২৪-২৫ সালের প্রতিযোগিতা থেকে নির্বাচন করা হয়েছে।”

ProverBench ডেটাসেটে AIME সমস্যাগুলোর অন্তর্ভুক্তি বিশেষভাবে উল্লেখযোগ্য। এটি চ্যালেঞ্জিং এবং সুপ্রতিষ্ঠিত গাণিতিক সমস্যা সরবরাহ করে, যা গাণিতিক সম্প্রদায়ে ব্যাপকভাবে স্বীকৃত। এটি DeepSeek-Prover-V2-এর কর্মক্ষমতা মূল্যায়ন এবং অন্যান্য পদ্ধতির সাথে তুলনা করার জন্য একটি মানসম্মত এবং কঠোর ভিত্তি প্রদান করে।

প্রাথমিক প্রতিশ্রুতিশীল ফলাফল: AIME সমস্যা মোকাবেলা

এই চ্যালেঞ্জিং AIME সমস্যাগুলোর ওপর কঠোর পরীক্ষার প্রাথমিক ফলাফল তাদের বিশেষভাবে ডিজাইন করা উপপাদ্য প্রমাণ মডেল থেকে ব্যতিক্রমী প্রতিশ্রুতি দেখিয়েছে। ডিপসিক দল গর্বের সাথে জানায় যে DeepSeek-Prover-V2 ১৫টি AIME সমস্যার মধ্যে ৬টি সফলভাবে সমাধান করতে সক্ষম হয়েছে। অন্যদিকে, সাধারণ উদ্দেশ্যে ব্যবহৃত DeepSeek-V3 মডেল, যখন সংখ্যাগরিষ্ঠ ভোটদানের কৌশল ব্যবহার করে, তখন ৮টি সমস্যা সফলভাবে সমাধান করতে পেরেছিল।

এই ফলাফলগুলো জটিল গাণিতিক সমস্যা মোকাবেলায় বিশেষ এবং সাধারণ উদ্দেশ্যে ব্যবহৃত এলএলএম উভয়ের সম্ভাবনাই তুলে ধরে। যদিও সাধারণ উদ্দেশ্যে ব্যবহৃত মডেলটি এই বিশেষ বেঞ্চমার্কে সামান্য বেশি সাফল্য দেখিয়েছে, তবে বিশেষ উপপাদ্য প্রমাণ মডেলটি আনুষ্ঠানিক গাণিতিক যুক্তিতে তার দক্ষতা প্রদর্শন করেছে।

মানুষের প্রমাণ নির্মাণের অনুকরণের চেষ্টা: চেইন-অফ-থট অ্যাপ্রোচ

ডিপসিক দল আরও জানায়, "সাধারণ উদ্দেশ্যে ব্যবহৃত মডেলগুলো প্রায়শই সম্পূর্ণ লীন প্রমাণ তৈরি করতে গিয়ে যে সমস্যার সম্মুখীন হয়, তা বিবেচনা করে আমরা কৌশলগতভাবে DeepSeek-V3-কে শুধুমাত্র একটি উচ্চ-স্তরের প্রমাণের রূপরেখা তৈরি করার নির্দেশ দিয়েছিলাম। যেখানে জটিল বিষয়গুলো ইচ্ছাকৃতভাবে বাদ দেওয়া হয়েছে। এর ফলে একটি চেইন অফ থট তৈরি হয়েছে। যেখানে লীন উপপাদ্যটি কতগুলো ‘হ্যাভ’ স্টেটমেন্ট নিয়ে গঠিত। প্রতিটি স্টেটমেন্ট একটি ‘সরি’ প্লেসহোল্ডার দিয়ে শেষ হয়, যা সমাধান করা প্রয়োজন এমন একটি উপ-লক্ষ্য নির্দেশ করে। এই উদ্ভাবনী পদ্ধতিটি মানুষের প্রমাণ নির্মাণের শৈলীকে সুন্দরভাবে প্রতিফলিত করে। যেখানে একটি জটিল উপপাদ্যকে ধীরে ধীরে আরও সহজবোধ্য লেমাতে রূপান্তরিত করা হয়।”

উচ্চ-স্তরের প্রমাণের রূপরেখা তৈরি করার এই উদ্ভাবনী পদ্ধতিটি গণিতবিদরা কীভাবে জটিল প্রমাণের কাছে যান তার সাথে সামঞ্জস্যপূর্ণ। সামগ্রিক কাঠামো এবং মূল পদক্ষেপগুলোর ওপর মনোযোগ কেন্দ্রীভূত করে, মডেলটি কার্যকরভাবে প্রমাণের পরবর্তী পরিমার্জন এবং সমাপ্তির দিকনির্দেশনা দিতে পারে।

একটি নিয়মতান্ত্রিক কৌশল: প্রতিটি প্রমাণ উপাদানের পৃথকভাবে সম্বোধন

সিস্টেমটি তখন প্রমাণের প্রতিটি উপাদানের জন্য একটি নিয়মতান্ত্রিক এবং সুগঠিত কৌশল ব্যবহার করে। এই নিয়মতান্ত্রিক পদ্ধতি নিশ্চিত করে যে প্রমাণের প্রতিটি দিক সাবধানে বিবেচনা করা হয়েছে এবং একটি যুক্তিযুক্ত এবং সুসংগত পদ্ধতিতে সমাধান করা হয়েছে। উপপাদ্য প্রমাণের জন্য সিস্টেমটি একটি অত্যন্ত সুগঠিত পদ্ধতি তৈরি করে, যা পূর্বের প্রতিষ্ঠিত ফলাফলগুলোর ওপর ভিত্তি করে প্রতিটি পরবর্তী ধাপের জন্য একটি শক্ত ভিত্তি নিশ্চিত করে।

গবেষকরা আরও বলেন, "DeepSeek-V3 দ্বারা তৈরি করা উপ-লক্ষ্যগুলো ব্যবহার করে, আমরা প্রতিটি মধ্যবর্তী প্রমাণ পদক্ষেপকে নিয়মতান্ত্রিকভাবে সমাধান করার জন্য একটি রিকার্সিভ সমাধান কৌশল গ্রহণ করি। আমরা হ্যাভ স্টেটমেন্ট থেকে উপ-লক্ষ্য অভিব্যক্তিগুলো বের করি এবং প্রদত্ত সমস্যাগুলোতে মূল লক্ষ্যের পরিবর্তে সেগুলো প্রতিস্থাপন করি। এরপর পূর্ববর্তী উপ-লক্ষ্যগুলোকে ভিত্তি হিসেবে অন্তর্ভুক্ত করি। এই কাঠামো পরবর্তী উপ-লক্ষ্যগুলোকে আগের ধাপগুলোর মধ্যবর্তী ফলাফল ব্যবহার করে সমাধান করতে সক্ষম করে। এর ফলে একটি স্থানীয় নির্ভরতা কাঠামো তৈরি হয় এবং সহজ লেমার বিকাশ সহজতর হয়।”

রিকার্সিভ সমাধান কৌশলটি জটিল প্রমাণগুলো পরিচালনা করার জন্য সিস্টেমের ক্ষমতার একটি গুরুত্বপূর্ণ দিক। সমস্যাটিকে ছোট, আরও সহজে পরিচালনাযোগ্য উপ-লক্ষ্যে বিভক্ত করে, সিস্টেমটি প্রতিটি পৃথক উপাদানের ওপর তার যুক্তিবোধ কার্যকরভাবে প্রয়োগ করতে পারে।

কম্পিউটেশনাল রিসোর্স অপটিমাইজ করা: একটি বিশেষ ৭বি প্যারামিটার মডেল

কম্পিউটেশনাল রিসোর্স কার্যকরভাবে অপটিমাইজ করার জন্য এবং দক্ষ প্রক্রিয়াকরণ নিশ্চিত করতে, সিস্টেমটি কৌশলগতভাবে একটি ছোট, বিশেষভাবে তৈরি করা ৭বি প্যারামিটার মডেল ব্যবহার করে। এই পদ্ধতিটি ব্যাপক প্রমাণ অনুসন্ধানের সাথে জড়িত কম্পিউটেশনাল চাহিদাগুলো কার্যকরভাবে পরিচালনার জন্য অত্যন্ত গুরুত্বপূর্ণ। এটি নিশ্চিত করে যে সিস্টেমটি অনুসন্ধানের জটিলতা দ্বারা অভিভূত না হয়ে দক্ষতার সাথে কাজ করতে পারে। এই পদ্ধতিটি স্বয়ংক্রিয়ভাবে একটি সম্পূর্ণ প্রমাণ তৈরি করে, যখন সমস্ত বিভক্ত ধাপ সফলভাবে সমাধান করা হয়।

গবেষকরা বর্ণনা করেন, "অ্যালগরিদমিক কাঠামো দুটি স্বতন্ত্র পর্যায়ে কাজ করে, যা দুটি পরিপূরক মডেল ব্যবহার করে: লেমা ডিকম্পোজিশনের জন্য DeepSeek-V3 এবং সংশ্লিষ্ট আনুষ্ঠানিক প্রমাণের বিশদ বিবরণ সম্পূর্ণ করতে একটি ৭বি প্রুভার মডেল।”

এই দ্বি-পর্যায়ের পদ্ধতিটি সিস্টেমকে একটি বৃহৎ সাধারণ উদ্দেশ্যে ব্যবহৃত মডেল এবং একটি ছোট বিশেষ মডেলের শক্তি ব্যবহার করতে দেয়। বৃহৎ মডেলটি উচ্চ-স্তরের প্রমাণের রূপরেখা তৈরি করতে ব্যবহৃত হয়, যখন ছোট মডেলটি বিশদ পূরণ করতে এবং আনুষ্ঠানিক প্রমাণ সম্পূর্ণ করতে ব্যবহৃত হয়।

আনুষ্ঠানিক যুক্তির ডেটা সংশ্লেষণ: একটি স্বাভাবিক পথ

এই সতর্কতার সাথে ডিজাইন করা আর্কিটেকচার কার্যকরভাবে আনুষ্ঠানিক যুক্তির ডেটা সংশ্লেষণের জন্য একটি স্বাভাবিক এবং স্বজ্ঞাত পথ তৈরি করে। উচ্চ-স্তরের গাণিতিক যুক্তির সাথে আনুষ্ঠানিক যাচাইকরণের কঠোর প্রয়োজনীয়তাগুলোকে নির্বিঘ্নে একত্রিত করে। এই একীকরণ সিস্টেমের ফলাফলগুলোর নির্ভরযোগ্যতা এবং বিশ্বাসযোগ্যতা নিশ্চিত করার জন্য অপরিহার্য।

গবেষকরা ব্যাখ্যা করেন, "আমরা চ্যালেঞ্জিং সমস্যাগুলোর একটি উপসেট তৈরি করি, যা ৭বি প্রুভার মডেল দ্বারা এন্ড-টু-এন্ড পদ্ধতিতে সমাধান করা যায়নি। তবে যেগুলোর জন্য সমস্ত বিভক্ত উপ-লক্ষ্য সফলভাবে সমাধান করা হয়েছে। সমস্ত উপ-লক্ষ্যের প্রমাণগুলো একত্রিত করে, আমরা মূল সমস্যার জন্য একটি সম্পূর্ণ আনুষ্ঠানিক প্রমাণ তৈরি করি।”

এই পদ্ধতিটি সিস্টেমকে তার ভুল থেকে শিখতে এবং জটিল সমস্যাগুলো সমাধান করার ক্ষমতা উন্নত করতে সহায়তা করে। যেসব নির্দিষ্ট উপ-লক্ষ্য সমস্যার সৃষ্টি করছে, সেগুলোকে চিহ্নিত করে, সিস্টেমটি সেই ক্ষেত্রগুলোতে তার কর্মক্ষমতা উন্নত করার দিকে মনোযোগ দিতে পারে।

উদ্বেগ এবং চ্যালেঞ্জ: বাস্তবায়ন বিশদ বিবেচনার অধীনে

DeepSeek-Prover-V2 দ্বারা প্রদর্শিত অনস্বীকার্য প্রযুক্তিগত অর্জন সত্ত্বেও, এই ক্ষেত্রের কিছু বিশেষজ্ঞ কিছু বাস্তবায়ন বিশদ সম্পর্কে প্রাসঙ্গিক উদ্বেগ প্রকাশ করেছেন। Epoch AI-এর একজন সম্মানিত প্রধান গণিতবিদ এলিয়ট গ্লেজার, সম্ভাব্য সমস্যাগুলোর দিকে ইঙ্গিত করেছেন, যেগুলোর আরও তদন্ত করা দরকার।

কিছু উদ্বেগ প্রকাশ করে তিনি বলেন, DeepSeek-Prover-V2 পেপারে কিছু ভুলভাবে আনুষ্ঠানিককৃত উদাহরণ থাকতে পারে। লীন জুলিপের আলোচনা থেকে জানা যায় যে PutnamBench-এর প্রমাণগুলো ভিত্তিহীন এবং একটি অন্তর্নিহিত "সরি" ব্যবহার করে (সম্ভবত apply? কৌশলের মধ্যে লুকানো), যা তাদের রিড-ইভাল-প্রিন্ট-লুপে রিপোর্ট করা হয়নি।

এই উদ্বেগগুলো আনুষ্ঠানিক যাচাইকরণ স্থানে বিদ্যমান চলমান চ্যালেঞ্জগুলোকে স্পষ্টভাবে তুলে ধরে। যেখানে ক্ষুদ্র এবং আপাতদৃষ্টিতে নগণ্য বাস্তবায়ন বিশদগুলোও ফলাফলের সামগ্রিক বৈধতা এবং নির্ভরযোগ্যতার ওপর непропорционально বড় প্রভাব ফেলতে পারে। আনুষ্ঠানিক যাচাইকরণ প্রক্রিয়ার জন্য বিস্তারিত মনোযোগ এবং প্রতিষ্ঠিত মানগুলোর প্রতি সতর্ক আনুগত্য প্রয়োজন।

সম্ভাব্য ভুলভাবে আনুষ্ঠানিককৃত উদাহরণ এবং PutnamBench প্রমাণগুলোতে লুকানো "সরি" কৌশলের সম্ভাবনা যাচাইকরণ প্রক্রিয়ার কঠোরতা এবং সম্পূর্ণতা সম্পর্কে গুরুত্বপূর্ণ প্রশ্ন তৈরি করে। এই উদ্বেগগুলো ফলাফলের অব্যাহত নিরীক্ষণ এবং স্বাধীন যাচাইকরণের প্রয়োজনীয়তার ওপর জোর দেয়।

উপলভ্যতা এবং সম্পদ: আনুষ্ঠানিক উপপাদ্য প্রমাণে অ্যাক্সেসকে গণতান্ত্রিক করা

ডিপসিক তাদের Prover-V2 দুটি ভিন্ন মডেল আকারে উপলব্ধ করেছে, যা বিভিন্ন কম্পিউটেশনাল রিসোর্স এবং গবেষণার উদ্দেশ্য পূরণ করে। প্রথম সংস্করণটি হলো তাদের আগের Prover-V1.5-Base-এর ওপর ভিত্তি করে তৈরি একটি 7B প্যারামিটার মডেল, যেখানে 32K টোকেন পর্যন্ত extended context length রয়েছে। দ্বিতীয় সংস্করণটি হলো DeepSeek-V3-Base-এর ওপর প্রশিক্ষিত একটি উল্লেখযোগ্যভাবে বৃহৎ 671B প্যারামিটার মডেল। উভয় মডেলই এখন HuggingFace-এ সহজে পাওয়া যাচ্ছে, যা মেশিন লার্নিং মডেল শেয়ারিং এবং সহযোগিতার জন্য একটি শীর্ষস্থানীয় প্ল্যাটফর্ম।

মডেলগুলো ছাড়াও, ডিপসিক তাদের সম্পূর্ণ ProverBench ডেটাসেটও HuggingFace-এ উপলব্ধ করেছে, যেখানে মূল্যায়ন উদ্দেশ্যে 325টি সতর্কতার সাথে আনুষ্ঠানিক সমস্যা রয়েছে। এই বিস্তৃত ডেটাসেট গবেষক এবং ডেভেলপারদের তাদের মডেলগুলোর কর্মক্ষমতা মূল্যায়ন করতে এবং DeepSeek-Prover-V2-এর সাথে তুলনা করার জন্য একটি মূল্যবান উৎস সরবরাহ করে।

এই রিসোর্সগুলো অবাধে উপলব্ধ করার মাধ্যমে, ডিপসিক আনুষ্ঠানিক উপপাদ্য প্রমাণ প্রযুক্তিতে অ্যাক্সেসকে গণতান্ত্রিক করছে এবং গবেষণা সম্প্রদায়ের মধ্যে সহযোগিতা বাড়াচ্ছে। এই ওপেন-সোর্স পদ্ধতিটি সম্ভবত এই ক্ষেত্রের অগ্রগতিকে ত্বরান্বিত করবে এবং স্বয়ংক্রিয় যুক্তি এবং যাচাইকরণে নতুন সাফল্য আনবে।

এই প্রকাশনা গবেষক এবং ডেভেলপারদের এই প্রযুক্তির ক্ষমতা এবং সীমাবদ্ধতাগুলো অন্বেষণ করার জন্য প্রয়োজনীয় রিসোর্স সরবরাহ করে। মডেল এবং ProverBench ডেটাসেটে উন্মুক্ত অ্যাক্সেস প্রদানের মাধ্যমে, ডিপসিক এই ক্ষেত্রের বিশেষজ্ঞদের দ্বারা উত্থাপিত উদ্বেগগুলো নিয়ে আরও অনুসন্ধান এবং সহযোগী প্রচেষ্টাকে উৎসাহিত করে। এই সহযোগী পদ্ধতিটি আনুষ্ঠানিক উপপাদ্য প্রমাণের জটিলতাগুলো উন্মোচন এবং এই যুগান্তকারী অগ্রগতির নির্ভরযোগ্যতা জোরদার করার চাবিকাঠি।