इस महीने की शुरुआत में एक कृत्रिम बुद्धिमत्ता (एआई) स्टार्टअप ने घोषणा की थी कि उनके एआई एजेंट ने शैतानी रूप से चुनौतीपूर्ण “उच्च आयामी क्षेत्र-पैकिंग समस्या” के दो मामलों के प्रमाण की पुष्टि की है। 2022 में, सबूत यूक्रेनी गणितज्ञ अर्जित किया मैरीना वियाज़ोव्स्का ए फील्ड्स मेडलगणित में सबसे प्रतिष्ठित पुरस्कारों में से एक।
यह एक बड़ा कदम था और इस क्षेत्र में एक शांत क्रांति के उद्भव का संकेत देता है।
सतह पर, यह इतना असाधारण नहीं लग सकता है। आख़िरकार, गणितज्ञों ने लंबे समय से अपनी क्षमताओं को बढ़ाने के लिए उपकरणों का उपयोग किया है – अबेकस, स्लाइड नियम, कैलकुलेटर और, अंततः, कंप्यूटर। फिर भी इनमें से किसी भी उपकरण ने कभी भी गणितज्ञों की जगह नहीं ली; उन्होंने हमें और अधिक दिलचस्प समस्याओं पर अपना ध्यान केंद्रित करने की अनुमति दी। गणित में एआई का आगमन उसी प्रक्रिया में एक और कदम की तरह लग सकता है। लेकिन एक महत्वपूर्ण अंतर है: इस बार, उपकरण हमें केवल गणना करने में मदद नहीं कर रहे हैं; वे हमें तर्क करने में मदद कर रहे हैं, या कम से कम कई कार्य करने में मदद कर रहे हैं। दिनचर्या जो मानवीय तर्क के अंतर्गत आती है।
लेख नीचे जारी है
किट येट्स यूके में बाथ विश्वविद्यालय में गणितीय जीव विज्ञान और सार्वजनिक सहभागिता के प्रोफेसर हैं
परिवर्तन कुछ समय से आ रहा है। वर्षों से, हमारा सबसे बड़ा प्रमाण एकल गणितज्ञों के प्रयास नहीं रहे हैं। शुद्ध गणित में कई आधुनिक शोध लेख अब विशाल वैचारिक ढांचे, लंबी निर्भरता श्रृंखला और परिणामों की सूची पर निर्भर करते हैं जिन्हें कोई भी व्यक्ति पूरी तरह से आत्मसात नहीं कर सकता है। कंप्यूटर ने पहले भी बड़े प्रमाणों में भूमिका निभाई है चार रंग प्रमेय और यह केप्लर अनुमान. लेकिन अब जो बदल रहा है वह स्वायत्तता और विश्वसनीयता का स्तर है जिसे हम औपचारिक प्रमाण सहायकों के साथ काम करने वाले एआई सिस्टम से उम्मीद कर सकते हैं – गणितीय तर्कों की जांच करने के लिए डिज़ाइन किए गए प्रोग्राम।
लेकिन हाल तक, अत्याधुनिक सबूतों को मशीन से जांचने योग्य रूप में बदलने के लिए विशेषज्ञों को काम के लिए महीनों या वर्षों का समय देना पड़ता था।
ये औपचारिक सत्यापन भाषाएँ गणितीय तर्कों को इस तरह व्यक्त करती हैं कि कंप्यूटर चरण दर चरण जाँच कर सकता है, यह गारंटी देते हुए कि प्रमाण का प्रत्येक भाग तार्किक रूप से सही है। भाषा ले लो दुबलाउदाहरण के लिए। सामान्य गणितीय लेखन के विपरीत, लीन को प्रत्येक परिभाषा और अनुमान को स्पष्ट करने की आवश्यकता होती है, और यह प्रत्येक चरण को यंत्रवत् और व्यवस्थित रूप से जांचता है। यह अक्षम्य है, लेकिन उत्पादक तरीके से: यदि तर्क लीन द्वारा पारित किया जाता है, तो, सिद्धांत रूप में, इसका मतलब है कि सबूत में छिपी हुई धारणाएं या विश्वास की छलांग नहीं है। पिछले कुछ वर्षों में, लीन अनुसंधान स्तर के गणित के लिए एक सिद्ध आधार बन गया है, और गणितज्ञ तेजी से जटिल समस्याओं का समर्थन करने के लिए “पुस्तकालय” का निर्माण कर रहे हैं।
ये पुस्तकालय परिभाषाओं और पहले से ही सत्यापित प्रमेयों का विशाल संग्रह हैं जिन्हें बड़ी मेहनत से प्रोग्राम किया गया है, जिससे शोधकर्ताओं को भाषा में नए परिणाम साबित करने की अनुमति मिलती है। लेकिन हाल तक, अत्याधुनिक सबूतों को मशीन से जांचने योग्य रूप में बदलने के लिए विशेषज्ञों को काम के लिए महीनों या वर्षों का समय देना पड़ता था।
यही वह संदर्भ है जिसमें वियाज़ोव्स्का के उच्च-आयामी क्षेत्र-पैकिंग परिणामों के हालिया औपचारिक सत्यापन को समझा जाना चाहिए। स्फीयर-पैकिंग समस्या पूछती है कि किसी भी आयाम के स्थानों में समान क्षेत्रों को एक साथ कितनी मजबूती से पैक किया जा सकता है, न कि केवल 3डी दुनिया जिसमें हम रहते हैं। वियाज़ोव्स्का की सफलता से पहले, स्फीयर-पैकिंग समस्या केवल आयाम एक, दो और तीन में पूरी तरह से हल हो गई थी, सभी उच्च-आयामी मामले खुले रह गए थे। वियाज़ोव्स्का के सबूत आठ- और 24-आयामी क्षेत्र-पैकिंग समस्यागणितीय अंतर्दृष्टि के गहन टुकड़े हैं जो उन समस्याओं को हल करते हैं जिन्हें पहले पहुंच से बाहर माना जाता था।
फील्ड्स मेडल-स्तर की प्रगति
हालिया महत्वपूर्ण कदम यह है कि मानव-एआई सहयोग ने अब उन तर्कों को पूरी तरह से सत्यापित लीन कोड में अनुवादित किया है, जो तब हर चरण की जांच करता है। उस उपलब्धि का पैमाना आश्चर्यजनक है; ये हालिया फील्ड्स मेडल स्तर के परिणाम हैं, और अब इन्हें विस्तार और निश्चितता के स्तर पर प्रमाणित किया गया है, जिसे बिना सहायता के पुन: प्रस्तुत करना व्यक्तिगत रेफरी, या यहां तक कि बड़ी मानव विशेषज्ञ टीमों के लिए असंभव होगा।
एक प्रमुख घटक था गणित, इंक.के एआई रीजनिंग एजेंट गॉस ने मानव गणितीय तर्कों को लीन प्रमाणों में बदलने में मदद करने में महत्वपूर्ण भूमिका निभाई थी। एआई प्रणाली पूरी तरह से बिना सहायता के काम नहीं कर रही थी; गणितज्ञों को अभी भी खाका तैयार करना था, समग्र संरचना को आकार देना था और यह सुनिश्चित करना था कि सही अवधारणाएँ मौजूद हों। लेकिन एक बार जब वह मचान अस्तित्व में आ गया, तो सिस्टम असाधारण गति से लापता टुकड़ों को भर सकता था। आठ-आयामी मामले में, इसने वह काम पूरा किया जिसके बारे में मानव योगदानकर्ताओं ने अनुमान लगाया था कि इसमें उन्हें महीनों लगेंगे, और इसने ऐसा कुछ दिनों में पूरा किया।. 24-आयामी मामला, जो और भी जटिल है, इसके तुरंत बाद आया।
स्फीयर-पैकिंग प्रोजेक्ट संभवतः जो संभव हो रहा है उसका अब तक का सबसे स्पष्ट प्रदर्शन है।
यह एक तकनीकी उपलब्धि से कहीं अधिक है. यह गणितज्ञों द्वारा अपने काम को व्यवस्थित करने के तरीके में बदलाव की ओर इशारा करता है। जब मैंने यूसीएलए के गणितज्ञ और फील्ड्स मेडलिस्ट से बात की टेरेंस ताओउन्होंने सुझाव दिया कि एआई का तात्कालिक मूल्य हमारी सबसे कठिन समस्याओं को सीधे हल करने से नहीं बल्कि हमें कठिन परिश्रम से राहत दिलाने से हो सकता है – हजारों छोटे मामले जो वैचारिक रूप से सीधे हैं लेकिन किसी एक व्यक्ति द्वारा हाथ से निपटने के लिए बहुत समय लेने वाला है।
उन्होंने तर्क दिया कि कुछ एआई सिस्टम पहले से ही इन कार्यों को संभालने में आश्चर्यजनक रूप से अच्छे हैं, जिससे गणितज्ञों को अपना ध्यान बहीखाता के बजाय रणनीति पर केंद्रित करने में मदद मिलती है। लीन जैसे उपकरण मायने रखते हैं क्योंकि वे हमें विचारों को उत्पन्न करने की रचनात्मकता को उनकी जांच करने की कठोरता से अलग करने का एक तरीका देते हैं।
एआई प्रमाण विशेषज्ञ केविन बज़र्डइंपीरियल कॉलेज लंदन के , ने एक पूरक विचार व्यक्त किया। वह सही रूप से, बड़े भाषा मॉडलों पर भरोसा करने के खतरों के बारे में चिंतित हैं जो शुद्धता की गारंटी के बिना आधिकारिक लगते हैं। लेकिन उनका यह भी तर्क है कि औपचारिकीकरण इसके माध्यम से एक रास्ता प्रदान करता है. लीन में, यदि प्रोग्राम सभी चरणों को स्वीकार करता है, तो यह एक वैध प्रमाण है। इसका मतलब यह नहीं है कि कंप्यूटर ने आवश्यक रूप से कुछ “बुद्धिमान” कार्य किया है, बल्कि यह है कि औपचारिक सत्यापन भाषा छिपे हुए कदमों या विचारोत्तेजक-लेकिन-अधूरे तर्कों के लिए कोई जगह नहीं छोड़ती है। चुनौती, जैसा कि वह देखते हैं, यह है कि अधिकांश आधुनिक गणित का अभी भी औपचारिक पुस्तकालयों में अनुवाद नहीं किया गया है, इसलिए सिस्टम में अभी तक वे अवधारणाएँ नहीं हैं जिनकी उन्हें आवश्यकता है।
इस नवीनतम कदम से पता चलता है कि अंतर कम होने लगा है। स्फीयर-पैकिंग प्रोजेक्ट संभवतः जो संभव हो रहा है उसका अब तक का सबसे स्पष्ट प्रदर्शन है।
इसका कोई मतलब नहीं है कि गणितज्ञ विलुप्त होने के कगार पर हैं। वास्तव में, मुझे संदेह है कि विपरीत सत्य है। जैसे-जैसे सत्यापन योग्य गणित का दायरा बढ़ता जा रहा है, वैसे-वैसे ऐसे लोगों की आवश्यकता भी बढ़ रही है जो अच्छे प्रश्न पूछ सकें, नई परिभाषाएँ बना सकें और पहचान सकें कि कोई तर्क वास्तव में व्यावहारिक है या नहीं। लेकिन हमें अनुकूलन करना होगा। हम खुद को वैज्ञानिक-यंत्र निर्माताओं की तरह अधिक और अकेले सिद्धांतकारों की तरह कम, मशीन-सत्यापित निश्चितता उत्पन्न करने के लिए मानवीय अंतर्ज्ञान और एआई दृढ़ता को एक साथ बुनते हुए पा सकते हैं।
गणित हमेशा सहायक उपकरणों के साथ साझेदारी करके आगे बढ़ा है। एआई उस प्रथा को नहीं बदलता है; यह इसे अगले स्तर पर ले जाता है। गणितीय अवधारणाओं को सिद्ध करना आसान नहीं होगा, लेकिन उन्हें परखने, सत्यापित करने और उन पर निर्माण करने की हमारी क्षमता निश्चित रूप से बढ़ जाएगी।
राय लाइव साइंस पर आपको विज्ञान के सबसे महत्वपूर्ण मुद्दों पर जानकारी मिलती है जो आज आपको और आपके आसपास की दुनिया को प्रभावित करते हैं, जो अपने क्षेत्र के विशेषज्ञों और अग्रणी वैज्ञानिकों द्वारा लिखा गया है।
