Towards a Certifying Grounder

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

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

यह शोध पत्र CertiFOX नामक एक नया सिस्टम पेश करता है जो इस "प्रूफ लॉगिंग" को स्वयं अनुवाद चरण में लाता है। लेखक, जो KU Leuven और Vrije Universiteit Brussel की एक टीम है, ने एक ऐसा ढांचा बनाया है जो केवल समस्याओं को हल नहीं करता; बल्कि एक प्रमाण (certificate) भी लिखता है जो यह सिद्ध करता है कि उच्च-स्तरीय रहस्य से निम्न-स्तरीय चेकलिस्ट में अनुवाद सही ढंग से किया गया था। उन्होंने तीन मुख्य उपकरण बनाए हैं: प्रमाण लिखने के लिए एक नई भाषा, एक "ग्राउंडर" (अनुवादक) जो काम करते समय प्रमाण लिखता है, और एक "चेकर" (दूसरा जासूस) जो काम को सत्यापित करने के लिए प्रमाण को पढ़ता है। उनके प्रयोग दिखाते हैं कि यह प्रणाली वर्तमान शीर्ष-स्तरीय उपकरणों की तरह ही अच्छी तरह से काम करती है, और प्रमाण लिखने और जाँचने में लगने वाला अतिरिक्त समय बहुत कम है—केवल एक छोटा सा स्थिरांक कारक (constant factor)। उन्होंने केवल यह सुझाव नहीं दिया कि यह काम कर सकता है; उन्होंने इसे बनाया, वास्तविक पहेलियों पर परीक्षण किया, और साबित किया कि यह काम को बहुत अधिक धीमा किए बिना इस कार्य को संभाल सकता है।

जासूस की दुविधा: अनुवादक पर भरोसा करना

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

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

CertiFOX समाधान: दस्तावेजी साक्ष्य (The Paper Trail)

लेखकों ने महसूस किया कि जबकि हम अंतिम उत्तर की जाँच करने में अच्छे हो गए हैं (क्या कंप्यूटर ने समाधान ढूँढ लिया?), हम अनुवाद की जाँच करने में अच्छे नहीं रहे हैं (क्या शेफ ने सूची सही ढंग से लिखी?)। वे इस "विश्वास अंतराल" (trust gap) को भरना चाहते थे।

ऐसा करने के लिए, उन्होंने CertiFOX बनाया। कल्पना कीजिए कि CertiFOX एक नया प्रकार का किचन है जहाँ शेफ केवल खाना ही नहीं बनाता; बल्कि वह अपने द्वारा किए गए हर एक कदम का विस्तृत, चरण-दर-चरण डायरी भी रखता है।

1. GroundFOX: यह नया शेफ है। यह उच्च-स्तरीय रेसिपी लेता है और उसे निम्न-स्तरीय सूची में अनुवादित करता है। लेकिन काम करते समय, यह एक "प्रमाण" लिखता है। यह केवल यह नहीं कहता कि "मैंने एलिस के लिए केक बनाया"; यह कहता है, "मैंने अतिथि सूची देखी, एलिस को देखा, और 'एलिस के लिए बेक करें' लिखने के लिए नियम 4 लागू किया।"
2. प्रमाण प्रारूप (The Proof Format): यह डायरी की भाषा है। लेखकों ने नियमों का एक विशिष्ट सेट (जैसे व्याकरण) डिज़ाइन किया है जिसका शेफ को पालन करना चाहिए। ये नियम इतने सरल हैं कि एक कंप्यूटर आसानी से उन्हें पढ़ सकता है और सत्यापित कर सकता है कि प्रत्येक चरण पिछले चरण का तार्किक रूप से अनुसरण करता है।
3. CheckFOX: यह स्वतंत्र निरीक्षक है। यह स्वयं रहस्य को सुलझाने की कोशिश नहीं करता। यह केवल शेफ की डायरी पढ़ता है और गणित की जाँच करता है। "क्या शेफ ने वास्तव में सूची में एलिस को देखा? हाँ। क्या नियम ने उसके लिए बेक करने को कहा था? हाँ। ठीक है, यह चरण सही है।"

यह कैसे काम करता है: "गार्ड्स" का जादू

लेखकों ने एक चतुर ट्रिक का उपयोग किया जिसे वे ग्राउंडिंग नॉर्मल फॉर्म (GNF) कहते हैं। सरल शब्दों में, यह नियमों को व्यवस्थित करने का एक तरीका है ताकि शेफ अधिक स्मार्ट हो सके। आमतौर पर, एक शेफ को यह देखने के लिए दुनिया के हर व्यक्ति की जाँच करनी पड़ सकती है कि क्या वे अतिथि हैं। यह धीमा है। लेकिन GNF के साथ, नियमों में "गार्ड्स" (guards) शामिल होते हैं।

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

परीक्षण: क्या यह वास्तव में काम करता है?

टीम ने केवल इसे सिद्धांत में नहीं बनाया; उन्होंने इसे परीक्षण में डाला। उन्होंने कई मानक पहेलियाँ (जैसे मानचित्रों को रंगना, स्थिर विवाहों का मिलान करना और संख्याओं में पैटर्न खोजना) लीं और उन्हें अपने नए सिस्टम के माध्यम से चलाया। उन्होंने अपनी नई शेफ (GroundFOX) की तुलना दो अन्य प्रसिद्ध शेफों से की: IDP-Z3 और pycleno।

परिणाम प्रभावशाली थे।

• गति: नया शेफ विशेषज्ञों के लगभग बराबर तेज़ था। कुछ मामलों में, यह थोड़ा धीमा था, लेकिन अन्य मामलों में, यह बहुत प्रतिस्पर्धी था। इसने लगभग सभी पचलियों को समय सीमा के भीतर हल किया।
• प्रमाण की लागत: सबसे महत्वपूर्ण प्रश्न यह था: "डायरी लिखने के कारण यह कितना धीमा है?" उत्तर था: "बहुत अधिक नहीं।" प्रमाण लिखने के लिए अतिरिक्त समय बहुत कम था। और जब निरीक्षक (CheckFOX) ने डायरी पढ़ी, तो इसमें खाना पकाने की तुलना में केवल 2 से 3 गुना अधिक समय लगा। पूर्ण निश्चितता के लिए यह एक बहुत ही छोटा मूल्य है।
• मेमोरी: दिलचस्प बात यह है कि नया सिस्टम कुछ बहुत कठिन पहेलियों पर अन्य उपकरणों की तुलना में मेमोरी खत्म होने से बचने में बेहतर था।

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

निष्कर्ष

शोध पत्र यह निष्कर्ष निकालता है कि CertiFOX घोषणात्मक समाधान (declarative solving) को विश्वसनीय बनाने का एक व्यवहार्य और आशाजनक तरीका है। यह सिद्ध करता है कि आपके पास एक ऐसा सिस्टम हो सकता है जो न केवल कठिन समस्याओं को हल करता है, बल्कि यह गणितीय गारंटी भी प्रदान करता है कि अनुवाद सही ढंग से किया गया था।

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

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