A Cost-Aware Probability Monad for Liquid Haskell

कल्पना कीजिए कि आप एक जासूस हैं जो एक रहस्य सुलझाने की कोशिश कर रहे हैं, लेकिन आप अंधेरी गली में सुराग नहीं ढूंढ रहे, बल्कि एक कंप्यूटर प्रोग्राम के अंदर देख रहे हैं। विशेष रूप से, आप उन प्रोग्रामों को देख रहे हैं जो यादृच्छिक (random) चुनाव करते हैं, जैसे कि कौन सा रास्ता लेना है यह तय करने के लिए सिक्का उछालना। कंप्यूटर विज्ञान की दुनिया में, इसे "प्रोबेबिलिस्टिक प्रोग्राम" (probabilistic program) कहा जाता है। ये प्रोग्राम जादुई पासे फेंकने वाले यंत्रों की तरह हैं; वे केवल एक काम नहीं करते, बल्कि कई चीजें करते हैं जिनके होने की अलग-अलग संभावनाएँ होती हैं। क्योंकि वे यादृच्छिक हैं, हम केवल यह नहीं पूछ सकते कि "क्या यह काम कर गया?" हमें यह पूछना होगा कि "औसतन यह कितना अच्छा काम कर रहा था?" और "इसे कोशिश करने में कितनी ऊर्जा या समय बर्बाद हुआ?"

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

यहीं पर ऑस्ट्रिया और जर्मनी के शोधकर्ताओं की एक टीम एक नया उपकरण लेकर आती है। उन्होंने 'लिक्विड हैस्केल' (Liquid Haskell) नामक एक प्रोग्रामिंग भाषा के लिए एक विशेष "कॉस्ट-अवेयर प्रोबेबिलिटी मोनैड" (cost-aware probability monad) बनाया है। एक "मोनैड" को एक जादुई बैकपैक (बस्ते) के रूप में सोचें जिसे एक प्रोग्राम अपने साथ ले जाता है। आमतौर पर, यह बैकपैक केवल एक यादृच्छिक चुनाव का परिणाम रखता है। लेकिन शोधकर्ताओं का यह नया बैकपैक विशेष है: इसमें एक अंतर्निहित कैलकुलेटर और एक जीपीएस (GPS) लगा है। हर बार जब प्रोग्राम एक कदम उठाता है, तो बैकपैक स्वचालित रूप से कुल लागत और उस कदम के होने की प्रायिकता को अपडेट करता है। यह केवल डेटा नहीं रखता; यह गणित को जानता है। इस स्मार्ट बैकपैक का उपयोग करके, शोधकर्ताओं ने दिखाया कि कंप्यूटर स्वचालित रूप से यादृच्छिक प्रोग्रामों की लागत की जाँच कर सकते हैं, जिससे एक कठिन मैन्युअल पहेली एक लगभग स्वचालित प्रक्रिया में बदल गई। उन्होंने 'मेल्डेबल हीप्स' और डेटा प्रबंधन जैसी क्लासिक समस्याओं पर इसका परीक्षण किया, जिससे सिद्ध हुआ कि उनकी नई विधि न केवल सटीक है, बल्कि पहले के तरीकों की तुलना में बहुत तेज़ और उपयोग में आसान भी है।

यादृच्छिक प्रोग्रामों के लिए जादुई बैकपैक

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

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

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

यह सरल शब्दों में इस प्रकार काम करता है:

1. बैकपैक गणित जानता है: जब प्रोग्राम एक सिक्का उछालता है (एक यादृच्छिक विकल्प), तो बैकपैक उस उछाल की औसत लागत की गणना स्वचालित रूप से करता है। इसे मानव द्वारा गणित लिखने की आवश्यकता नहीं होती; बैकपैक यह आपके लिए करता है।
2. यह सब कुछ ट्रैक करता है: जैसे-जैसे प्रोग्राम चलता है, बैकपैक एक स्कोर रखता है। यदि प्रोग्राम एक ऐसा कदम लेता है जिसमें 1 यूनिट समय लगता है, तो बैकपैक कुल में 1 जोड़ देता है। यदि प्रोग्राम दो रास्तों में विभाजित होता है, तो बैकपैक दोनों रास्तों की संयुक्त औसत लागत का पता लगा लेता है।
3. यह कंप्यूटर से बात करता है: शोधकर्ताओं ने लिक्विड हैस्केल नामक एक टूल का उपयोग किया, जो एक सुपर-स्मार्ट रोबोट की तरह है जो आपकी कोडिंग की गलतियों की जाँच करता है। अपने "कॉस्ट-अवेयर बैकपैक" को लिक्विड हैस्केल में डालकर, उन्होंने रोबोट को गणित की जाँच स्वचालित रूप से करने दिया। रोबोट कोड को देख सकता है और कह सकता है, "हाँ, यह यादृच्छिक सॉर्टिंग एल्गोरिदम औसतन 2(n+1) बार हार्मोनिक नंबर घटाकर n चरणों में लेगा," बिना किसी इंसान द्वारा प्रमाण लिखे।

बैकपैक का परीक्षण: हीप्स से लेकर हायरिंग तक

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

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

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

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

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

इसका भविष्य के लिए क्या अर्थ है

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

लेखकों ने दिखाया कि प्रोग्राम की संरचना (बैकपैक) में लागत-ट्रैकिंग को सीधे शामिल करके, आप दोनों दुनियाओं का सर्वश्रेष्ठ प्राप्त कर सकते हैं। कंप्यूटर अधिकांश काम स्वचालित रूप से कर सकता है, लेकिन जब गणित वास्तव में कठिन हो जाता है, तो इंसान पूरे प्रमाण को फिर से लिखे बिना मार्गदर्शन करने के लिए हस्तक्षेप कर सकता है।

उन्होंने यह भी सिद्ध किया कि उनकी विधि सत्यनिष्ठ (sound) है, जो एक फैंसी तरीका है यह कहने का कि "यह गणितीय रूप से सही है।" उन्होंने केवल अनुमान नहीं लगाया; उन्होंने दिखाया कि यदि रोबोट कहता है कि लागत X है, तो लागत वास्तव में X ही है।

हालाँकि, कुछ सीमाएँ भी हैं। पेपर नोट करता है कि उनका बैकपैक वर्तमान में केवल उन प्रोग्रामों के लिए काम करता है जो सीमित समय में और सीमित परिणामों के साथ समाप्त होते हैं। यह अभी उन प्रोग्रामों को नहीं संभाल सकता जो अनंत काल तक चल सकते हैं या जिनमें अनंत संभावनाएं हो सकती हैं। लेकिन आज हम जिन अधिकांश उपयोगी यादृच्छिक एल्गोरिदम का उपयोग करते हैं, उनके लिए यह उपकरण एक क्रांतिकारी बदलाव है। यह एक उबाऊ, त्रुटि-प्रवण कार्य को एक सुव्यवस्थित, अधिकतर स्वचालित प्रक्रिया में बदल देता है, जिससे तेज़, सस्ते और अधिक विश्वसनीय सॉफ़्टवेयर बनाना आसान हो जाता है।

संक्षेप में, शोधकर्ताओं ने हमारे डिजिटल खोजकर्ताओं के लिए एक स्मार्ट बैकपैक बनाया है। अब, जब हमारे प्रोग्राम अपने यादृच्छिक रोमांच पर निकलते हैं, तो वे अपना नक्शा और कैलकुलेटर अपने साथ रखते हैं, जिससे हमें पता चलता है कि खजाने तक पहुँचने की लागत कितनी है।