VeriAct: Beyond Verifiability -- Agentic Synthesis of Correct and Complete Formal Specifications
यह शोध पत्र VeriAct को प्रस्तुत करता है, जो एक सत्यापन-निर्देशित एजेंटिक फ्रेमवर्क (verification-guided agentic framework) है जो प्रॉम्प्ट-आधारित संश्लेषण (prompt-based synthesis) की सीमाओं और मानक सत्यापनकर्ताओं (standard verifiers) की अपर्याप्तता को दूर करने के लिए औपचारिक विशिष्टताओं (formal specifications) को पुनरावृत्ति के माध्यम से परिष्कृत करता है ताकि यह सुनिश्चित किया जा सके कि वे न केवल सत्यापन योग्य हैं बल्कि वास्तव में सही और पूर्ण भी हैं।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक सख्त बिल्डिंग इंस्पेक्टर (Verifier) हैं जो एक आर्किटेक्ट (AI) द्वारा बनाए गए नए घर की जांच कर रहे हैं।
सॉफ्टवेयर की दुनिया में, "फॉर्मल स्पेसिफिकेशन" (Formal Specifications) ब्लूप्रिंट और सुरक्षा अनुबंधों की तरह होते हैं जो प्रोग्राम के लिए बनाए जाते हैं। वे कंप्यूटर को ठीक-ठीक बताते हैं कि कोड को क्या करना चाहिए और उसे क्या नहीं करना चाहिए। यदि कोड इन नियमों का पालन करता है, तो सॉफ्टवेयर सुरक्षित और विश्वसनीय होता है।
लंबे समय से, लोग AI का उपयोग इन ब्लूप्रिंट्स को स्वचालित रूप से लिखने के लिए करने की कोशिश कर रहे हैं। समस्या यह है कि AI अक्सर ऐसे ब्लूप्रिंट लिखता है जो इंस्पेक्टर को तो एकदम सही लगते हैं, लेकिन वास्तव में वे बेकार या खतरनाक होते हैं।
यहाँ एक सरल विवरण दिया गया है कि इस शोध पत्र, VeriAct, ने क्या खोजा और इस समस्या को कैसे ठीक किया।
1. समस्या: "पासिंग ग्रेड" का जाल (The "Passing Grade" Trap)
शोधकर्ताओं ने पाया कि वर्तमान AI उपकरण इंस्पेक्टर से "पास" प्राप्त करने में तो बहुत अच्छे हैं, लेकिन वे अच्छे ब्लूप्रिंट लिखने में बहुत खराब हैं।
- उपमा (Analogy): कल्पना कीजिए कि आपने AI से एक दरवाजे के लिए नियम लिखने को कहा: "दरवाजा खुला होना चाहिए।"
- इंस्पेक्टर का दृष्टिकोण: इंस्पेक्टर दरवाजे की जांच करता है। दरवाजा खुला है। नियम पूरा हुआ। पास!
- वास्तविकता: यह नियम बेकार है। यह यह नहीं बताता कि दरवाजा कब खुला होना चाहिए, या अगर बारिश हो रही हो तो क्या होगा। यह यह भी नहीं रोकता कि जब आपको दरवाजा बंद चाहिए हो, तब भी वह खुला रहे।
- शोध पत्र की खोज: AI मॉडल "तुच्छ" (trivial) नियम लिख रहे थे (जैसे "दरवाजा खुला है") जो तकनीकी रूप से परीक्षण में पास तो हो गए, लेकिन वे वास्तव में यह वर्णन नहीं कर पाए कि सॉफ्टवेयर को कैसे व्यवहार करना चाहिए। वे "सिस्टम को चकमा" दे रहे थे।
2. पहला प्रयास: निर्देशों में बदलाव (Prompt Optimization)
शोधकर्ताओं ने इसे बेहतर निर्देश (जिसे "प्रॉम्प्ट ऑप्टिमाइज़ेशन" कहा जाता है) देकर ठीक करने की कोशिश की। उन्होंने GEPA नामक एक स्मार्ट सिस्टम का उपयोग किया जो एक कोच की तरह काम करता था, जो AI को कहता था: "तुम्हें पास तो कर दिया गया, लेकिन तुम्हारा नियम बहुत अस्पष्ट था। फिर से कोशिश करो।"
- परिणाम: AI इंस्पेक्टर के टेस्ट में पास होने में बेहतर हो गया।
- पेंच: यह एक सीमा (ceiling) पर पहुँच गया। कोच के होने के बावजूद, AI अभी भी ऐसे नियम लिख रहा था जो बहुत सरल थे या जिनमें महत्वपूर्ण विवरणों की कमी थी। वह सही दिखने में तो अच्छा था, लेकिन सही होने में नहीं।
3. नया टूल: Spec-Harness (द स्ट्रेस टेस्ट)
शोधकर्ताओं को एहसास हुआ कि इंस्पेक्टर (Verifier) को बेवकूफ बनाना बहुत आसान था। उन्हें एक नए टूल की आवश्यकता थी जो यह जांच सके कि ब्लूप्रिंट वास्तव में पूर्ण और सटीक है या नहीं। उन्होंने Spec-Harness बनाया।
- उपमा: केवल इंस्पेक्टर से यह पूछने के बजाय कि "क्या दरवाजा खुला है?", Spec-Harness एक स्ट्रेस टेस्ट है।
- यह दरवाजे को तोड़ने की कोशिश करता है। यह पूछता है: "अगर कोई दरवाजे को तब धक्का दे जब उसे लॉक होना चाहिए? क्या तुम्हारा नियम उन्हें रोक पाता है?"
- यह जांचता है: "यदि मैं बाहर का तापमान बदल दूँ, तो क्या नियम अभी भी कायम रहता है?"
- चौंका देने वाली खोज: जब उन्होंने Spec-Harness का उपयोग किया, तो उन्होंने पाया कि AI द्वारा लिखे गए अधिकांश ब्लूप्रिंट (यहाँ तक कि वे भी जो इंस्पेक्टर के टेस्ट में पास हुए थे) वास्तव में दोषपूर्ण थे। वे या तो बहुत कमजोर थे (बुरी चीजों को होने दे रहे थे) या बहुत सख्त (अच्छी चीजों को रोकने वाले थे)।
4. समाधान: VeriAct (द सेल्फ-करेक्टिंग आर्किटेक्ट)
चूंकि AI को केवल "बेहतर करने के लिए कहा" नहीं जा सकता था, इसलिए शोधकर्ताओं ने VeriAct नामक एक नया सिस्टम बनाया। VeriAct को एक बिल्ट-इन क्वालिटी कंट्रोल टीम वाले आर्किटेक्ट के रूप में समझें।
केवल एक ब्लूप्रिंट लिखने और उसे सौंप देने के बजाय, VeriAct एक लूप (loop) में काम करता है:
- ड्राफ्ट (Draft): AI एक नियम लिखता है।
- निरीक्षण (Inspect): Verifier जांचता है कि क्या यह कानूनी रूप से सही है।
- स्ट्रेस टेस्ट (Stress Test): Spec-Harness इसे तोड़ने की कोशिश करता है।
- फीडबैक (Feedback): यदि नियम बहुत कमजोर या बहुत सख्त है, तो VeriAct AI को ठीक-ठीक बताता है कि वह कहाँ विफल हुआ।
- मरम्मत (Repair): AI उस विशिष्ट फीडबैक के आधार पर नियम को फिर से लिखता है।
- दोहराना (Repeat): यह तब तक चलता रहता है जब तक कि नियम न केवल "कानूनी" हो जाए, बल्कि वास्तव में परफेक्ट न हो जाए।
मुख्य निष्कर्ष (The Bottom Line)
- पहले: AI ऐसे नियम लिखता था जो इंस्पेक्टर को तो धोखा दे देते थे लेकिन वास्तविक दुनिया में विफल हो जाते थे।
- बाद में (VeriAct): AI एक सावधान इंजीनियर की तरह कार्य करता है। वह एक नियम लिखता है, हजारों "क्या-अगर" (what-if) परिदृश्यों के विरुद्ध उसका परीक्षण करता है, अपनी गलतियों को सुधारता है, और तभी रुकता है जब नियम वास्तव में मजबूत हो जाता है।
संक्षेप में: यह शोध पत्र सिद्ध करता है कि केवल इसलिए कि कोड एक टेस्ट पास कर लेता है, इसका मतलब यह नहीं है कि वह अच्छा है। वास्तव में विश्वसनीय सॉफ्टवेयर प्राप्त करने के लिए, हमें ऐसे AI की आवश्यकता है जो केवल टेस्ट पास न करे, बल्कि सक्रिय रूप से अपनी गलतियों को खोजे और उन्हें तब तक ठीक करे जब तक कि काम सही ढंग से पूरा न हो जाए।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।