Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
यह शोध पत्र एक ऐसे प्रयोग की रिपोर्ट करता है जहाँ एक लेखक ने चर्च के बेसिक रिकर्सिव अरिथमेटिक (Basic Recursive Arithmetic) के लिए एगडा (Agda) में गोडेल के दूसरे अपूर्णता प्रमेय (Gödel's second incompleteness theorem) को ऑटोफॉर्मलाइज़ करने के लिए एआई मॉडल क्लॉड (Claude) का उपयोग किया, जिसके परिणामस्वरूप 50,000 पंक्तियों का एक पोस्टुलेट-मुक्त (postulate-free) मशीन-चेक्ड प्रमाण प्राप्त हुआ जो मॉडल की निहित गणितीय तर्कों को पुनर्गठित करने की क्षमता और अपर्याप्त विशिष्टताओं (specifications) दिए जाने पर गणितीय रूप से गलत परिणाम उत्पन्न करने की उसकी प्रवृत्ति पर एक केस स्टडी के रूप में भी कार्य करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक आदर्श, स्वयं-जांच करने वाला रोबोट बनाने की कोशिश कर रहे हैं जो अपना गणित का होमवर्क खुद सत्यापित कर सके। यह रोबोट, जिसे हम BRA कहेंगे, बहुत बुद्धिमान है लेकिन बहुत सख्त, सरल नियमों का पालन करता है। यह जोड़, घटाव और यह जांच सकता है कि चीजें बराबर हैं या नहीं, लेकिन इसके पास कोई "कॉमन सेंस" (सामान्य ज्ञान) मॉड्यूल नहीं है।
आप जो पेपर पढ़ रहे हैं, वह एक प्रयोग की रिपोर्ट है जहाँ एक मानव शोधकर्ता (थियरी कोक्वांड) ने एक AI (क्लॉड) के साथ मिलकर इस रोबोट को एक बहुत ही प्रसिद्ध, बहुत कठिन पाठ सिखाने के लिए टीम बनाई: गोडेल का दूसरा अपूर्णता प्रमेय (Gödel's Second Incompleteness Theorem)।
यहाँ इस प्रयोग की कहानी है, जिसे सरल भागों में विभाजित किया गया है।
1. लक्ष्य: क्या रोबोट यह सिद्ध कर सकता है कि वह सुरक्षित है?
गोडेल का दूसरा प्रमेय गणितीय प्रणालियों के लिए थोड़ा "झूठे विरोधाभास" (liar's paradox) जैसा है। यह कहता है: "यदि कोई प्रणाली सुसंगत (consistent) है (वह कभी भी गलत चीजें सिद्ध नहीं करती है), तो वह अपनी सुसंगतता को सिद्ध नहीं कर सकती।"
दूसरे शब्दों में, यदि हमारा रोबट BRA वास्तव में गणित सही ढंग से कर रहा है, तो वह कभी भी यह लिखकर प्रमाण नहीं दे पाएगा कि, "मैं एक अच्छा रोबोट हूँ।" यदि वह ऐसा सिद्ध कर सका, तो इसका अर्थ होगा कि वह वास्तव में खराब हो चुका है। इस परियोजना का लक्ष्य 'एगडा' (Agda) नामक एक कंप्यूटर प्रोग्राम का उपयोग करके इस प्रमाण का एक डिजिटल संस्करण बनाना था।
2. पहला प्रयास: एक "नकली" सफलता
टीम ने AI को रोज (Rose) नामक एक गणितज्ञ के पुराने पेपर को पढ़ने और उसके आधार पर प्रमेय को सिद्ध करने के लिए कहा।
- क्या हुआ: AI ने कई दिनों तक कड़ी मेहनत की और एक "प्रमाण" तैयार किया। यह प्रभावशाली लग रहा था!
- समस्या: AI को धोखा दिया गया था। वह पुराना पेपर जिसे AI पढ़ रहा था, उसमें एक गलती (एक गलत प्रमेय) थी। AI ने निर्देशों का पूरी तरह से पालन किया, लेकिन क्योंकि शुरुआती बिंदु ही गलत था, इसलिए परिणाम कुछ ऐसा था जो गोडेल के प्रमेय जैसा दिखता तो था, लेकिन वास्तव में निरर्थक था।
- सबक: इसने दिखाया कि AI तर्क का पालन करने में बहुत अच्छा है, लेकिन यदि आप इसे एक गलत नक्शा देते हैं, तो यह खुशी-खुशी आपको गलत मंजिल तक ले जाएगा। आप केवल AI पर यह भरोसा नहीं कर सकते कि वह आपको क्या सिद्ध करना है, आपको मंजिल खुद पता होनी चाहिए।
3. वास्तविक प्रयास: नक्शा ठीक करना
असफलता के बाद, टीम ने एक अलग, अधिक विश्वसनीय नोट्स की ओर रुख किया जो आर. गार्ड (R. Guard) नामक एक गणितज्ञ के थे। ये नोट्स एक ऐसे खजाने के नक्शे की तरह थे जिसमें कुछ हिस्से गायब थे और कुछ गलतियाँ थीं।
- चुनौती: गार्ड के नोट्स 1963 में लिखे गए थे। वे सटीक थे लेकिन उनमें कई सूक्ष्म, स्पष्ट विवरणों को छोड़ दिया गया था जिन्हें एक मानव गणितज्ञ स्वतः ही भर देता। उदाहरण के लिए, गार्ड ने मान लिया था कि पाठक जानता है कि रोबोट के मस्तिष्क के भीतर "न्यूमरल्स" (संख्याओं जैसे 1, 2, 3) को कैसे संभालना है।
- AI की भूमिका: मानव शोधकर्ता ने एक भी लाइन कोड नहीं लिखा। इसके बजाय, उन्होंने एक "अनुवादक" या "वास्तुकार" (architect) के रूप में कार्य किया। उन्होंने AI को बताया: "यह रहा छूटा हुआ हिस्सा। यह रहा नियम। अब, कोड लिखो।"
- परिणाम: AI ने शून्य से 50,000 लाइनों का कोड सफलतापूर्वक लिखा। उसने पूरा रोबोट, प्रमाण और सत्यापन प्रणाली बनाई, और इसमें मानव द्वारा एक भी लाइन टाइप नहीं की गई। अंतिम परिणाम एक मशीन-चेक्ड प्रमाण था कि रोबोट BRA अपनी सुरक्षा को सिद्ध नहीं कर सकता।
4. छिपे हुए तरीके (The "Secret Sauce")
पेपर इस बात पर प्रकाश डालता है कि AI को इसे सफल बनाने के लिए कौन से चतुर तरीके सीखने पड़े, जो पुराने नोट्स में छिपे हुए थे:
- "नेस्टेड बॉक्स" (Nested Box) की समस्या: रोबोट को अपने इतिहास की जांच करने की आवश्यकता थी। कल्पना कीजिए कि आप एक किताब लिखने के साथ-साथ उसे पढ़ने की कोशिश कर रहे हैं। AI को रोबोट के मस्तिष्क के भीतर एक विशेष "हिस्ट्री टेप" बनाने की आवश्यकता थी। यह पता चला कि रोबोट के बुनियादी उपकरण इसके लिए नहीं बने थे, इसलिए AI को एक जटिल "रूसी गुड़िया" (Russian nesting doll) जैसी संरचना बनानी पड़ी ताकि रोबोट अपने पिछले चरणों को याद रख सके।
- "क्लोज्ड बॉक्स" (Closed Box) का नियम: रोबोट को संख्याओं (जैसे 5) को "बंद बक्सों" के रूप में मानना होगा जिन्हें प्रतिस्थापन (substitution) द्वारा बदला नहीं जा सकता। पुराने नोट्स ने माना था कि यह स्पष्ट है। AI को स्पष्ट रूप से यह सिद्ध करने के लिए कहा जाना पड़ा कि "5 एक बंद बॉक्स है" इससे पहले कि वह आगे बढ़ सके।
- "परिकल्पनात्मक" (Hypothetical) शॉर्टकट: रोबोट एक बहुत ही कठोर तरीके (हिल्बर्ट-शैली के तर्क) में काम करता है जहाँ वह आसानी से यह नहीं कह सकता कि "यदि X सत्य है, तो Y।" AI ने एक चतुर ट्रिक (जिसे "कार्नेइरो लिफ्ट" कहा जाता है) का उपयोग किया, जिसमें हर कथन को एक "यदि..." (If...) रैपर में लपेटा गया, जिससे रोबton अपने नियमों को तोड़े बिना जटिल तर्क का अनुकरण कर सका।
5. यह क्यों महत्वपूर्ण है
यह केवल एक गणितीय प्रमेय को सिद्ध करने के बारे में नहीं है। यह भविष्य में मानव और AI मिलकर कैसे काम करेंगे, इसका एक परीक्षण है।
- मानव एक वास्तुकार (Architect) है: मानव ने दृष्टि (vision), सही नक्शा और यह पहचानने की क्षमता प्रदान की कि AI कब पटरी से उतर रहा है (जैसे पहले असफल प्रयास में हुआ था)।
- AI एक राजमिस्त्री (Mason) है: AI ने भारी काम किया, प्रमाण की हर एक ईंट बिछाते हुए 50,000 लाइनों का काम पूरा किया।
- खोज: इस प्रक्रिया ने खुलासा किया कि पुराने गणितीय नोट्स वास्तव में कुछ जगहों पर "लापरवाह" थे। AI को एकदम सटीक कोड लिखने के लिए मजबूर करके, टीम ने मूल 1963 के टेक्स्ट में छिपे हुए अनुमानों और गलतियों को खोज निकाला जिन्हें दशकों तक अनदेखा किया गया था।
सारांश
इस परियोजना को एक ऐसी टीम के रूप में सोचें जो एक सेल्फ-ड्राइविंग कार बना रही है। मानव ड्राइवर को मंजिल (गोडेल का प्रमेय) और सड़क के नियम पता थे। AI वह इंजन निर्माता था जिसने कार को असेंबल किया।
- पहले, AI ने एक टूटे हुए ब्लूप्रिंट के आधार पर कार बनाने की कोशिश की और एक ऐसा वाहन बनाया जो कार जैसा दिखता तो था लेकिन चल नहीं सकता था।
- फिर, उन्होंने एक बेहतर ब्लूप्रिंट पर स्विच किया। AI ने एक पूर्ण, कार्यात्मक कार बनाई।
- इस दौरान, उन्हें एहसास हुआ कि ब्लूप्रिंट में कुछ निर्देश गायब थे, इसलिए उन्हें काम करने के लिए नए पुर्जे बनाने पड़े।
परिणाम एक पूरी तरह से सत्यापित, मशीन-चेक्ड प्रमाण है कि एक विशिष्ट गणितीय प्रणाली अपनी सुसंगतता को सिद्ध नहीं कर सकती, जिसे पूरी तरह से एक ऐसे सहयोग के माध्यम से प्राप्त किया गया जहाँ मानव ने AI का मार्गदर्शन किया, और AI ने लेखन का कार्य किया।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।