एक ऐसी दुनिया की कल्पना करें जहाँ रोबोट नए खोजकर्ता हैं, जो परमाणु कचरे के स्थलों, गहरे अंतरिक्ष और समुद्र तल में उन कामों के लिए जा रहे हैं जो इंसानों के लिए बहुत खतरनाक हैं। लेकिन यहाँ एक पेच है: ये रोबोट केवल रिमोट-कंट्रोल कारों जैसे साधारण मशीनें नहीं हैं; ये जटिल, मॉड्यूलर मशीनें हैं जिन्हें विशाल लेगो (Lego) सेट्स की तरह बनाया गया है। इनके पास कई अलग-अलग हिस्से हैं—देखने के लिए सेंसर, सोचने के लिए दिमाग और चलने के लिए पहिए—जो आपस में बात करते हैं। समस्या यह है कि जब आप दस लाख लेगो ईंटों को एक साथ जोड़ते हैं, तो यह सुनिश्चित करना अविश्वसनीय रूप से कठिन होता है कि पूरा टावर गिरेगा नहीं। कंप्यूटर विज्ञान की दुनिया में, इसे "सत्यापन" (verification) कहा जाता है, और यह यह सिद्ध करने की कला है कि एक रोबोट बिल्कुल वही करेगा जो आप चाहते हैं, और कुछ भी नहीं जो आप नहीं चाहते। इसे करने के लिए, वैज्ञानिक अक्सर "अनुबंधों" (contracts) का उपयोग करते हैं। एक अनुबंध को दो दोस्तों के बीच के वादे की तरह समझें: "यदि तुम मुझे एक साफ कमरा देते हो (मान्यता/assumption), तो मैं वादा करता हूँ कि मैं तुम्हारे लिए एक सैंडविच लाऊँगा (गारंटी/guarantee)।" यदि हर कोई अपना वादा निभाता है, तो पूरा सिस्टम काम करता है। लेकिन जब रोबोट जटिल होते जाते हैं, तो हर वादे की मैन्युअल रूप से जाँच करना असंभव हो जाता है।

यह शोध पत्र इन रोबमिक वादों को जाँचने का एक चतुर नया तरीका पेश करता है, विशेष रूप से उन रोबोटों के लिए जो ROS (रोबोट ऑपरेटिंग सिस्टम) नामक एक लोकप्रिय टूलकिट का उपयोग करके बनाए गए हैं। लेखक, जो कंप्यूटर वैज्ञानिकों की एक टीम है, एक "कंपोजिशनल" (compositional) दृष्टिकोण प्रस्तावित करते हैं। पूरे रोबोट को एक साथ सत्यापित करने के बजाय (जो कि आँखों पर पट्टी बाँधकर एक विशाल जिग्सॉ पहेली को हल करने जैसा है), वे रोबोट को उसके व्यक्तिगत टुकड़ों या "नोड्स" (nodes) में तोड़ देते हैं। वे प्रत्येक नोड के लिए एक विशिष्ट अनुबंध लिखते हैं, यह सिद्ध करते हुए कि यदि नोड को सही इनपुट मिलता है, तो वह निश्चित रूप से सही आउटपुट देगा। फिर, वे इन व्यक्तिगत अनुबंधों को आपस में जोड़ने के लिए नियमों के एक विशेष सेट (एक "कैलकुलस") का उपयोग करते हैं, यह दिखाते हुए कि यदि हर हिस्सा अपना वादा निभाता है, तो पूरा रोबोट अपना बड़ा, अंतिम वादा निभाएगा। उन्होंने "वांडा" (Vanda) नामक एक उपकरण भी बनाया जो स्वचालित रूप से इन लिखित अनुबंधों को डिजिटल "सुरक्षा गार्डों" में बदल देता है जो वास्तविक समय में रोबोट की निगरानी करते हैं, और यदि कोई वादा टूटता है तो "रुको!" चिल्लाने के लिए तैयार रहते हैं।

अपने विचार का परीक्षण करने के लिए, टीम ने केवल कोड नहीं लिखा; उन्होंने एक परमाणु भंडारण सुविधा की खोज करने वाले एक रोबोट रोवर का सिमुलेशन बनाया। रोबोट का काम रेडिएशन (विकिरण) की जांच करने के लिए 12 अलग-अलग स्थानों पर जाना था। यदि रेडिएशन बहुत अधिक हो जाता, तो रोबोट को मिशन छोड़ना पड़ता और वापस निकास की ओर भागना पड़ता। टीम ने रोबोट के "दिमाग" (एजेंट), उसकी "आँखों" (रेडिएशन सेंसर) और उसके "पैरों" (नेविगेशन सिस्टम) के लिए अनुबंध लिखे। उन्होंने प्रत्येक भाग को जाँचने के लिए विभिन्न तरीकों का उपयोग किया: कुछ की गणितीय प्रमाणों से जाँच की गई, कुछ की कंप्यूटर सिमुलेशन से, और कुछ की कोड समीक्षा से। परिणाम क्या रहा? सिस्टम काम कर गया। अनुबंधों ने सफलतापूर्वक विभिन्न सत्यापन विधियों को निर्देशित किया, और स्वचालित "सुरक्षा गार्डों" (रनटाइम मॉनिटर) ने बिना रोबोट की गति धीमी किए उसकी निगरानी की। यह शोध पत्र सुझाव देता है कि यह विधि जटिल, मॉड्यूलर रोबोटों को सुरक्षित और अधिक विश्वसनीय बनाने का एक शक्तिशाली तरीका है, भले ही वे अलग-अलग लोगों द्वारा अलग-अलग उपकरणों का उपयोग करके बनाए गए हिस्सों से बने हों।

मुख्य विचार: रोबोट वादा-निभाने वाली प्रणाली

कल्पना कीजिए कि आप एक परमाणु कचरे के ढेर की खोज करने के लिए एक विशाल, स्वायत्त रोबोट बना रहे हैं। यह रोबोट धातु का एक एकल ब्लॉक नहीं है; यह साथ मिलकर काम करने वाले विशेषज्ञों की एक टीम है। एक हिस्सा नेविगेटर (Navigator) है, जो यह तय करता है कि बिंदु A से बिंदु B तक कैसे पहुँचना है। दूसरा सेंसर (Sensor) है, जो हवा में रेडिएशन की मात्रा मापता है। तीसरा ब्रेन (Brain) है, जो यह तय करता है कि सेंसर जो देखता है उसके आधार पर आगे कहाँ जाना है।

पुराने दिनों में, यदि आप यह सुनिश्चित करना चाहते थे कि आपका रोबोट दीवार से न टकरा जाए या रेडिएशन से नष्ट न हो जाए, तो आप पूरे रोबोट का एक साथ परीक्षण करने का प्रयास कर सकते थे। लेकिन यह एक टूटे हुए कार इंजन को ठीक करने के लिए पूरी कार पर हथौड़े से मारने जैसा है। यह अव्यवस्थित है, और यदि कुछ गलत हो जाता है, तो आपको पता नहीं चलेगा कि किस हिस्से ने कारण दिया।

यह शोध पत्र एक स्मार्ट तरीका प्रस्तावित करता है: अनुबंध प्रणाली (The Contract System)।

प्रत्येक रोबोटिक हिस्से को एक कारखाने के कर्मचारी के रूप में सोचें। काम शुरू करने से पहले, वे एक अनुबंध पर हस्ताक्षर करते हैं।

• मान्यता (Assumption - "यदि"): "मैं अपना काम करूँगा यदि आप मुझे स्वच्छ डेटा देते हैं।"
• गारंटी (Guarantee - "तो"): "यदि आप मुझे स्वच्छ डेटा देते हैं, तो मैं आपको एक सही मानचित्र देने का वादा करता हूँ।"

इस शोध पत्र के लेखकों ने RCL (ROS कॉन्ट्रैक्ट लैंग्वेज) नामक एक विशेष भाषा बनाई है ताकि वे इन वादों को इस तरह लिख सकें जिसे कंप्यूटर समझ सके। वे फर्स्ट-ऑर्डर लॉजिक (FOL) नामक एक प्रकार के गणित का उपयोग करते हैं, जो मूल रूप से "यदि रेडिएशन लाल है, तो रोबोट को रुकना चाहिए" जैसे वाक्य लिखने का एक बहुत ही सटीक तरीका है।

जादुई गोंद: कैलकुलस (The Calculus)

यहाँ पेचीदा हिस्सा यह है। केवल इसलिए कि नेविगेटर अपना वादा निभाता है और सेंसर अपना वादा निभाता है, इसका मतलब यह नहीं है कि पूरा रोबोट अपने आप काम करेगा। आपको यह जानने की आवश्यकता है कि नेविगेटर का "आउटपुट" (मानचित्र) वास्तव में सेंसर के "इनपुट" (डेटा जिसकी उसे आवश्यकता है) से मेल खाता है।

लेखकों ने एक कैलकुलस (तार्किक नियमों का एक सेट) बनाया जो गोंद के रूप में कार्य करता है। यह एक मास्टर पहेली सुलझाने वाले की तरह है।

1. आप नेविगेटर के लिए अनुबंध देते हैं।
2. आप सेंसर के लिए अनुबंध देते हैं।
3. कैलकुलस जाँच करता है: "क्या नेविगेटर का मानचित्र देने का वादा, सेंसर के मानचित्र को स्वीकार करने के वादे से मेल खाता है?"
4. यदि वे मेल खाते हैं, तो कैलकुलस उन्हें एक साथ जोड़ देता है और एक सिस्टम-लेवल प्रॉमिस बनाता है: "यदि रोबोट बैटरी के साथ शुरू होता है, तो वह अंततः सभी सुरक्षित स्थानों पर जाएगा।"

इसे कंपोजिशनल वेरिफिकेशन (Compositional Verification) कहा जाता है। इसका अर्थ है कि आप छोटे टुकड़ों को अलग-अलग सत्यापित कर सकते हैं और फिर यह सिद्ध कर सकते हैं कि पूरा सिस्टम काम करेगा, बस यह देखकर कि टुकड़े एक दूसरे में कैसे फिट बैठते हैं।

सुरक्षा जाल: वांडा और सुरक्षा गार्ड

अनुबंध लिखना बढ़िया है, लेकिन क्या होगा यदि रोबोट वास्तव में चलते समय भ्रमित हो जाए? क्या होगा यदि कोई सेंसर खराब हो जाए?

लेखकों ने वांडा (Vanda) नामक एक उपकरण बनाया। वांडा को एक अनुवादक और एक सुरक्षा गार्ड दोनों के रूप में समझें।

1. अनुवादक (Translator): यह लिखित अनुबंधों (RCL) को लेता है और उन्हें कोड में बदल देता है जो रोबोट पर चल सकता है।
2. सुरक्षा गार्ड (Runtime Monitor): एक बार जब रोबोट चल रहा होता है, तो वांडा छोटे "सुरक्षा गार्ड" बनाता है जो रोबोट द्वारा भेजे गए और प्राप्त किए गए प्रत्येक संदेश की निगरानी करते हैं। यदि नेविगेटर कहता है, "मैं दरवाजे पर हूँ," लेकिन अनुबंध कहता है, "आप दरवाजे पर तभी हैं जब रेडिएशन कम है," तो गार्ड रेडिएशन की जाँच करता है। यदि रेडिएशन अधिक है, तो गार्ड चिल्लाता है, "उल्लंघन!" (Violation!)।

शोध पत्र दिखाता है कि ये गार्ड बहुत कुशल हैं। उनके परीक्षण में, रोबोट में गार्ड जोड़ने से उसकी गति पर बहुत कम प्रभाव पड़ा। यह एक कार में सुरक्षा कैमरे जोड़ने जैसा था; कार उतनी ही तेज़ चलती है, लेकिन अब आप जानते हैं कि यदि कोई चोरी करने की कोशिश करता है तो क्या होगा।

परीक्षण ड्राइव: न्यूक्लियर रोवर

यह सिद्ध करने के लिए कि यह काम करता है, टीम ने केवल बातें नहीं कीं; उन्होंने एक जैकल रोवर (Jackal rover) का सिमुलेशन बनाया जो परमाणु कचरे के भंडार की खोज कर रहा है।

• मिशन: रोबलेट को रेडिएशन स्तर की जांच करने के लिए 12 विशिष्ट स्थानों (वेपॉइंट्स) पर जाना था।
• नियम:
  • यदि रेडिएशन कम (हरा) या मध्यम (नारंगी) है, तो चलते रहें।
  • यदि रेडिएशन उच्च (लाल) है, तो तुरंत रुकें और निकास की ओर वापस भागें।
  • प्रत्येक स्थान की कम से कम एक बार यात्रा की जानी चाहिए।

उन्होंने इस रोबोट के लिए अपनी पद्धति लागू की:

1. चरण 1: उन्होंने रोबोट के सॉफ़्टवेयर को देखा और इसे चार मुख्य भागों वाले एक मॉडल में सरल बनाया: एजेंट (दिमाग), नेविगेशन (पैर), रेडिएशन सेंसर (आँखें), और लोकलाइजेशन (दिशा का बोध)।
2. चरण 2: उन्होंने प्रत्येक भाग के लिए अनुबंध लिखे। उदाहरण के लिए, एजेंट के अनुबंध में कहा गया, "यदि मैं लाल रेडिएशन देखता हूँ, तो मैं रोबोट को निकास की ओर जाने का आदेश दूँगा।"
3. चरण 3: उन्होंने कैलकुलस का उपयोग यह सिद्ध करने के लिए किया कि यदि सेंसर लाल देखता है, तो एजेंट जाने का आदेश देगा, और नेविगेशन वास्तव में रोबोट को चलाएगा।
4. चरण 4: उन्होंने प्रत्येक भाग को अलग-अलग तरीके से सत्यापित किया।
   • एजेंट (दिमाग) की जाँच एक मॉडल चेकर (एक उपकरण जो किसी प्रोग्राम द्वारा लिए जा सकने वाले हर संभावित पथ का परीक्षण करता है) का उपयोग करके की गई।
   • नेविगेशन (पैर) का परीक्षण 47 सिमुलेशन चलाकर किया गया जहाँ रोबोट ने यादृच्छिक स्थानों पर जाने की कोशिश की। यह औसतन 21.4 सेमी लक्ष्य से भटक गया, जो कि अनुमत सुरक्षा मार्जिन के भीतर था।
   • रेडिएशन सेंसर की जाँच एक गणितीय प्रमाण (होअर लॉजिक) के साथ की गई ताकि यह सुनिश्चित हो सके कि यह रेडिएशन को सही ढंग से हरा, नारंगी या लाल के रूप में वर्गीकृत करता है।
5. चरण 5: उन्होंने वांडा मॉनिटर्स को चालू किया। रोबोट ने मिशन चलाया, और मॉनिटर्स ने बारीकी से निगरानी की। उन्होंने पुष्टि की कि रोबोट ने नियमों का पालन किया: उसने स्थानों का दौरा किया और जब रेडिएशन बहुत अधिक हो गया तो वह वापस भाग गया।

यह भविष्य के लिए क्या मायने रखता है

शोध पत्र सुझाव देता है कि यह दृष्टिकोण सुरक्षित रोबोट बनाने के लिए एक गेम-चेंजर है, विशेष रूप से उन रोबोटों के लिए जो कई अलग-अलग हिस्सों से बने हैं।

• मिक्स एंड मैच: क्योंकि हर कोई अनुबंध पर सहमत है, आप "दिमाग" को किसी दूसरे से बदल सकते हैं। शायद एक टीम एक शानदार AI का उपयोग करती है, और दूसरी टीम सरल कोड का। जब तक वे दोनों एक ही अनुबंध (एक ही चीज़ करने का वादा) पर हस्ताक्षर करते हैं, कैलकुलस कहता है कि रोबोट अभी भी काम करेगा।
• विषम सत्यापन (Heterogeneous Verification): आपको हर हिस्से की जाँच करने के लिए एक ही उपकरण का उपयोग करने की आवश्यकता नहीं है। कुछ हिस्से गणित से जाँचने के लिए बेहतर होते हैं, अन्य सिमुलेशन से, और अन्य परीक्षणों से। अनुबंध इन सभी विभिन्न विधियों को जोड़ने वाली एक सामान्य भाषा के रूप में कार्य करते हैं।
• वास्तविक समय सुरक्षा (Real-Time Safety): रनटाइम मॉनिटर एक अंतिम सुरक्षा जाल के रूप में कार्य करते हैं। भले ही सत्यापन चरण में कुछ छूट गया हो, मॉनिटर वहाँ है ताकि रोबोट को पकड़ सके यदि वह वास्तव में काम करते समय कुछ खतरनाक करने लगे।

लेखक स्वीकार करते हैं कि उनकी पद्धति अभी भी पूर्ण नहीं है। यह मानती है कि डेटा सुचारू रूप से प्रवाहित होता है (एक समय में एक हिस्सा) और कि "गोंद" (कैलकुलस) वर्तमान में मनुष्यों द्वारा लगाया जाता है, न कि स्वचालित रूप से किसी कंप्यूटर द्वारा। लेकिन उन्होंने दिखाया है कि यह एक सिमुलेशन में काम करता है, और उनके पास इसे और भी बेहतर बनाने का एक स्पष्ट मार्ग है।

संक्षेप में, यह शोध पत्र हमें अपने रोबोटिक सहायकों पर विश्वास करने का एक नया तरीका देता है। केवल यह उम्मीद करने के बजाय कि वे काम करेंगे, हम उनके वादों को लिख सकते हैं, यह जाँच सकते हैं कि वादे आपस में मेल खाते हैं या नहीं, और यह सुनिश्चित करने के लिए एक सुरक्षा गार्ड तैनात कर सकते हैं कि वे अपना वचन निभाएं। और एक ऐसी दुनिया में जहाँ रोबोट एक दिन परमाणु कचरे की सफाई कर सकते हैं या मंगल ग्रह की खोज कर सकते हैं, वह मानसिक शांति अमूल्य है।