FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning
FM-Agent एक नवीन फ्रेमवर्क है जो प्राकृतिक भाषा में कॉलर की अपेक्षाओं से फंक्शन-स्तर के विनिर्देश (specifications) उत्पन्न करके, बड़े पैमाने के सिस्टम के लिए कंपोजिशनल रीजनिंग को स्वचालित करने हेतु लार्ज लैंग्वेज मॉडल्स का लाभ उठाता है, जिससे जटिल कोडबेस के भीतर कुछ ही दिनों के भीतर सैकड़ों महत्वपूर्ण बग्स की खोज संभव हो पाती है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक विशाल निर्माण परियोजना (construction project) के प्रबंधक हैं। आपने एक टीम को काम पर रखा है जो अविश्वसनीय रूप से तेज़ और सुपर-स्मार्ट रोबोट्स (LLMs) की है ताकि वे एक गगनचुंबी इमारत बना सकें। ये रोबोट ब्लूप्रिंट तैयार करने और ईंटें बिछाने में किसी भी मानव टीम की तुलना में कहीं अधिक तेज़ हैं। लेकिन एक पेंच है: ये रोबोट कभी-कभी विचलित हो जाते हैं, भ्रमित (hallucinate) हो जाते हैं, या ऐसी छोटी गलतियाँ कर देते हैं जो बाद में पूरी इमारत को ढहा सकती हैं।
समस्या यह है कि इमारत इतनी विशाल है (100,000 से अधिक लाइनों का कोड, या "ईंटें") कि कोई भी इंसान त्रुटियों की जाँच करने के लिए हर एक ब्लूप्रिंट को नहीं पढ़ सकता। पारंपरिक सुरक्षा निरीक्षक (पुराने सत्यापन उपकरण) बेहतरीन हैं, लेकिन उन्हें काम शुरू करने से पहले हर कमरे के लिए एक सटीक, गणितीय नियम पुस्तिका लिखने की आवश्यकता होती है। चूंकि रोबोट कमरे बनाते हुए आगे बढ़ रहे हैं, और इंसान पूरी तरह से नहीं समझते कि रोबोट का अजीब तर्क क्या है, इसलिए वह नियम पुस्तिका लिखना असंभव है।
यहाँ FM-Agent आता है। इसे एक नए प्रकार के "AI सुरक्षा निरीक्षक" के रूप में सोचें जिसे पहले से नियम पुस्तिका लिखने की आवश्यकता नहीं है। इसके बजाय, यह यह समझने की कोशिश करता है कि इमारत को कैसा दिखना चाहिए यह देखते हुए कि कमरे एक-दूसरे से कैसे जुड़ते हैं।
FM-Agent कैसे काम करता है, इसे हमारे निर्माण सादृश्य (analogy) का उपयोग करके तीन सरल चरणों में तोड़कर समझाया गया है:
1. "टॉप-डाउन" जासूस (स्पेसिफिकेशन जनरेशन)
पुराना तरीका: आमतौर पर, किसी कमरे की जाँच करने के लिए, आप कमरे के अंदर की ईंटों को देखते हैं और अनुमान लगाने की कोशिश करते हैं कि उस कमरे को क्या करना चाहिए था। लेकिन यदि रोबोट ने ईंटें बिछाते समय कोई गलती की है, तो आपका अनुमान गलत होगा।
FM-Agent का तरीका: FM-Agent उस गलियारे (कॉलर) को देखता है जो कमरे के अंदर ले जाता है। यह पूछता है, "गलियारा इस कमरे से क्या उम्मीद करता है?"
- यदि गलियारा "भारी" लेबल वाला एक पैकेज भेजता है, तो कमरे को उसे संभालने के लिए पर्याप्त मजबूत होना ही चाहिए।
- यदि गलियारा "हल्का" पैकेज वापस मिलने की उम्मीद करता है, तो कमरे को कुछ हल्का ही वापस करना चाहिए।
केवल कमरे के भीतर की अव्यवस्थित ईंटों को देखने के बजाय, कमरे में प्रवेश करने वाले लोगों (कॉलर्स) की उम्मीदों को देखकर, FM-Agent हर कमरे के लिए एक "यूजर मैनुअल" (स्पेसिफिकेशन) लिख सकता है, भले ही कमरा खराब तरीके से बनाया गया हो। यह इमारत के शीर्ष से बेसमेंट तक नीचे की ओर बढ़ते हुए इन मैनुअलों का निर्माण करता है, जिससे यह सुनिश्चित होता है कि हर कमरे को अपना काम पता हो।
2. "नेचुरल लैंग्वेज" निरीक्षक (कोड रीजनिंग)
पुराना तरीका: पारंपरिक निरीक्षक केवल "गणित" की भाषा बोलते हैं। यदि आप रोबोट के बिखराव को सटीक गणितीय सूत्रों में अनुवाद नहीं कर सकते, तो वे जाँच नहीं कर सकते।
FM-Agent का तरीका: FM-Agent "मानव" भाषा बोलता है। यह "यूजर मैनुअल" (जो साधारण अंग्रेजी में लिखा गया है) को लेता है और उसकी तुलना वास्तविक कमरे से करता है।
- यह कमरे के माध्यम से चरण-दर-चरण चलता है।
- यह AI से पूछता है: "यदि मैं एक भारी पैकेज से शुरू करता हूँ, और मैं यह कदम उठाता हूँ, फिर वह कदम उठाता हूँ, तो क्या मेरे पास अंत में अभी भी एक भारी पैकेज होगा?"
- यदि गणित मेल नहीं खाता, या यदि अंतिम परिणाम यूजर मैनुअल से मेल नहीं खाता, तो FM-Agent इसे संभावित आपदा के रूप में चिह्नित करता है।
यह एक ऐसे अनुवादक की तरह है जो रोबोट के बिखरे हुए नोट्स को पढ़ सकता है और कह सकता है, "हे, तुमने कहा था कि तुम एक हल्का पैकेज वापस करोगे, लेकिन वास्तव में तुमने एक बड़ा पत्थर वापस दिया। यह एक बग है!"
3. "क्रैश टेस्ट" ड्राइवर (बग वैलिडेटर)
पुराना तरीका: कभी-कभी, निरीक्षक कहता है, "यह गलत लग रहा है," लेकिन वह इसे साबित नहीं कर पाता। वह केवल अनुमान लगाता है।
FM-Agent का तरीका: FM-Agent केवल अनुमान नहीं लगाता; यह परीक्षण करता है। जब इसे कोई संदिग्ध कमरा मिलता है, तो यह एक स्टंट ड्राइवर की तरह व्यवहार करता है।
- यह एक विशिष्ट परिदृश्य (टेस्ट केस) बनाता है जिसे विशेष रूप से उस विशिष्ट गलती को ट्रिगर करने के लिए डिज़ाइन किया गया है।
- यह बिल्डिंग सिमुलेशन चलाता है।
- यदि परीक्षण के दौरान इमारत वास्तव में हिलती है या कमरा ढह जाता है, तो FM-Agent कहता है, "आहा! मुझे एक असली बग मिल गया!" और डेवलपर्स को दिखाता है कि इसे ठीक करने के लिए क्या करना है।
यह एक बड़ी बात क्यों है?
शोधकर्ताओं ने चार विशाल प्रणालियों (एक कंपाइलर, एक ऑपरेटिंग सिस्टम, एक डेटाबेस, और एक AI फ्रेमवर्क) पर FM-Agent का परीक्षण किया, जिन्हें पूरी तरह से AI रोबोट द्वारा बनाया गया था। इन सिस्टमों का मानक तरीकों का उपयोग करके मनुष्यों द्वारा पहले ही परीक्षण किया जा चुका था, फिर भी FM-Agent ने 522 नए, गंभीर बग खोज निकाले जिन्हें बाकी सभी ने मिस कर दिया था।
- पैमाना (Scale): इसने केवल दो दिनों में 143,000 लाइनों के कोड जितने बड़े सिस्टम को संभाला।
- प्रभाव: इसने ऐसे बग खोजे जो क्रैश, डेटा हानि, या सुरक्षा छिद्रों का कारण बन सकते थे।
निष्कर्ष
FM-Agent एक सुपर-इंटेलिजेंट क्वालिटी कंट्रोल सिस्टम की तरह है जो समझता है कि एक फंक्शन को क्या करना चाहिए (उसका इरादा/intent), यह इस बात से अधिक महत्वपूर्ण है कि उसे वास्तव में कैसे बनाया गया है (उसका कार्यान्वयन/implementation)। ऊपर से नीचे की ओर "इरादे" को पढ़कर और फिर परिणामों का परीक्षण करके, यह हमारे विशाल, AI-निर्मित सॉफ्टवेयर सिस्टम को सुरक्षित रख सकता है, भले ही निर्माता AI गलतियाँ करें।
यह मानव इंजीनियरों की आवश्यकता को प्रतिस्थापित नहीं करता है, बल्कि यह उन्हें एक शक्तिशाली नया उपकरण देता है जो नींव में अदृश्य दरारों को इमारत गिरने से पहले पकड़ सके।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।