A Sequent Calculus for General Inductive Definitions
यह शोध पत्र SCFO(ID) को प्रस्तुत करता है, जो एक नया सीक्वेंट कैलकुलस (sequent calculus) है जो स्थिर अर्थशास्त्र (stable semantics) के सिद्धांतों को अनुकूलित करके पिछले वाक्यात्मक (syntactic) सीमाओं को दूर करने के लिए, FO(ID) में सामान्य गैर-एकदिष्ट (non-monotone) आगमनात्मक परिभाषाओं (inductive definitions) के औपचारिक प्रमाणों का समर्थन करने हेतु मौजूदा LKID प्रणाली का विस्तार करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक रोबोट को दुनिया को समझना सिखाने की कोशिश कर रहे हैं। आप उसे ज्ञान बनाने के लिए नियमों का एक सेट देते हैं, जैसे "यदि यह एक पक्षी है, तो यह उड़ता है" या "यदि यह एक माता-पिता है, तो उसका एक बच्चा है।" यह आसान है। लेकिन क्या होगा यदि आप उसे कुछ अधिक कठिन सिखाना चाहते हैं, जैसे "यदि यह पक्षी नहीं है, तो यह नहीं उड़ता है"? या यहाँ तक कि और भी अजीब, "यदि यह झूठा नहीं है, तो यह सच बोलता है"?
ये "नकारात्मक" नियम (जो "नहीं" का उपयोग करते हैं) नॉन-मोनोटोनिक परिभाषाएं (non-monotone definitions) कहलाते हैं। ये शक्तिशाली हैं लेकिन खतरनाक भी हैं। यदि आप सावधान नहीं रहे, तो वे तार्किक लूप (logical loops) बना सकते हैं जो रोबोट के दिमाग को हमेशा के लिए घुमाते रहेंगे, जैसे कोई कुत्ता अपनी ही पूंछ का पीछा कर रहा हो। यही विरोधाभास (paradoxes) की समस्या है (जैसे प्रसिद्ध "यह वाक्य असत्य है")।
लंबे समय तक, कंप्यूटर वैज्ञानिकों को रोबोट को सुरक्षित रखने के लिए इन नियमों पर सख्त सुरक्षा घेरे लगाने पड़े थे। उन्होंने कहा, "आप 'नहीं' का उपयोग तभी कर सकते हैं जब आप एक बहुत ही विशिष्ट, उबाऊ क्रम का पालन करें।" इसने रोबोट को क्रैश होने से तो बचाया, लेकिन इसने उसे कई प्राकृतिक और उपयोगी चीजें सीखने से भी रोक दिया।
मुख्य विचार: एक नया नियमकोश
इस शोध पत्र के लेखक, रॉबे वैन डेन ईड और मार्क डेनेकर ने एक नया नियमकोश (एक "सीक्वेंट कैलकुलस" जिसे SCFO(ID) कहा जाता है) लिखा है, जो रोबोट को उन उबाऊ सुरक्षा घेरों के बिना इन पेचीदा, नॉन-मोनोटोनिक नियमों को सिखाने में मदद करता है।
इस नए नियमकोश को एक स्मार्ट निर्माण मैनुअल (smart construction manual) के रूप में सोचें।
1. निर्माण स्थल (तर्क/Logic)
कल्पना कीजिए कि आप एक घर बना रहे हैं।
- पुराना तरीका (मोनोटोनिक): आप एक ईंट रखते हैं, फिर उसके ऊपर दूसरी। एक बार ईंट वहां आ गई, तो वह वहीं रहती है। आप इसे कभी हटा नहीं सकते। यह सुरक्षित है लेकिन सीमित है।
- नया तरीका (नॉन-मोनोटोनिक): आप कह सकते हैं, "यदि यहाँ कोई दीवार नहीं है, तो एक खिड़की बनाओ।" लेकिन यदि आप बाद में दीवार बनाते हैं, तो खिड़की को गायब होना होगा। यह अधिक लचीला है लेकिन जोखिम भरा है। यदि आप सावधान नहीं रहे, तो आप एक ऐसे लूप में फंस सकते हैं जहाँ आप बार-बार एक ही दीवार बनाने और गिराने का काम करते रहेंगे।
लेखकों का नया सिस्टम रोबोट को इस "बनाने और गिराने" को सुरक्षित रूप से संभालने की अनुमति देता है। यह स्टेबल सिमेंटिक्स (Stable Semantics) नामक एक अवधारणा का उपयोग करता है, जो एक "रियलिटी चेक" की तरह है। यह पूछता है: "यदि मैं यह मान लूँ कि यह सत्य है, तो क्या यह सत्य ही रहता है? यदि मैं यह मान लूँ कि यह असत्य है, तो क्या यह असत्य ही रहता है?" यदि उत्तर "नहीं, यह आगे-पीछे बदलता रहता है" है, तो सिस्टम इसे एक विरोधाभास के रूप में पहचान लेता है और क्रैश होने के बजाय निर्माण को रोक देता है।
2. जादुई उपकरण: इंडक्शन हाइपोथेसिस (Induction Hypothesis)
उनके नए नियमकोश का मुख्य हिस्सा एक विशेष उपकरण है जिसे इंडक्शन रूल (Induction Rule) कहा जाता है।
कल्पना कीजिए कि आप यह सिद्ध करने की कोशिश कर रहे हैं कि स्कूल के हर छात्र ने यूनिफॉर्म पहनी है।
- मानक प्रमाण: आप पहले छात्र की जांच करते हैं। फिर आप कहते हैं, "यदि छात्र A यूनिफॉर्म पहने हुए है, तो छात्र B (जो A के बाद आता है) भी पहने हुए होगा।" आप इस तरह आगे बढ़ते रहते हैं।
- "नहीं" के साथ समस्या: क्या होगा यदि नियम यह हो कि "यदि कोई छात्र यूनिफॉर्म नहीं पहनता है, तो उसे डिटेंशन मिलता है"? किसी को डिटेंशन मिलने का प्रमाण देने के लिए, आपको यह सिद्ध करना होगा कि वह यूनिफॉर्म नहीं पहन रहा है। लेकिन यह सिद्ध करने के लिए कि वह यूनिफॉर्म नहीं पहन रहा है, आपको सुनिश्चित होना होगा कि किसी और ने उसे पहनने के लिए मजबूर नहीं किया है। यह उलझ जाता है।
लेखकों की तरकीब सरल लेकिन शानदार है: अपना अनुमान लगाते समय केवल "हाँ" वाले हिस्सों पर ध्यान दें।
जब वे एक अनुमान (एक "इंडक्शन हाइपोथेसिस") लगाते हैं कि रोबोट को क्या विश्वास करना चाहिए, तो वे केवल नियमों के "हाँ" (सकारात्मक) हिस्सों को अपने अनुमान से बदलते हैं। वे "नहीं" (नकारात्मक) हिस्सों को वैसे ही रहने देते हैं।
- उपमा: कल्पना कीजिए कि आप एक भूलभुलैया (maze) को हल करने की कोशिश कर रहे हैं। आप मानचित्र पर एक रास्ता खींचते हैं। यदि आप दीवार से टकराते हैं (एक नकारात्मक स्थिति), तो आप दीवार को फिर से बनाने की कोशिश नहीं करते; आप बस दीवार के अस्तित्व को स्वीकार करते हैं और आगे बढ़ते रहते हैं। "नहीं" वाले हिस्सों को अपने अनुमान में अनदेखा करके, आप उस लूप में फंसने से बच जाते हैं जहाँ आपका अनुमान दीवार को बदल देता है, जो आपके अनुमान को बदल देता है, जो फिर से दीवार को बदल देता है...
3. यह क्यों महत्वपूर्ण है
इस शोध पत्र से पहले, यदि आप किसी जटिल, स्व-संदर्भित प्रणाली (जैसे एक कंप्यूटर प्रोग्राम जो अपने स्वयं के कोड की जांच करता है, या एक कानूनी प्रणाली जो अपने स्वयं के अपवादों को परिभाषित करती है) के बारे में कुछ सिद्ध करना चाहते थे, तो आप अक्सर औपचारिक रूप से ऐसा नहीं कर पाते थे। आपको अंतर्ज्ञान (intuition) पर निर्भर रहना पड़ता था।
SCFO(ID) के साथ, अब आप:
- औपचारिक रूप से सिद्ध कर सकते हैं: आप गणितीय रूप से दिखा सकते हैं कि नियमों का एक जटिल सेट सही ढंग से काम करता है।
- विरोधाभासों को पकड़ सकते हैं: सिस्टम औपचारिक रूप से सिद्ध कर सकता है कि नियमों का एक सेट क्यों टूटा हुआ है (नॉन-टोटल)। उदाहरण के लिए, यह सिद्ध कर सकता है कि "लायर पैराडॉक्स" (Liar Paradox) का कोई समाधान नहीं है, बजाय इसके कि केवल यह कहे कि "रोबोट भ्रमित है।"
- वास्तविक दुनिया के तर्क को संभाल सकते हैं: यह ऐसी परिभाषाओं को संभालने की अनुमति देता है जो वास्तव में इंसानों के सोचने के तरीके जैसी दिखती हैं, जिसमें अपवाद और निषेध (negations) शामिल हैं, बिना उन्हें एक कठोर, अस्वाभाविक संरचना में मजबूर किए।
पकड़ (द "गोडेल" सीमा)
लेखक अपनी सीमाओं के बारे में ईमानदार हैं। वे कहते हैं, "हम सब कुछ सिद्ध नहीं कर सकते।"
यह एक प्रसिद्ध गणितीय नियम (गोडेल का अपूर्णता प्रमेय - Gödel's Incompleteness Theorem) के कारण है जो कहता है कि किसी भी ऐसी प्रणाली में जो संख्याओं को गिनने के लिए पर्याप्त जटिल है, हमेशा कुछ ऐसे सत्य कथन होंगे जिन्हें आप सिद्ध नहीं कर पाएंगे।
इसलिए, हालांकि उनका नया नियमकोश पिछले नियमों की तुलना में बहुत अधिक शक्तिशाली है, लेकिन यह जादू नहीं है। यह हर संभव पहेली को हल नहीं कर सकता। हालाँकि, यह पहले की तुलना में बहुत अधिक समस्याओं को हल करता है, और वह भी एक ऐसे तरीके से जो गणितीय रूप से सुदृढ़ है।
सारांश
इस शोध पत्र को तार्किक तर्क (logical reasoning) के ऑपरेटिंग सिस्टम को अपग्रेड करने के रूप में समझें।
- पहले: सिस्टम एक सख्त शिक्षक की तरह था जो केवल तभी सवाल पूछने देता था जब आप एक कठोर स्क्रिप्ट का पालन करते थे। यह सुरक्षित था, लेकिन यह जटिल, वास्तविक जीवन की स्थितियों को नहीं संभाल सकता था।
- अब: सिस्टम एक बुद्धिमान गुरु की तरह है। यह आपको "क्या होगा अगर" और "नहीं" से जुड़े जटिल, पेचीदा सवाल पूछने की अनुमति देता है। इसमें एक विशेष सुरक्षा तंत्र (इंडक्शन रूल) है जो आपको तार्किक जाल में गिरने से बचाता है, और यह यहाँ तक बता सकता है कि कोई प्रश्न अनुत्तरित क्यों है क्योंकि प्रश्न स्वयं एक विरोधाभास है।
यह कंप्यूटर वैज्ञानिकों को अधिक मजबूत, बुद्धिमान प्रणालियाँ बनाने की अनुमति देता है जो वास्तविक दुनिया की अव्यवस्थित, विरोधाभासी और जटिल प्रकृति के बारे में तर्क कर सकें।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।