Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

जासूसी गाइड: चीजों को मेल बिठाना

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

द दशकों से, कंप्यूटर वैज्ञानिक मशीनों को इस पहेली को स्वचालित रूप से हल करना सिखाने की कोशिश कर रहे हैं। लक्ष्य केवल यह नहीं है कि कंप्यूटर "हाँ, वे मेल खाते हैं" कहे, बल्कि यह है कि कंप्यूटर उस प्रक्रिया का चरण-दर-चरण नुस्खा (एल्गोरिदम) खुद तैयार करे जिससे वे मेल खा सकें। इसे डिडक्टिव प्रोग्राम सिंथेसिस (deductive program synthesis) कहा जाता है। इसे एक सुपर-स्मार्ट रोबोट से गणित का प्रमेय (theorem) सिद्ध करने के लिए कहने जैसा समझें, लेकिन अंत में केवल "Q.E.D." लिखने के बजाय, रोबोट को आपको एक काम करने वाला सॉफ़्टवेयर सौंपना होगा जो समस्या को हल करता हो। पेच क्या है? रोबोट को अपने सॉफ़्टवेयर के बारे में पूरी तरह से आश्वस्त होना होगा क्योंकि प्रमाण (proof) ही उसकी गारंटी है। यदि प्रमाण सही है, तो प्रोग्राम काम करेगा। यदि प्रमाण विफल होता है, तो प्रोग्राम बेकार है।

पेपर की बड़ी खोज: एक रोबोट को अपना खुद का पहेली समाधान बनाना सिखाना

रिचर्ड वाल्डिंगर द्वारा लिखा गया यह पेपर, स्नार्क (Snark) नामक एक रोबोट की कहानी है जिसे केवल तर्क के नियमों का उपयोग करके एक यूनिफिकेशन एल्गोरिदम बनाने के लिए कहा गया था। लेखक ने स्नार्क को केवल उत्तर नहीं दिया; उसने उसे तार्किक नियमों का एक सेट (एक "एक्सिओमैटिक थ्योरी") और एक लक्ष्य दिया: "एक ऐसा प्रतिस्थापन (substitution) खोजें जो इन दो अभिव्यक्तियों को एक जैसा बना दे।"

पेपर का मुख्य निष्कर्ष यह है कि स्नार्क ने सफलतापूर्वक एक काम करने वाला यूनिफिकेशन एल्गोरिदम स्वचालित रूप से व्युत्पन्न (automatically derived) किया। इसने केवल किसी पुराने एल्गोरिदम की नकल नहीं की; इसने एक नया संस्करण खोजा जो पिछले कुछ मैनुअल प्रयासों की तुलना में वास्तव में अधिक कुशल और समझने में आसान है। रोबोट ने इसे एक विशाल तार्किक पहेली के रूप में मानकर किया। इसने एक अस्पष्ट लक्ष्य से शुरुआत की और समस्या को छोटे मामलों में तोड़कर (जैसे, "क्या होगा यदि पहला आइटम एक स्थिरांक (constant) है?" या "क्या होगा यदि यह एक वेरिएबल है?"), एक जटिल "इफ-देन-एल्स" (if-then-else) निर्णय वृक्ष (decision tree) बनाया। यही वृक्ष अंतिम प्रोग्राम है।

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

रोबोट ने कैसे "सोचा"

यह समझने के लिए कि स्नार्क ने यह कैसे किया, कल्पना कीजिए कि आप एक बच्चे को खिलौनों के ढेर को छाँटना सिखा रहे हैं। आप केवल यह नहीं कहते "छाँटो"। आप उन्हें नियमों का एक सेट देते हैं: "यदि यह एक ब्लॉक है, तो इसे लाल बिन में रखें। यदि यह एक कार है, तो इसे नीले बिन में रखें।" लेकिन क्या होगा यदि खिलौना एक ब्लॉक और एक कार दोनों है? आपको उसके लिए भी एक नियम चाहिए।

स्नार्क ने डिडक्टिव टैबलो (deductive tableaux) नामक पद्धति का उपयोग किया। एक व्हाइटबोर्ड की कल्पना करें जिसमें दो कॉलम हैं: "हम क्या जानते हैं" (असर्शन) और "हमें क्या खोजना है" (लक्ष्य)।

1. लक्ष्य: "एक तरीका खोजें जिससे अभिव्यक्ति A और अभिव्यक्ति B एक जैसी दिखें।"
2. प्रक्रिया: स्नार्क लक्ष्य को देखता है और पूछता है, "क्या होगा यदि A एक वेरिएबल है? क्या होगा यदि यह एक स्थिरांक है?" यह समस्या को इन विभिन्न "मामलों" में विभाजित करता है।
3. "अहा!" क्षण: जब स्नार्क को एहसास होता है कि एक बड़ी समस्या को हल करने के लिए, उसे पहले उसी समस्या के एक छोटे संस्करण को हल करने की आवश्यकता हो सकती है, तो वह रिकर्सन (recursion) पेश करता है। यह ऐसा है जैसे कहना, "इस बड़े ढेर को छाँटने के लिए, मैं पहले बाएं हिस्से को छाँटूंगा, फिर दाएं हिस्से को छाँटूंगा, और फिर उन्हें मिला दूँगा।" पेपर बताता है कि स्नार्क को यहाँ बहुत सावधान रहना पड़ा ताकि यह सुनिश्चित हो सके कि वह अनंत काल तक छाँटता न रहे। इसने एक "वेल-फाउंडेड रिलेशन" (एक गणितीय गारंटी कि प्रत्येक चरण समस्या को सख्ती से छोटा बनाता है, जैसे 100 से 0 तक गिनती करना) का उपयोग किया ताकि यह सिद्ध किया जा सके कि प्रक्रिया अंततः समाप्त हो जाएगी।

"एनवायरनमेंट" वाली ट्रिक

पेपर की सबसे चतुर चालों में से एक समस्या को थोड़ा बदलकर उसे रोबोट के लिए आसान बनाना था। केवल यह पूछने के बजाय कि "A और B को कैसे मिलाया जाए?", स्नार्क से पूछा गया, "A और B को कैसे मिलाया जाए यह देखते हुए कि आपके पास पहले से ही मैचों की एक सूची है?" इस सूची को एनवायरनमेंट (environment) कहा जाता है।

इसे "साइमन कहता है" (Simon Says) के खेल की तरह समझें। यदि साइमन कहता है "अपनी नाक छुओ," तो आप करते हैं। लेकिन यदि साइमन "अपनी नाक छुओ" कहने के बाद कहता है "टोपी पहनो," तो आपको टोपी को याद रखना होगा और फिर नाक छूनी होगी। "एनवायरनमेंट" (टोपी) को ट्रैक करके, रोबोट एक अधिक कुशल एल्गोरिदम बना सकता है। पेपर सुझाव देता है कि यह तीन-आर्ग्युमेंट वाला संस्करण (अभिव्यक्ति A, अभिव्यक्ति B, और एनवायरनमेंट) वास्तव में उस सरल दो-आर्ग्युमेंट वाले संस्करण की तुलना में कंप्यूटर के लिए स्वचालित रूप से सिंथेसाइज करना आसान है जिसका उपयोग मनुष्य आमतौर पर करते हैं।

अंतिम परिणाम: एक नया नुस्खा

पेपर वास्तविक कोड दिखाता है जो स्नार्क ने तैयार किया है। यह "यदि यह, तो वह" निर्देशों की एक लंबी सूची जैसा दिखता है।

• यदि एनवायरनमेंट टूटा हुआ है, तो "विफलता" (failure) सिग्नल लौटाएं।
• यदि दोनों अभिव्यक्तियाँ पहले से ही एक समान हैं, तो वर्तमान मैचों की सूची लौटाएं।
• यदि एक वेरिएबल है और दूसरा स्थिरांक (constant) है, तो उन्हें बदलने के लिए एक नया नियम बनाएं।
• यदि दोनों जटिल संरचनाएं (जैसे वस्तुओं की सूची) हैं, तो उन्हें उनके बाएं और दाएं हिस्सों में तोड़ें, पहले बाएं हिस्से को हल करें, और फिर उस परिणाम का उपयोग दाएं हिस्से को हल करने के लिए करें।

पेपर इस बात पर जोर देता है कि यह प्रोग्राम सिद्ध रूप से सही (provably correct) है। क्योंकि प्रोग्राम को सीधे एक तार्किक प्रमाण से निकाला गया है, हम जानते हैं कि यह काम करता है। यदि प्रमाण कहता है कि "यह चरण मान्य है," तो कोड चरण भी मान्य है। लेखक नोट करते हैं कि हालांकि इस प्रमाण को खोजने में स्नार्क सिस्टम को लगभग 10 सेकंड लगे, असली मूल्य इसकी विधि में है: यह दिखाता है कि हम अनुमान लगाने और जाँचने के बजाय प्रमेयों को सिद्ध करके सॉफ़्टवेयर बना सकते हैं।

यह क्यों मायने रखता है (और यह अभी तक जादू क्यों नहीं है)

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

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