An Empirical Study of LLM-Generated Specifications for VeriFast
यह शोध पत्र 303 C फलनों (functions) के लिए VeriFast विनिर्देशों (specifications) को उत्पन्न करने में आठ प्रॉम्प्टिंग रणनीतियों के माध्यम से दस लार्ज लैंग्वेज मॉडल्स की प्रभावशीलता का अनुभवजन्य मूल्यांकन करता है, जिससे यह स्पष्ट होता है कि जबकि LLMs कार्यात्मक व्यवहार को बनाए रखते हैं, वे मुख्य रूप से डोमेन-विशिष्ट सेपरेशन लॉजिक ज्ञान में त्रुटियों के कारण केवल मामूली सत्यापन सफलता (31.4%) ही प्राप्त करते हैं।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आपके पास एक बहुत ही सख्त, सुपर-स्मार्ट रोबोट इंस्पेक्टर है जिसका नाम VeriFast है। इसका काम कंप्यूटर कोड की जांच करना है ताकि यह सुनिश्चित हो सके कि वह कभी क्रैश न हो, डेटा कभी न खोए, और बिल्कुल वैसा ही व्यवहार करे जैसा वादा किया गया है। लेकिन इसमें एक पेंच है: VeriFast इंसानी भाषा नहीं बोलता। यह एक बहुत ही जटिल, गणितीय बोली बोलता है जिसे सेपरेशन लॉजिक (Separation Logic) कहा जाता है। VeriFast से अपना काम करवाने के लिए, एक इंसान को एक विशाल "निर्देश पुस्तिका" (स्पेसिफिकेशन) लिखनी होगी जो यह समझा सके कि कोड मेमोरी को कैसे संभालता है, जैसे कि शहर के ट्रैफिक नियमों का एक विस्तृत नक्शा।
यह मैनुअल लिखना अविश्वसनीय रूप से कठिन और समय लेने वाला काम है। यह ऐसा है जैसे सड़क यात्रा के दौरान ड्राइवर द्वारा लिए जाने वाले हर मोड़ के लिए एक कानूनी अनुबंध लिखने की कोशिश करना।
बड़ा सवाल
शोधकर्ताओं ने पूछा: क्या आर्टिफिशियल इंटेलिजेंस (विशेष रूप से लार्ज लैंग्वेज मॉडल्स या LLMs) VeriFast के लिए ये जटिल निर्देश पुस्तिकाएं लिख सकते हैं?
उन्होंने LLMs के साथ ऐसा व्यवहार किया जैसे वे एक नया प्रशिक्षु (apprentice) हो जो कोड तो लिख सकता है लेकिन उसे VeriFast की सख्त बोली सीखने की जरूरत है। उन्होंने यह देखने के लिए कि क्या AI मैनुअल लिख सकता है और क्या VeriFast इसे स्वीकार करेगा, 10 अलग-अलग AI मॉडल्स का परीक्षण 303 अलग-अलग कंप्यूटर फंक्शन्स (कोड के छोटे हिस्से) पर किया।
प्रयोग: "तीन-चरण" वाला टेस्ट
शोधकर्ताओं ने एक बड़ा परीक्षण सेटअप किया:
- इनपुट्स (Inputs): उन्होंने प्रत्येक कार्य के लिए AI को तीन प्रकार की "ब्रीफिंग" दी:
- नेचुरल लैंग्वेज (Natural Language): बस एक साधारण अंग्रेजी विवरण (जैसे, "यह फंक्शन एक लिस्ट के अंत में एक नोड जोड़ता है")।
- फॉर्मल बिहेवियर (Formal Behavior): कोड और कुछ गणितीय प्रतीकों का मिश्रण।
- फॉर्मल प्लस (Formal Plus): कोड और एक बहुत ही विस्तृत, लगभग पूर्ण गणितीय मैनुअल।
- प्रॉम्प्ट्स (Prompts): उन्होंने AI को काम करने के लिए कहने के 8 अलग-अलग तरीके आजमाए (जैसे, एक स्टेप-बाय-स्टेप रेसिपी देना बनाम सिर्फ "इसे करो" कहना)।
- मॉडल्स (Models): उन्होंने GPT-4o से लेकर Gemini 2.5 Pro तक 10 अलग-अलग AI दिमागों का परीक्षण किया।
परिणाम: अच्छा, बुरा और "लगभग"
अच्छी खबर (प्रशिक्षु ईमानदार है):
AI कोड के इरादे (intent) को समझने में आश्चर्यजनक रूप से अच्छा था। 91% से अधिक मामलों में, AI ने अनजाने में उस काम को नहीं बदला जो कोड को करना चाहिए था। इसने कोड को सिद्ध करना आसान बनाने के लिए उसे बदलने की कोशिश नहीं की। यह मूल कार्य विवरण के प्रति सच्चा रहा।बुरी खबर (प्रशिक्षु नियमों के बारे में अनभिज्ञ है):
भले ही AI काम को समझ गया था, लेकिन वह ऐसा मैनुअल लिखने में विफल रहा जिसे VeriFast स्वीकार कर सके। AI द्वारा बनाए गए मैनुअल्स में से केवल लगभग 31% ही निरीक्षण में पास हुए। यह हर 3 प्रयासों में से लगभग 1 प्रयास है।"क्यों" (यह तर्क नहीं, सिंटैक्स है):
जब AI विफल हुआ, तो यह आमतौर पर इसलिए नहीं था क्योंकि वह "मूर्ख" था या गणित नहीं कर सकता था। वह इसलिए विफल हुआ क्योंकि उसे VeriFast की विशिष्ट व्याकरण और नियमों का ज्ञान नहीं था।- उपमा (Analogy): कल्पना कीजिए कि AI एक शानदार शेफ है जो एक परफेक्ट स्टेक बनाना जानता है। लेकिन VeriFast एक हेल्थ इंस्पेक्टर है जो केवल फ्रेंच की एक विशिष्ट, अज्ञात बोली में लिखी गई रेसिपी को ही स्वीकार करता है। शेफ रेसिपी को अंग्रेजी या स्पेनिश में लिखता रहता है। खाना बेहतरीन है, लेकिन इंस्पेक्टर उसे खारिज कर देता है क्योंकि फॉर्मेट गलत है।
- पेपर ने पाया कि 94% त्रुटियां इन्हीं विशिष्ट नियमों के बारे में थीं (जैसे कि मेमोरी ब्लॉक को "ओपन" करना या "क्लोज" करना भूल जाना, या किसी विशिष्ट कीवर्ड को छोड़ देना), न कि प्रोग्राम के तर्क के बारे में।
कौन जीता?
- सबसे अच्छा AI: Gemini 2.5 Pro स्पष्ट विजेता था। इसने अन्य मॉडल्स की तुलना में कम गलतियाँ कीं और अधिक सफल निरीक्षण पास किए।
- सबसे अच्छा इनपुट: जब शोधकर्ताओं ने AI को "फॉर्मल प्लस" ब्रीफिंग (एक बहुत ही विस्तृत शुरुआती बिंदु) दी, तो सफलता दर बढ़ गई। जब उन्होंने इसे केवल एक साधारण अंग्रेजी विवरण दिया, तो AI को सबसे अधिक संघर्ष करना पड़ा।
निष्कर्ष (Takeaway)
पेपर यह निष्कर्ष निकालता है कि हालांकि AI इस बात को समझने में महान है कि कोड को क्या करना चाहिए, लेकिन यह वर्तमान में VeriFast जैसे उन्नत वेरिफिकेशन टूल्स के लिए विशिष्ट, कठोर निर्देशों को लिखने में बहुत अच्छा नहीं है।
AI इसलिए विफल नहीं हो रहा है क्योंकि वह तर्क नहीं कर सकता; वह इसलिए विफल हो रहा है क्योंकि वह टूल की विशिष्ट "बोली" को नहीं जानता। इसे ठीक करने के लिए, शोधकर्ताओं का सुझाव है कि हमें या तो:
- AI को VeriFast के विशिष्ट नियमों को बेहतर ढंग से सिखाना होगा।
- AI को गलती करने पर बेहतर फीडबैक देना होगा (जैसे कि केवल "गलत" कहने के बजाय व्याकरण सुधारने वाला शिक्षक बनना)।
- अंतराल को भरने के लिए AI और पारंपरिक टूल्स के मिश्रण का उपयोग करना होगा।
संक्षेप में: AI प्रशिक्षु प्रतिभाशाली और ईमानदार है, लेकिन अकेले काम करने से पहले उसे रोबोट इंस्पेक्टर की विशिष्ट "भाषा" पर बहुत अधिक प्रशिक्षण की आवश्यकता है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।