When Agda met Vampire
यह शोध पत्र एक प्रोटोटाइप सिस्टम प्रस्तुत करता है जो एक साझा इक्वेशनल हॉर्न फ्रैगमेंट (equational Horn fragment) के माध्यम से प्रूफ़ ऑब्लिगेशन्स (proof obligations) को अनुवादित करके Agda और Vampire ATP के बीच सेतु बनाता है, जिससे उन जटिल गणितीय गुणों के लिए स्वचालित रचनात्मक प्रमाणों (constructive proofs) का निर्माण संभव हो पाता है जिन्हें पहले कई दिनों के मैनुअल प्रयास की आवश्यकता होती थी।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक मास्टर आर्किटेक्ट (प्रूफ असिस्टेंट, विशेष रूप से Agda) हैं जो एक गगनचुंबी इमारत बना रहे हैं जिसे पूरी तरह से सुरक्षित होना चाहिए। हर एक ईंट, बीम और बोल्ट का निरीक्षण और अनुमोदन किया जाना चाहिए। यदि एक भी ईंट थोड़ी सी भी अपनी जगह से हटती है, तो पूरी इमारत को असुरक्षित माना जाता है।
समस्या यह है कि यह निरीक्षक अविश्वसनीय रूप से सूक्ष्म है लेकिन बहुत धीमा भी है। वे हर एक विवरण को मैन्युअल रूप से जांचते हैं। यदि आपको यह सिद्ध करना है कि एक विशिष्ट खिड़की एक विशिष्ट फ्रेम में फिट बैठती है, तो निरीक्षक इसे सत्यापित करने में घंटों लगा सकता है, भले ही वह एक मानक खिड़की हो।
यहाँ प्रवेश होता है Vampire का, जो एक सुपर-फास्ट, हाई-स्पीड रोबोट डिटेक्टिव है। Vampire पहेलियों को सुलझाने और तुरंत कनेक्शन खोजने में माहिर है। हालाँकि, Vampire की एक शर्त है: यह एक अलग भाषा (क्लासिकल लॉजिक) बोलता है और नियमों का एक अलग सेट उपयोग करता है। यदि आप Vampire से कोई समस्या हल करने के लिए कहते हैं, तो वह चिल्ला सकता है, "मुझे उत्तर मिल गया!" लेकिन इसकी व्याख्या एक ऐसे कोड में लिखी होती है जिसे आपका निरीक्षक नहीं समझता या उस पर भरोसा नहीं करता।
यह पेपर एक अनुवादक और एक पुल बनाने के बारे में है जो धीमे, सख्त आर्किटेक्ट और तेज़, अराजक रोबोट के बीच सेतु का काम करता है।
मुख्य समस्या: दो अलग दुनिया
- Agda (द आर्किटेक्ट): "कंस्ट्रक्टिव लॉजिक" (Constructive Logic) में काम करता है। इसका अर्थ है कि कुछ अस्तित्व में है, यह सिद्ध करने के लिए, आपको वास्तव में उसे बनाना होगा। यह ऐसा है जैसे कहना, "मैं सिद्ध कर सकता हूँ कि मेरे पास एक चाबी है क्योंकि मैं उसे अपने हाथ में पकड़े हुए हूँ।"
- Vampire (द रोबोट): "क्लासिकल लॉजिक" (Classical Logic) में काम करता है। यह यह कहने में सहज है कि, "मैं सिद्ध कर सकता हूँ कि एक चाबी मौजूद है क्योंकि यदि वह नहीं होती, तो दरवाजा बंद होता, जो कि असंभव है।" यह तेज़ है लेकिन हमेशा "चाबी को" अपने हाथ में नहीं रखता; यह बस जानता है कि वह वहाँ है।
आमतौर पर, ये दोनों एक-दूसरे से बात नहीं कर सकते। यदि आप Vampire को एक काम भेजते हैं, तो वह एक ऐसा प्रमाण वापस लाता है जिसे Agda अस्वीकार कर देता है क्योंकि वह "बहुत अधिक क्लासिकल" है।
समाधान: "हॉर्न क्लॉज" ब्रिज (The "Horn Clause" Bridge)
लेखकों ने महसूस किया कि हालांकि दोनों भाषाएँ बहुत अलग हैं, वे एक छोटा, सामान्य बोली (dialect) साझा करती हैं जिसे Horn Clauses कहा जाता है। इसे एक सरल, सार्वभौमिक "पिजिन" भाषा के रूप में सोचें जिसे आर्किटेक्ट और रोबोट दोनों समझ सकते हैं। यह अंग्रेजी के एक सरल संस्करण जैसा है जहाँ आप केवल ऐसी चीजें कहते हैं जैसे:
- "यदि A सत्य है, और B सत्य है, तो C सत्य है।"
- "यदि X, Y के बराबर है, और Y, Z के बराबर है, तो X, Z के बराबर है।"
उन्होंने आर्किटेक्ट की पूरी जटिल भाषा को अनुवाद करने की कोशिश नहीं की। इसके बजाय, उन्होंने उन विशिष्ट, नियमित कार्यों की पहचान की (जैसे कि यह जांचना कि दो बीजगणितीय व्यंजक समान हैं या नहीं) जो इस सरल बोली में फिट बैठते हैं।
यह कैसे काम करता है: तीन-चरणीय नृत्य
अनुवाद (Agda से Vampire तक):
जब आर्किटेक्ट (Agda) किसी उबाऊ, दोहराव वाले कार्य (जैसे कि रूट्स ऑफ यूनिटी के बारे में एक जटिल गणितीय गुण सिद्ध करना) पर फंस जाता है, तो वह एक विशेष दर्पण (जिसे Reflection कहा जाता है) का उपयोग करके समस्या को देखता है। वह जटिल गणितीय समस्या को सरल "Horn Clause" बोली में अनुवादित करता है और उसे रोबोट (Vampire) को भेज देता है।डिटेक्टिव वर्क (Vampire हल करता है):
Vampire तेजी से अंदर आता है, पहेली को हल करता है, और एक सेकंड के अंश में समाधान चिल्लाकर बताता है। लेकिन, क्योंकि Vampire एक क्लासिकल डिटेक्टिव है, इसका समाधान एक रिफ्यूटेशन (refutation) की तरह दिखता है (उदाहरण के लिए, "यह असंभव है कि उत्तर गलत हो!")।पुनर्निर्माण (Vampire से Agda तक):
यही जादू का काम है। लेखकों ने एक छोटा, चतुर इंजन बनाया है (जो Prolog में लिखा गया है, जो तर्क पहेलियों के लिए अच्छी भाषा है) जो एक अनुवादक के रूप में कार्य करता है।- यह Vampire के "गलत होना असंभव है" वाले प्रमाण को लेता है।
- यह इसे यांत्रिक रूप से, चरण-दर-चरण, "यहाँ चाबी है" वाले प्रमाण में फिर से लिखता है।
- यह क्लासिकल लॉजिक को वापस कंस्ट्रक्टिव लॉजिक में बदल देता है।
- अंत में, यह इस नए, पूरी तरह से फॉर्मेट किए गए प्रमाण को आर्किटेक्ट (Agda) को सौंप देता है।
Agda इस नए प्रमाण की जाँच करता है। चूंकि इसे Agda के सख्त नियमों के अनुसार चरण-दर-चरण बनाया गया है, इसलिए Agda इसे तुरंत स्वीकार कर लेता है।
वास्तविक परीक्षण: कॉम्प्लेक्स फील्ड (The Complex Field)
यह सिद्ध करने के लिए कि यह काम करता है, लेखकों ने एक वास्तविक, कठिन समस्या पर इसे आजमाया: "रूट्स ऑफ यूनिटी के साथ एक कॉम्प्लेक्स फील्ड" के गुणों को सत्यापित करना।
- ब्रिज के बिना: Agda का उपयोग करते हुए एक पेशेवर गणितज्ञ को इन गुणों को मैन्युअल रूप से सिद्ध करने में दो पूरे दिन बिताने पड़े।
- ब्रिज के साथ: इस सिस्टम ने इसे एक सेकंड के एक अंश में स्वचालित रूप से कर दिया।
यह क्यों महत्वपूर्ण है
इसे गणितज्ञों के लिए एक स्पेल-चेकर (spell-checker) के रूप में सोचें।
पहले, यदि आप प्रमाणों की एक लंबी, जटिल पुस्तक लिखना चाहते थे, तो आपको हर एक वाक्य को मैन्युअल रूप से जांचना पड़ता था। यह थका देने वाला और धीमा था।
अब, यह सिस्टम एक "हैमर" (Hammer - इस क्षेत्र में उपयोग किया जाने वाला शब्द) के रूप में कार्य करता है। यह प्रमाण के उबाऊ, दोहराव वाले, यांत्रिक भागों को संभालता है ताकि मानव गणितज्ञ बड़े, रचनात्मक विचारों पर ध्यान केंद्रित कर सके।
संक्षेप में:
लेखकों ने एक हल्का अनुवादक बनाया है जो एक धीमे, सख्त, कंस्ट्रक्टिव प्रूफ असिस्टेंट को एक तेज़, क्लासिकल थ्योरम प्रोवर की गति उधार लेने की अनुमति देता है। वे समस्या को एक सरल भाषा में अनुवादित करते हैं, रोबोट को हल करने देते हैं, और फिर रोबोट के बिखरे हुए समाधान को एक साफ, भरोसेमंद प्रमाण में वापस अनुवादित करते हैं जिसे सख्त निरीक्षक स्वीकार कर सके। यह काम के कई दिनों को बचाता है और सत्यापित सॉफ्टवेयर बनाना बहुत आसान बनाता है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।