VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus
VeriStruct एक नवीन फ्रेमवर्क है जो व्यवस्थित कोड जनरेशन के लिए एक प्लानर और सिंटैक्स त्रुटियों को सुधारने के लिए एक रिपेयर स्टेज का उपयोग करके Verus में जटिल डेटा स्ट्रक्चर मॉड्यूल के लिए AI-सहायता प्राप्त स्वचालित सत्यापन का विस्तार करता है, जिससे ग्यारह Rust मॉड्यूल्स में फंक्शन्स को सत्यापित करने में 99.2% सफलता दर प्राप्त होती है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप लेगो ब्रिक्स (LEGO bricks) से एक विशाल, जटिल शहर बना रहे हैं। आप 100% सुनिश्चित करना चाहते हैं कि वहां रहने से पहले हर पुल, सुरंग और गगनचुंबी इमारत संरचनात्मक रूप से सुरक्षित (structurally sound) है। सॉफ्टवेयर की दुनिया में, इस "संरचनात्मक मजबूती" को फॉर्मल वेरिफिकेशन (formal verification) कहा जाता है। यह कोड के बग-मुक्त होने को सिद्ध करने का एक गणितीय तरीका है।
हालाँकि, इसे मैन्युअल रूप से करना ऐसा है जैसे हर एक ईंट की जांच करने के लिए इंजीनियरों की एक टीम को हाथ से काम पर रखना। इसमें बहुत समय लगता है, यह अविश्वसनीय रूप से महंगा है, और इसके लिए गणित में पीएचडी की आवश्यकता होती है।
हाल ही में, हमने आर्किटेक्ट्स को एक एआई असिस्टेंट (एक लार्ज लैंग्वेज मॉडल या LLM) दिया है ताकि वे उनकी मदद कर सकें। एआई कोड लिखने में बहुत अच्छा है, लेकिन जब बात गणित की जांच करने की आती है, तो यह अक्सर भ्रमित हो जाता है। यह एक शानदार लेकिन अनुभवहीन इंटर्न को एक ऐसी गुप्त भाषा में लिखे गए ब्लूप्रिंट देने जैसा है जिसे उसने पहले कभी नहीं देखा है। वे एक सुंदर इमारत तो बना सकते हैं, लेकिन वे यह जांचना भूल सकते हैं कि क्या नींव वास्तव में भार सह सकती है।
वेरिस्ट्रक्ट (VeriStruct) से मिलिए।
वेरिस्ट्रक्ट एक नया "सुपर-इंटर्न मैनेजर" है जिसे एआई सहायकों को जटिल सॉफ्टवेयर मॉड्यूल (जैसे डेटा स्ट्रक्चर) को सत्यापित करने में मदद करने के लिए डिज़ाइन किया गया है, जो वेरस (Verus) नामक एक टूल का उपयोग करता है (जो रस्ट (Rust) की भाषा बोलता है, जो एक लोकप्रिय प्रोग्रामिंग भाषा है)।
वेरिस्ट्रक्ट कैसे काम करता है, इसके लिए कुछ रोजमर्रा के उदाहरणों का उपयोग करते हैं:
1. समस्या: "अनुवाद" का अंतर (The "Translation" Gap)
कल्पना कीजिए कि आप एक एआई को एक रिंग बफ़र (Ring Buffer) (एक प्रकार का डेटा स्टोरेज जो एक गोलाकार कन्वेयर बेल्ट की तरह काम करता है) को सत्यापित करने के लिए कहते हैं।
- एआई की गलती: एआई कन्वेयर बेल्ट का वर्णन करने के लिए हर एक ईंट की स्थिति को सूचीबद्ध करने की कोशिश कर सकता है। यह तकनीकी रूप से सही है, लेकिन यह इतना अव्यवस्थित है कि गणितीय चेकर (math checker) अभिभूत होकर हार मान लेता है।
- सिंटैक्स का जाल (The Syntax Trap): वेरस के बहुत सख्त नियम हैं (जैसे "आप प्रूफ लिखते समय ग्लोबल स्टेट को छू नहीं सकते")। एआई, जिसने बहुत सारा सामान्य कोड पढ़ा है लेकिन वेरस का कम कोड देखा है, अक्सर इन नियमों को तोड़ देता है, जैसे पेच (screw) को कसने के लिए हथौड़े का उपयोग करने की कोशिश करना।
2. समाधान: "प्रोजेक्ट मैनेजर" (द प्लानर)
केवल एआई से "यह कोड ठीक करो" कहने के बजाय, वेरिस्ट्रक्ट एक प्रोजेक्ट मैनेजर की तरह कार्य करता है।
- प्लानर मॉड्यूल: एआई द्वारा एक भी लाइन लिखने से पहले, प्लानर कोड को देखता है और पूछता है: "हमें वास्तव में यहाँ क्या चाहिए?"
- क्या हमें एक व्यू (View) चाहिए? (इसे एक "सरलीकृत मानचित्र" के रूप में सोचें। हर ईंट दिखाने के बजाय, मानचित्र बस यह कहता है, "यहाँ बेल्ट पर मौजूद वस्तुओं की सूची है।")
- क्या हमें एक टाइप इनवेरिएंट (Type Invariant) चाहिए? (यह एक "सुरक्षा नियम" है जो हमेशा सत्य होना चाहिए, जैसे "बेल्ट में हमेशा कम से कम एक खाली जगह होनी चाहिए।")
- क्या हमें प्रूफ ब्लॉक्स (Proof Blocks) चाहिए? (ये गणितीय चेकर को कठिन पहेली को हल करने के लिए दिए जाने वाले छोटे संकेत हैं।)
- प्लानर यह तय करता है कि किन उपकरणों का उपयोग कब और किस क्रम में किया जाए, ताकि एआई फुटपाथ बिछाने के बजाय पुल बनाने में अपना समय बर्बाद न करे।
3. "ड्राफ्टिंग" चरण (जेनरेशन)
एक बार योजना सेट हो जाने के बाद, वेरिस्ट्रक्ट एआई को एनोटेशन (सुरक्षा नियम और मानचित्र) लिखने के लिए कहता है।
- प्रॉम्प्ट (The Prompt): एआई को केवल "यह करो" नहीं कहा जाता है। इसे एक चीट शीट (सिंटैक्स दिशानिर्देश) और उदाहरण दिए जाते हैं कि अन्य विशेषज्ञों ने समान समस्याओं को कैसे हल किया था। यह एआई को "गुप्त भाषा" का गलत उपयोग करने से रोकता है।
- रिफाइनमेंट (The Refinement): कभी-कभी एआई एक ऐसा मानचित्र बनाता है जो बहुत विस्तृत होता है (बहुत अधिक ईंटें)। वेरिस्ट्रक्ट के पास एक "रिफाइनमेंट स्टेप" है जो एआई को बताता है: "हे, इसे सरल बनाएं। हमें हर व्यक्तिगत ईंट देखने की आवश्यकता नहीं है; बस हमें यातायात का प्रवाह दिखाएं।" यह गणित को जांचने में बहुत आसान बना देता है।
4. "इंस्पेक्टर" चरण (रिपेयर)
एक बेहतरीन योजना के बावजूद, एआई गलतियाँ करेगा। कोड गणितीय जांच में विफल हो सकता है।
- रिपेयर लूप (The Repair Loop): हार मानने के बजाय, वेरिस्ट्रक्ट एक क्वालिटी कंट्रोल इंस्पेक्टर की तरह कार्य करता है।
- गणितीय चेकर कहता है, "त्रुटि: आपने पेच पर हथौड़ा चलाने की कोशिश की!"
- वेरिस्ट्रक्ट इस विशिष्ट त्रुटि को पकड़ता है, इसे एक विशेष "रिपेयर मॉड्यूल" (एक छोटा-सा एआई जो विशेष रूप से उस प्रकार की गलती को ठीक करने के लिए प्रशिक्षित है) को भेजता है, और मुख्य एआई को फिर से प्रयास करने के लिए कहता है।
- यह तब तक बार-बार करता रहता है, जैसे कि "हॉट एंड कोल्ड" का खेल हो, जब तक कि कोड हर जांच को पास न कर ले।
परिणाम: एक सुपरचार्ज्ड टीम
शोधकर्ताओं ने 11 अलग-अलग जटिल डेटा स्ट्रक्चर (जैसे रिंग बफ़र, ट्रीज़ और लॉक्स) पर वेरिस्ट्रक्ट का परीक्षण किया।
- वेरिस्ट्रक्ट के बिना: एक मानक एआई केवल 11 में से लगभग 4 मॉड्यूल को सत्यापित कर सका।
- वेरिस्ट्रक्ट के साथ: सिस्टम ने 11 में से 10 मॉड्यूल को सफलतापूर्वक सत्यापित किया, और उनके अंदर के सभी व्यक्तिगत फंक्शनों में से 99.2% की जांच की।
बड़ी तस्वीर
वेरिस्ट्रक्ट को एक कच्चे, अप्रशिक्षित इंटर्न को निर्माण स्थल में फेंकने और उन्हें एक प्रोजेक्ट मैनेजर, एक सुरक्षा मैनुअल, एक विशेष टूल किट और एक क्वालिटी कंट्रोल टीम देने के बीच के अंतर के रूप में समझें।
यह एआई या इंसान की जगह नहीं लेता है; यह उन्हें व्यवस्थित (orchestrate) करता है। यह एआई की कच्ची रचनात्मकता को एक कठोर, चरण-दर-चरण प्रक्रिया के माध्यम से निर्देशित करता है जो फॉर्मल वेरिफिकेशन के सख्त नियमों को समझती है। यह हमें एक ऐसे भविष्य के एक कदम करीब लाता है जहाँ हमारे महत्वपूर्ण सॉफ्टवेयर (जैसे सेल्फ-ड्राइविंग कार या बैंकिंग सिस्टम) को स्वचालित रूप से सुरक्षित सिद्ध किया जा सके, बिना किसी मानव गणितज्ञ की टीम द्वारा कोड की हर एक लाइन को जांचने की आवश्यकता के।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।