Evaluating LLM-Generated ACSL Annotations for Formal Verification
यह शोध पत्र 506 वास्तविक दुनिया के C प्रोग्रामों के लिए ACSL विनिर्देशों (specifications) को उत्पन्न करने और सत्यापित करने में तीन लार्ज लैंग्वेज मॉडल्स सहित पांच स्वचालित प्रणालियों की प्रभावशीलता का अनुभवजन्य मूल्यांकन करता है, जो पारंपरिक नियम-आधारित दृष्टिकोणों की तुलना में उनकी क्षमताओं और सीमाओं पर नया प्रमाण प्रदान करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक विशाल, जटिल घर (एक सॉफ़्टवेयर प्रोग्राम) बना रहे हैं। आप पूरी तरह आश्वस्त होना चाहते हैं कि इसमें आग नहीं लगेगी, यह ढहेगा नहीं, या इसमें कोई ऐसा दरवाज़ा नहीं होगा जो कहीं भी न जाता हो। ऐसा करने के लिए, आप एक अत्यंत सख्त बिल्डिंग इंस्पेक्टर (फॉर्मल वेरिफिकेशन) को काम पर रखते हैं जो आपके ब्लूप्रिंट की कड़े सुरक्षा कानूनों (ACSL एनोटेशन) के विरुद्ध जांच करता है।
समस्या क्या है? इन सुरक्षा कानूनों को इंस्पेक्टर की सख्त, गणितीय भाषा में लिखना अविश्वसनीय रूप से कठिन, उबाऊ और मानवीय त्रुटियों के प्रति संवेदनशील है।
बड़ा सवाल: क्या आर्टिफिशियल इंटेलिजेंस (AI) हमारे लिए ये सुरक्षा कानून लिख सकता है, और क्या इंस्पेक्टर वास्तव में उन पर भरोसा कर सकता है?
यह पेपर एक "टेस्ट टेस्ट" है जहाँ लेखकों ने पाँच अलग-अलग "शेफ" (रसोइयों) को आज़माया ताकि यह देखा जा सके कि कौन सबसे अच्छे सुरक्षा नियम लिख सकता है, और उन्होंने 506 अलग-अलग C प्रोग्रामों (घर के ब्लूप्रिंट) का उपयोग किया।
पाँच शेफ (परीक्षण किए गए सिस्टम)
- रोबोट शेफ (नियम-आधारित पायथन स्क्रिप्ट): यह AI नहीं है। यह निर्देशों का एक कठोर सेट है। यह एक रेसिपी का ठीक वैसे ही पालन करता है। यह उबाऊ है, लेकिन यह शायद ही कभी गलती करता है।
- सेफ्टी गार्ड (Frama-C RTE प्लगइन): यह एक विशेष टूल है जिसे विशेष रूप से रनटाइम एरर (जैसे शून्य से विभाजन) को पकड़ने के लिए डिज़ाइन किया गया है। यह एक गार्ड डॉग की तरह है जो केवल ज्ञात खतरों पर ही भौंकता है।
- क्रिएटिव राइटर्स (तीन लार्ज लैंग्वेज मॉडल्स):
- DeepSeek: एक बहुत ही स्मार्ट, आधुनिक AI।
- GPT-5: OpenAI का प्रसिद्ध, शक्तिशाली AI।
- OLMo3: एक ओपन-सोर्स AI मॉडल।
- इन्हें प्रतिभाशाली लेकिन कभी-कभी अति-उत्साही इंटर्न के रूप में सोचें जो सिद्धांत के बारे में बहुत कुछ जानते हैं लेकिन विवरणों में थोड़ी गलती कर सकते हैं।
प्रयोग: "टेस्ट टेस्ट"
लेखकों ने 506 C प्रोग्राम लिए और प्रत्येक पाँच शेफ से उनके लिए सुरक्षा नियम लिखने को कहा। फिर, उन्होंने ये नियम चार अलग-अलग "इंस्पेक्टर्स" (SMT सॉल्वर्स: Alt-Ergo, CVC4, CVC5, और Z3) को सौंप दिए ताकि यह देखा जा सके कि क्या नियम समझ में आते हैं और क्या घर सुरक्षित है।
उन्होंने दो चीजें मापीं:
- क्या इंस्पेक्टर नियमों को समझ पाया? (प्रूफ सक्सेस)
- क्या इंस्पेक्टर भ्रमित होकर बहुत अधिक समय ले रहा था? (टाइमआउट और स्पीड)
परिणाम: क्या हुआ?
1. रोबोट और गार्ड डॉग (विजेता)
नियम-आधारित स्क्रिप्ट और सेफ्टी गार्ड स्पष्ट विजेता थे।
- उपमा: उन्होंने ऐसे नियम लिखे जो सरल, शुष्क और पूरी तरह से फॉर्मेट किए गए थे।
- परिणाम: इंस्पेक्टर 99% समय उन्हें समझ गए और उन्होंने काम पलक झपकते ही पूरा कर लिया। वे उबाऊ थे लेकिन भरोसेमंद थे। यदि आपको गारंटी चाहिए कि आपका सॉफ़्टवेयर क्रैश नहीं होगा, तो ये वे लोग हैं जिनका उपयोग किया जाना चाहिए।
2. क्रिएटिव राइटर्स (एक मिला-जुला अनुभव)
AI मॉडल्स (DeepSeek, GPT-5, OLMo3) बहुत अधिक दिलचस्प थे, लेकिन भी बहुत अधिक अराजक भी थे।
- DeepSeek: यह "स्टार स्टूडेंट" था। इसने ऐसे नियम लिखे जो लगभग रोबोट शेफ जितने अच्छे थे। यह सटीक होने के लिए पर्याप्त स्मार्ट था और जटिल स्थितियों को संभालने के लिए पर्याप्त रचनात्मक भी।
- OLMo3: इसने ठीक-ठाक काम किया, जो बीच में स्थित था। यह स्थिर था लेकिन DeepSeek जितना प्रभावशाली नहीं था।
- GPT-5: यह सबसे अधिक "मानवीय" और सबसे अधिक समस्याग्रस्त था। इसने ऐसे नियम लिखे जो सुनने में शानदार और दिखने में फैंसी थे, लेकिन वे अक्सर बहुत अस्पष्ट या भ्रमित करने वाले थे।
- उपमा: कल्पना कीजिए कि GPT-5 एक सुरक्षा नियम लिख रहा है जैसे, "सुनिश्चित करें कि दरवाज़ा सुरक्षित है।" इंस्पेक्टर (कंप्यूटर) पूछता है, "सुरक्षित का क्या मतलब है? क्या यह लॉक है? क्या यह अग्नि-रोधी है? क्या इसका रंग सही है?" इंस्पेक्टर इसे समझने की कोशिश में फंस जाता है, जिससे टाइमआउट (इंस्पेक्टर हार मान लेता है क्योंकि कार्य बहुत कठिन है) होता है।
मुख्य निष्कर्ष: "एक्सप्रेसिवनेस बनाम स्टेबिलिटी" का ट्रेड-ऑफ
पेपर ने एक मौलिक तनाव पाया, जो एक सी-सॉ (seesaw) की तरह है:
- एक तरफ: स्टेबिलिटी (स्थिरता)। रोबोट शेफ और गार्ड डॉग ऐसे नियम बनाते हैं जिन्हें कंप्यूटर द्वारा चेक करना आसान होता है। वे तेज़ और विश्वसनीय हैं, लेकिन वे सूक्ष्म, जटिल खतरों को मिस कर सकते हैं क्योंकि वे बहुत कठोर हैं।
- दूसरी ओर: एक्सप्रेसिवनेस (अभिव्यक्तिशीलता)। AI मॉडल्स (विशेष रूप से GPT-5) बहुत विस्तृत, सूक्ष्म नियम लिख सकते हैं जो जटिल परिदृश्यों को कवर करते हैं। हालाँकि, क्योंकि वे इतने विस्तृत और कभी-कभी थोड़े अस्पष्ट होते हैं, कंप्यूटर इंस्पेक्टर अभिभूत हो जाते हैं और धीमे हो जाते हैं या विफल हो जाते हैं।
"DeepSeek" का स्वीट स्पॉट:
DeepSeek ने इसे सबसे अच्छी तरह से संतुलित किया। इसने ऐसे नियम लिखे जो उपयोगी होने के लिए पर्याप्त जटिल थे लेकिन इंस्पेक्टरों के समझने के लिए पर्याप्त स्पष्ट थे।
फैसला
- क्या AI सुरक्षा नियम लिख सकता है? हाँ!
- क्या हम उन पर आँख मूंदकर भरोसा कर सकते हैं? अभी नहीं।
- भविष्य: हम केवल AI को नियम लिखने के लिए नहीं छोड़ सकते और उम्मीद नहीं कर सकते कि सब ठीक होगा। हमें एक "हाइब्रिड" दृष्टिकोण की आवश्यकता है। हम विचारों का ड्राफ्ट तैयार करने के लिए AI का उपयोग कर सकते हैं (क्योंकि यह रचनात्मक है), लेकिन फिर हमें एक "रोबोट शेफ" या मानव की आवश्यकता होगी जो नियमों को साफ-सुथरा करे ताकि कंप्यूटर इंस्पेक्टर बिना सिरदर्द के उन्हें सत्यापित कर सके।
संक्षेप में: AI एक शानदार मंथन साथी (brainstorming partner) है, लेकिन महत्वपूर्ण सुरक्षा जाँचों के लिए, हमें अभी भी अंतिम, विश्वसनीय सत्यापन करने के लिए उबाऊ, कठोर, नियम का पालन करने वाले उपकरणों की आवश्यकता है। यह पेपर साबित करता है कि हालांकि AI बेहतर हो रहा है, फिर भी इसे वास्तव में "फॉर्मल" और भरोसेमंद होने के लिए थोड़ी मदद की आवश्यकता है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।