VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
यह शोध पत्र VeriContest को प्रस्तुत करता है, जो Rust और Verus के साथ 946 प्रतिस्पर्धी प्रोग्रामिंग समस्याओं का एक व्यापक बेंचमार्क है जो प्राकृतिक भाषा विवरणों को विशेषज्ञ-सत्यापित औपचारिक विशिष्टताओं और मशीन-जांच योग्य प्रमाणों के साथ जोड़ता है, जो वर्तमान मॉडलों की कोडिंग क्षमताओं और उनकी सत्यापन योग्य कोड जनरेशन की क्षमता के बीच एक महत्वपूर्ण प्रदर्शन अंतराल को प्रकट करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक प्रतिभाशाली लेकिन अनुभवहीन वास्तुकार (architect) को एक घर बनाने के लिए काम पर रख रहे हैं।
मानक कोडिंग बेंचमार्क की दुनिया में, आप वास्तुकार को एक सरल विवरण देते हैं: "तीन बेडरूम और एक रसोई वाला एक घर बनाओ।" वास्तुकार ब्लूप्रिंट तैयार करता है, घर बनाता है, और आप जाँच करते हैं कि दरवाजे खुल रहे हैं या नहीं और लाइटें काम कर रही हैं या नहीं। यदि वे काम करती हैं, तो वास्तुकार को पास होने का ग्रेड मिलता है। यह वर्तमान AI मॉडल द्वारा कोड लिखने जैसा है: वे ऐसी चीजें बनाने में माहिर हैं जो दिखने में और काम करने में सही लगती हैं।
लेकिन क्या होगा यदि आपको एक ऐसा घर चाहिए जो गणितीय रूप से गारंटी देता हो कि वह कभी ढहेगा नहीं, यहाँ तक कि तूफान में भी नहीं? आप केवल लाइटों की जाँच नहीं कर सकते; आपको संरचना के सुदृढ़ होने का एक औपचारिक प्रमाण (formal proof) चाहिए। यहीं पर "VeriContest" पेपर काम आता है।
समस्या: "यह काम करता है, लेकिन क्या यह सत्य है?"
वर्तमान AI मॉडल उन प्रतिभाशाली वास्तुकारों की तरह हैं जो एक ऐसा घर बना सकते हैं जो दृश्य निरीक्षण (visual inspection) में पास हो जाता है। हालाँकि, वे अक्सर कठोर इंजीनियरिंग गणित को छोड़ देते हैं। वे एक ऐसा घर बना सकते हैं जो दिखने में ठीक लगे लेकिन जिसकी नींव में कोई छिपा हुआ दोष हो जो केवल विशिष्ट तनाव (stress) के तहत सामने आए।
इस शोध पत्र के लेखक तर्क देते हैं कि हमें AI को परखने का एक नया तरीका चाहिए। केवल यह पूछने के बजाय कि "क्या कोड चलता है?", हमें पूछने की आवश्यकता है, "क्या आप गणितीय निश्चितता के साथ सिद्ध कर सकते हैं कि यह कोड बिल्कुल वैसा ही करता है जैसा इसे करना चाहिए, और इसके अलावा कुछ भी नहीं?"
समाधान: VeriContest
टीम ने एक विशाल "परीक्षा" बनाई जिसे VeriContest कहा जाता है। इसे AI वास्तुकारों के लिए एक उच्च-दांव वाली प्रतियोगिता के रूप में समझें, लेकिन इसके तीन सख्त नियम हैं:
- ब्लूप्रिंट (विशिष्टीकरण/Specification): AI को पहले एक गणितीय अनुबंध लिखना होगा। यह केवल एक विवरण नहीं है; यह नियमों का एक कठोर सेट है जो सटीक रूप से परिभाषित करता है कि इनपुट क्या है और आउटपुट क्या होना चाहिए।
- निर्माण (कोड): AI को उन नियमों का पालन करते हुए वास्तविक कोड (Rust प्रोग्रामिंग भाषा में) लिखना होगा।
- इंजीनियरिंग प्रमाण (सत्यापन/Verification): AI को यह गणितीय प्रमाण प्रदान करना होगा कि कोड विफल नहीं हो सकता। यह यह दिखाने जैसा है कि छत नहीं गिरेगी, इसके लिए गणित दिखाना, न कि केवल यह उम्मीद करना कि वह नहीं गिरेगी।
उन्होंने इसका परीक्षण प्रसिद्ध कोडिंग प्रतियोगिताओं (LeetCode और Codeforces) से लिए गए 946 कठिन पहेलियों पर किया। ये साधारण "Hello World" कार्य नहीं हैं; ये जटिल लॉजिक संबंधी समस्याएं हैं जिनमें डेटा में पैटर्न खोजना या मार्ग अनुकूलित (optimize) करना जैसे विषय शामिल हैं।
निर्माण प्रक्रिया
इस परीक्षा को बनाना कठिन था। टीम ने केवल AI से प्रश्न नहीं पूछे; उन्होंने इसे तीन चरणों में बनाया:
- चरण 1 (बीज/Seed): मानव विशेषज्ञों ने मैन्युअल रूप से 91 आदर्श उदाहरण दोषरहित प्रमाणों के साथ लिखे।
- चरण 2 (विस्तार/Expansion): उन्होंने अधिक समस्याएँ उत्पन्न करने के लिए एक AI सहायक का उपयोग किया, लेकिन मानव विशेषज्ञों ने "संपादक" के रूप में कार्य किया, प्रत्येक की जाँच की ताकि यह सुनिश्चित हो सके कि गणित सही है।
- चरण 3 (तनाव परीक्षण/Stress Test): उन्होंने "नेगेटिव टेस्ट केस" बनाए—ऐसी स्थितियाँ जो AI को धोखा देने के लिए डिज़ाइन की गई थीं। यदि AI का प्रमाण अधूरा था, तो ये ट्रिकी सवाल उस खामी को उजागर कर देते।
परिणाम: एक बड़ा अंतर
जब उन्होंने दुनिया के सबसे स्मार्ट AI मॉडल को इस परीक्षा के माध्यम से चलाया, तो परिणाम आश्चर्यजनक और स्पष्ट थे।
- "सामान्य" टेस्ट: जब केवल विवरण से कोड लिखने के लिए कहा गया (बिना प्रमाण के), तो सर्वश्रेष्ठ AI 92% बार सही रहा। वह एक मास्टर बिल्डर है।
- "ब्लूप्रिंट" टेस्ट: जब गणितीय अनुबंध (specification) लिखने के लिए कहा गया, तो स्कोर गिरकर 48% हो गया। AI नियमों को सटीक रूप से परिभाषित करने में संघर्ष कर रहा था।
- "प्रमाण" टेस्ट: जब कोड के काम करने का गणितीय प्रमाण देने के लिए कहा गया, तो स्कोर तेजी से गिरकर 14% रह गया। AI भारी गणित का काम करने में असमर्थ रहा।
- "पूर्ण परीक्षा" (एंड-टू-एंड): जब एक साथ तीनों चरण करने के लिए कहा गया (ब्लूप्रिंट + कोड + प्रमाण), तो सर्वश्रेष्ठ AI केवल 5.3% बार सफल हुआ।
उपमा: "परफेक्ट हाउस"
कल्पना कीजिए कि AI एक शेफ है।
- मानक कोडिंग: आप बर्गर मांगते हैं। शेफ एक बर्गर बनाता है जो स्वादिष्ट होता है। आप उसे खाते हैं। सफलता!
- सत्यापन योग्य कोडिंग (Verifiable Coding): आप एक बर्गर मांगते हैं, लेकिन आप एक प्रमाण पत्र भी मांगते हैं जो यह साबित करे कि मांस एक विशिष्ट फार्म से आया है, बन को ठीक 350 डिग्री पर पकाया गया था, और बर्गर में कोई भी छिपा हुआ एलर्जेन नहीं है। शेफ बर्गर बना सकता है, लेकिन वे प्रमाण पत्र लिखने या खाना पकाने के पीछे के गणित को सिद्ध करने में बहुत खराब हैं।
निष्कर्ष
पेपर यह निष्कर्ष निकालता है कि जबकि AI प्रोग्राम चलाने के लिए सही कोड का "अनुमान" लगाने में बहुत अच्छा हो रहा है, यह सिद्ध करने में अभी भी बहुत खराब है कि कोड सही है। सबसे बड़ी बाधा कोड लिखना नहीं है; बल्कि वे औपचारिक नियम और गणितीय प्रमाण लिखना है जो गारंटी देते हैं कि कोड सुरक्षित है।
VeriContest अब शोधकर्ताओं के लिए एक उपकरण है जिससे वे सटीक रूप से माप सकें कि AI को कितना आगे जाना है, इससे पहले कि उस पर सॉफ्टवेयर बनाने के लिए भरोसा किया जा सके जो गणितीय रूप से बग-मुक्त होने की गारंटी देता हो।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।