কেন একটি নতুন বেঞ্চমার্ক প্রয়োজন
নিউরাল নেটওয়ার্ক যত বেশি কোড লেখে, প্রশ্নটি ততই তীব্র হয়: কীভাবে নিশ্চিত হওয়া যায় যে এই কোডটি সত্যিই যা প্রয়োজন তা করে? সাধারণ পরীক্ষাগুলি কিছু ত্রুটি খুঁজে পায়, কিন্তু সঠিকতার আনুষ্ঠানিক নিশ্চয়তা দেয় না। এর জন্য প্রয়োজন যাচাইকরণ — প্রোগ্রামটিকে কঠোর গাণিতিক বিবৃতির ভাষায় অনুবাদ করা এবং এর বৈশিষ্ট্যগুলি প্রমাণ করা। এই কাজটি ব্যয়বহুল এবং জটিল, তাই গবেষকরা এটি AI-এর উপর চাপাতে চান।
সমস্যা হল, সাবধানে তৈরি শিক্ষামূলক উদাহরণে প্রশিক্ষিত মডেলগুলি বাস্তব কোডের মুখোমুখি হলে প্রায়ই বিভ্রান্ত হয়ে যায়। প্রকৃত প্রকল্পে অগণিত অন্তর্নিহিত চুক্তি, ভাষার বিশেষত্ব এবং নথিভুক্ত নয় এমন আচরণ থাকে। AI এই ধরনের পরিস্থিতিতে কতটা ভালোভাবে মোকাবেলা করে তা পরীক্ষা করার জন্য, সিন্থেটিক সমস্যার পরিবর্তে বাস্তব প্রোগ্রামের উপর নির্মিত একটি বৃহৎ পরিসরের পরীক্ষার ক্ষেত্র প্রয়োজন।
FVSpec: AI-এর জন্য একটি চ্যালেঞ্জ হিসেবে বাস্তব পরীক্ষা
গবেষকদের একটি দল — Quinn Dougherty, Max von Hippel, Simon Henniger, Hazel Shackleton এবং Mike Dodds — FVSpec বেঞ্চমার্কটি উপস্থাপন করেছে। কাজটি arXiv-এ 2606.01008 নম্বরে প্রকাশিত হয়েছে এবং ২০২৬ সালের আগস্টে লেখকরা একটি আপডেট সংস্করণ প্রকাশ করেছেন।
মূল ধারণাটি হল বাস্তব Python রিপোজিটরি থেকে property-based পরীক্ষাগুলি নেওয়া এবং সেগুলিকে Lean 4 ভাষায় আনুষ্ঠানিক স্পেসিফিকেশনে রূপান্তর করা। এই ধরনের পরীক্ষাগুলি নির্দিষ্ট উদাহরণ নয়, বরং ফাংশনের বৈশিষ্ট্যগুলি পরীক্ষা করে: "যেকোনো বৈধ ইনপুটের জন্য একটি নির্দিষ্ট শর্ত পূরণ হয়"। এটি তাদের গাণিতিক আনুষ্ঠানিকীকরণের একটি প্রাকৃতিক সেতু করে তোলে।
লেখকরা ওপেন-সোর্স Python প্রকল্প থেকে ১১,০৩৯টি property-based পরীক্ষা সংগ্রহ করেছেন। তাদের মধ্যে মাত্র ২,৭৭২টি স্বয়ংক্রিয়ভাবে Lean 4-এ অনুবাদ করা সম্ভব হয়েছে — প্রায় এক-চতুর্থাংশ। ফলে ৯,৪১৫টি স্পেসিফিকেশন তৈরি হয়েছে: প্রতিটি সফলভাবে অনূদিত পরীক্ষার জন্য প্রায় তিনটি আনুষ্ঠানিকীকরণের রূপ। এই অতিরিক্ত প্রয়োজন কারণ একই বৈশিষ্ট্য বিভিন্নভাবে লেখা যেতে পারে, এবং কোন রূপটি পরবর্তী প্রমাণের জন্য বেশি সুবিধাজনক হবে তা আগে থেকে সবসময় স্পষ্ট নয়।
কেন এটি কঠিন
Lean-এ পরীক্ষা পুনর্লিখন একটি যান্ত্রিক সিনট্যাক্স প্রতিস্থাপন নয়। Python এবং Lean বিভিন্ন দৃষ্টান্তে রয়েছে: প্রথমটিতে — ডায়নামিক টাইপিং, পরিবর্তনযোগ্য অবজেক্ট এবং ইম্পেরেটিভ কনস্ট্রাক্ট, দ্বিতীয়টিতে — ডিপেন্ডেন্ট টাইপ সহ একটি কঠোর সিস্টেম। স্পেসিফিকেশনটি কোডের প্রকৃত আচরণের সাথে মিলে যাওয়ার জন্য, Python-এর শব্দার্থবিদ্যাকে সাবধানে মডেল করতে হয়।
অতিরিক্ত জটিলতা হল যে একটি property-based পরীক্ষা প্রায়শই একটি ইম্পেরেটিভ স্ক্রিপ্ট হিসেবে লেখা হয়: লুপ, ব্যতিক্রম এবং স্টেট ম্যানেজমেন্ট সহ। এটি থেকে "যেকোনো x-এর জন্য P(x) সত্য" আকারের একটি বিশুদ্ধ বিবৃতি বের করা একটি পৃথক গবেষণামূলক কাজ।
সবশেষে, Lean 4 একটি জটিল টাইপ সিস্টেম সহ একটি ভাষা হিসেবে রয়ে গেছে, যা এমনকি পেশাদার ডেভেলপমেন্টেও বিরল। ভাষার মডেলগুলির জন্য এটি একটি গুরুতর চ্যালেঞ্জ: তাদের একই সাথে বিরল সিনট্যাক্স শিখতে হবে, ডিপেন্ডেন্ট টাইপে অভ্যস্ত হতে হবে এবং সঠিক সংজ্ঞা তৈরি করতে হবে।
পাইপলাইন এবং মূল্যায়ন কীভাবে গঠন করা হয়েছে
স্বয়ংক্রিয় অনুবাদের জন্য লেখকরা তিনটি LLM-এজেন্টের একটি পাইপলাইন তৈরি করেছেন। বর্ণনা অনুযায়ী, এজেন্টরা নিজেদের মধ্যে কাজ ভাগ করে নেয়: একজন উৎস পরীক্ষা বিশ্লেষণ করে, অন্যজন স্পেসিফিকেশন তৈরি করে, তৃতীয়জন ফলাফল পরীক্ষা করে উন্নত করে। পাইপলাইনের সম্পূর্ণ কোড প্রকাশিত হয়েছে, যেমন সংগৃহীত ডেটাও।
অনুবাদের গুণমান বিভিন্ন দিক থেকে মূল্যায়ন করা হয়েছে। কভারেজ দেখায় যে প্রকৃত পরীক্ষার কত অংশ আনুষ্ঠানিকীকরণযোগ্য। পৃথক মানের মেট্রিক্স মূল্যায়ন করে যে ফলস্বরূপ স্পেসিফিকেশনটি কোডের মূল আচরণকে কতটা প্রতিফলিত করে। উপরন্তু, গবেষকরা প্রমাণ তৈরির জন্য বেসলাইন স্থির করেছেন: তারা বেশ কয়েকটি স্বয়ংক্রিয় এবং মডেল-ভিত্তিক পদ্ধতি চালিয়েছেন এবং খুঁজে বের করেছেন যে সেগুলি কত ঘন ঘন প্রণয়নকৃত বিবৃতিগুলি প্রমাণ করতে সক্ষম হয়। এই ধরনের পরিমাপ ভবিষ্যতের কাজগুলিকে তুলনার জন্য একটি রেফারেন্স পয়েন্ট দেয়।
এটি অনুশীলনে কী দেয়
FVSpec একটি কম অনুসন্ধান করা ক্ষেত্রকে লক্ষ্য করে — বাস্তব সফ্টওয়্যারের AI-সহায়ক আনুষ্ঠানিক যাচাইকরণ। শিক্ষামূলক উদাহরণের বৈশিষ্ট্য প্রমাণ করার ক্ষমতা বাস্তব কোডে সাফল্যের নিশ্চয়তা দেয় না, তাই বাস্তব পরীক্ষার উপর নির্মিত একটি বেঞ্চমার্ক পদ্ধতিগুলিকে সৎভাবে তুলনা করতে এবং অগ্রগতি ট্র্যাক করতে সহায়তা করে।
এই ধরনের পদ্ধতির গুরুত্ব নিউরাল নেটওয়ার্ক দ্বারা উত্পন্ন কোডের পরিমাণের সাথে সাথে বৃদ্ধি পায়। যদি AI ক্রমবর্ধমানভাবে প্রোগ্রাম লেখে, তাহলে সঠিকতা যাচাইয়ের স্বয়ংক্রিয় সরঞ্জামগুলি বিলাসিতা নয়, বরং প্রয়োজনীয়তা হয়ে ওঠে।
উপসংহার
FVSpec আনুষ্ঠানিক যাচাইকরণকে সংকীর্ণ বিশেষজ্ঞদের ডোমেইন থেকে বের করে একটি ব্যবহারিক হাতিয়ারে পরিণত করার দিকে একটি উল্লেখযোগ্য পদক্ষেপ। বেঞ্চমার্কটি প্রকৃত property-based পরীক্ষা, Lean 4 ভাষা এবং একটি ওপেন LLM-পাইপলাইনকে একত্রিত করে। অ্যাক্সেসযোগ্য ডেটা এবং কোডের জন্য ধন্যবাদ, যেকোনো গবেষক পরীক্ষাগুলি পুনরুত্পাদন করতে বা নিজস্ব পদ্ধতির প্রস্তাব দিতে পারেন, এবং এইভাবে সম্প্রদায়ের এগিয়ে যাওয়ার জন্য একটি সাধারণ পয়েন্ট রয়েছে।
