MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics
यह शोधपत्र MathlibLemma को प्रस्तुत करता है, जो एक स्वचालित LLM-आधारित पाइपलाइन है जो Lean Mathlib लाइब्रेरी का विस्तार करने के लिए लुप्त "लोकप्रिय" (folklore) लेम्मा की खोज और औपचारिकीकरण करती है, साथ ही AI-सहायता प्राप्त औपचारिक गणित को आगे बढ़ाने के लिए 4,000 से अधिक सत्यापित गणितीय कथनों का एक व्यापक बेंचमार्क स्थापित करती है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक रोबोट सहायक का उपयोग करके गणितीय ज्ञान का एक विशाल, पूर्ण पुस्तकालय बनाने की कोशिश कर रहे हैं। आपके पास एक विशाल, मौजूदा पुस्तकालय है जिसे Mathlib कहा जाता है (जो Lean प्रूफ़ असिस्टेंट के लिए बनाया गया है), यह गणित के तथ्यों के एक सुपर-व्यवस्थित विश्वकोश की तरह है।
हालाँकि, एक समस्या है: जबकि इस पुस्तकालय में बड़े, प्रसिद्ध प्रमेय (theorems) मौजूद हैं, इसमें हजारों छोटे, "स्पष्ट" तथ्य गायब हैं जिनका उपयोग मानव गणितज्ञ हर दिन बिना सोचे-समझे करते हैं। इन्हें folklore lemmas कहा जाता है।
इसे इस तरह सोचिए: यदि आप एक उपन्यास लिख रहे होते, तो आपको यह समझाने की आवश्यकता नहीं होती कि "एक वर्ग (square) की चार भुजाएँ होती हैं" या "यदि आप किसी संख्या में शून्य जोड़ते हैं, तो वह वैसी ही रहती है।" आप बस यह मान लेते हैं कि सभी को यह पता है। लेकिन एक रोबोट प्रूफ़-चेकर के लिए, यदि वह छोटा सा तथ्य पुस्तकालय में स्पष्ट रूप से नहीं लिखा है, तो वह अटक जाता है। यह ऐसा है जैसे आप एक घर बनाने की कोशिश कर रहे हों लेकिन आपको एहसास हो कि आप छत को थामने के लिए आवश्यक विशिष्ट प्रकार के कीलों को खरीदना भूल गए हैं। घर (प्रमाण/proof) वैचारिक रूप से सही है, लेकिन आप निर्माण पूरा नहीं कर सकते क्योंकि एक छोटा सा, "स्पष्ट" हिस्सा गायब है।
समस्या: "द लास्ट माइल" (अंतिम मील)
यह शोध पत्र तर्क देता है कि यह गायब "जुड़ने वाला ऊतक" (connective tissue) ही लास्ट माइल बाधा है। यह गणितज्ञों को इन शक्तिशाली कंप्यूटर उपकरणों का उपयोग उतनी आसानी से करने से रोकता है जितनी आसानी से वे वर्ड प्रोसेसर या कैलकुलेटर का उपयोग करते हैं। भले ही एक मानव को प्रमाण पता हो, कंप्यूटर उसे नहीं कर सकता क्योंकि इसमें छोटे, मध्यवर्ती चरण गायब हैं।
इसके अलावा, जब AI (लार्ज लैंग्वेज मॉडल्स) इन प्रमाणों को लिखने में मदद करने की कोशिश करता है, तो वह अक्सर विफल हो जाता है। क्यों? क्योंकि यदि AI पुस्तकालय में उस "स्पष्ट" तथ्य को नहीं ढूंढ पाता है, तो वह पूरे प्रमाण को शून्य से बनाने की कोशिश करता है। यह एक ब्लूप्रिंट के बिना पुल बनाने के लिए किसी को कहने जैसा है; वे रास्ता भटक सकते हैं, गलतियाँ कर सकते, या कल्पना (hallucinate) कर सकते हैं (चीजें बना सकते हैं) क्योंकि कार्य बहुत बड़ा है।
समाधान: MATHLIBLEMMA
लेखकों ने MATHLIBLEMMA नामक एक प्रणाली बनाई है। इसे इस प्रकार सोचिए कि यह उन लापता "स्पष्ट" तथ्यों को खोजने, उन्हें सही ढंग से लिखने और उन्हें सत्य सिद्ध करने के लिए बनाया गया एक चार-चरणीय कारखाना (four-stage factory) है।
यह कारखाना इस प्रकार काम करता है:
द एक्सप्लोरर (डिस्कवरी मॉड्यूल - खोजक):
कल्पना कीजिए कि एक जिज्ञासु लाइब्रेरियन मौजूदा पुस्तकालय को पढ़ता है और कहता है, "हे, हमारे पास त्रिभुजों के बारे में बहुत कुछ है, लेकिन हमारे पास इस नियम की कमी है कि जब आप एक को उल्टा कर देते हैं तो क्या होता है। यह शायद सच है, लेकिन यह गायब है!" यह मॉड्यूल मौजूदा तथ्यों के आधार पर इन लापता तथ्यों के लिए विचार मंथन करने के लिए AI का उपयोग करता है।द गेटकीपर (जज मॉड्यूल - द्वारपाल):
एक्सप्लोरर गलतियाँ कर सकता है। यह कुछ ऐसा सुझाव दे सकता है जो सुनने में अच्छा लगे लेकिन वास्तव में गणितीय रूप से गलत हो (जैसे यह कहना कि "सभी संख्याएँ सम (even) हैं")। गेटकीपर एक दूसरा AI है जो सुझावों को देखता है और कहता है, "नहीं, यह बकवास है," या "हाँ, यह सही लगता है।" यह कचरे को छानकर अलग कर देता है ताकि कारखाना समय बर्बाद न करे।द एडिटर (फॉर्मलाइज़र मॉड्यूल - संपादक):
भले ही कोई विचार गणितीय रूप से सही हो, AI इसे अजीब तरीके से लिख सकता है (जैसे खराब व्याकरण वाला वाक्य)। एडिटर सिंटैक्स (syntax) को ठीक करता है। यह कंप्यूटर (Lean server) से बात करता है कि क्या गलत है, त्रुटि संदेश प्राप्त करता है, और AI से इसे तब तक ठीक करने के लिए कहता है जब तक कि कंप्यूटर यह न कह दे, "ठीक है, यह वाक्य व्याकरणिक रूप से सही है।"द बिल्डर (प्रूवर मॉड्यूल - निर्माता):
अब जब तथ्य सही ढंग से लिख दिया गया है, तो बिल्डर इसे सिद्ध करने का प्रयास करता है। वह एक तार्किक तर्क बनाने का प्रयास करता है। यदि वह विफल होता है, तो उसे एक त्रुटि मिलती है, वह फिर से प्रयास करता है, और अपनी गलतियों को सुधारता है। यदि वह सफल होता है, तो वह एक सत्यापित प्रमाण (verified proof) बनाता है जिसे कंप्यूटर 100% सत्य के रूप में स्वीकार करता है।
उन्होंने क्या पाया
टीम ने इस कारखाने को चलाया और दो प्रमुख चीजें बनाईं:
- तथ्यों का एक नया पुस्तकालय: उन्होंने इन लापता "folklore" तथ्यों में से 1,506 को खोजा और सिद्ध किया। उन्होंने वास्तव में इनका एक छोटा नमूना लिया और उन्हें आधिकारिक Mathlib लाइब्रेरी में सफलतापूर्वक जोड़ा, जिससे यह सिद्ध हुआ कि AI ऐसे तथ्य उत्पन्न कर सकता है जो मानव विशेषज्ञों के उच्च मानकों को पूरा करते हैं।
- एक नई चुनौती (द बेंचमार्क): उन्होंने इन लापता तथ्यों के 4,028 का एक परीक्षण सेट बनाया ताकि यह देखा जा सके कि विभिन्न AI मॉडल इन तथ्यों को खोजने और सिद्ध करने में कितने अच्छे हैं।
परिणाम:
- वर्तमान AI मॉडल बेहतर हो रहे हैं, लेकिन वे अभी भी पूर्णता से दूर हैं। सर्वश्रेष्ठ मॉडल भी अकेले इन "स्पष्ट" तथ्यों में से केवल लगभग 19% को ही हल कर सके।
- हालाँकि, जब आप विभिन्न मॉडलों की शक्तियों को मिलाते हैं (जैसे विशेषज्ञों की एक टीम का उपयोग करना), तो वे लगभग 37% को हल कर सकते हैं।
- महत्वपूर्ण रूप से, जब मानव विशेषज्ञों ने उन मामलों को देखा जिन्हें AI हल नहीं कर सका, तो उन्होंने पाया कि उनमें से 78% वास्तव में हल करने योग्य और गणितीय रूप से सत्य थे। इसका मतलब है कि AI इसलिए विफल नहीं हुआ क्योंकि तथ्य फर्जी थे; यह इसलिए विफल हुआ क्योंकि कार्य वास्तव में कठिन था।
मुख्य निष्कर्ष (The Takeaway)
यह शोध पत्र दिखाता है कि हम AI का उपयोग केवल मौजूदा गणितीय पुस्तकालयों का उपभोग करने के लिए ही नहीं, बल्कि सक्रिय रूप से उन्हें विस्तारित करने के लिए भी कर सकते हैं। इन छोटे, लापता टुकड़ों की खोज और उन्हें स्वचालित करने के माध्यम से, हम औपचारिक गणित (formal mathematics) के लिए अधिक पूर्ण, उपयोगी और विश्वसनीय आधार बनाने में मदद कर रहे हैं। यह एक मानचित्र के अंतराल को भरने जैसा है ताकि एक गणितीय विचार से कंप्यूटर-सत्यापित प्रमाण तक की यात्रा सुगम और आसान हो सके।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।