शोधपत्र क्या दावा करता है
गूगल डीपमाइंड की एक टीम ने ऐसे एआई तंत्र का सहकर्मी-समीक्षित विवरण प्रकाशित किया है जो गणितीय प्रमाण खोजता है और साथ-साथ उन्हें मशीन से जँचवाता है। यह शोधपत्र, त्सूकालास और सहयोगियों का “Advancing Mathematics Research with AI-Driven Formal Proof Search”, 8 अक्टूबर को साइंस में छपा।
तंत्र, अल्फ़ाप्रूफ़ नेक्सस, जेमिनाई 3.1 प्रो के इर्द-गिर्द बना है। यह लीन में प्रमाण लिखता है — वह औपचारिक भाषा जिसमें हर तार्किक क़दम सॉफ़्टवेयर से जाँचा जाता है — और जाँचकर्ता के त्रुटि संदेश अगला मसौदा तय करते हैं। कठिन उप-समस्याओं के लिए यह डीपमाइंड के विशेष औज़ार अल्फ़ाप्रूफ़ को काम सौंप सकता है।
शोधकर्ताओं ने एर्दोश संग्रह से 353 खुली समस्याएँ चुनीं और उन्हें लीन में लिखा। तंत्र ने उनमें से नौ हल कीं — लगभग 2.5% — जिनमें दो 56 साल से अनसुलझी थीं। इसने पूर्णांक अनुक्रमों के ऑनलाइन विश्वकोश की 44 परिकल्पनाएँ भी सिद्ध कीं, बीजीय ज्यामिति का एक खुला प्रश्न सुलझाया और मिन-मैक्स अनुकूलन की एक ज्ञात सीमा सुधारी, जो कुछ एआई मॉडलों के प्रशिक्षण में काम आती है।
दिलचस्प हिस्सा अब्लेशन है
डीपमाइंड बताती है कि तंत्र ने वही नौ एर्दोश समस्याएँ अल्फ़ाप्रूफ़ के बिना भी हल कीं। एक अब्लेशन विश्लेषण में पाया गया कि एक सरल व्यवस्था, जिसे शोधपत्र एजेंट ए कहता है, उन्हीं नौ तक पहुँची — यह बात कातालोनिया के मुक्त विश्वविद्यालय के जोसेप कुर्तो ने साइंस मीडिया सेंटर स्पेन द्वारा जुटाई गई विशेषज्ञ टिप्पणियों में उठाई। कुर्तो इसे अति-अभियांत्रिकी का संकेत मानते हैं और कहते हैं कि शोधपत्र में पद्धतिगत असंगतियाँ हैं।
उनकी अधिक पैनी बात यह है कि औपचारिक सत्यापन क्या देता है और क्या नहीं। वे कहते हैं कि लीन इस बात की गारंटी देता है कि प्रमाण तार्किक रूप से वैध है। यह गारंटी नहीं देता कि जो कथन किसी ने औपचारिक रूप में लिखा वही वह समस्या है जो वह कहना चाहता था। अनौपचारिक परिकल्पना को लीन में बदलना अब भी मनुष्य का क़दम है, और वहाँ की ग़लती जाँचकर्ता से बचकर निकल जाती है।
353 में से नौ को कैसे पढ़ें
हर अंश के नीचे का हर मायने रखता है। ये नौ सफलताएँ उस निश्चित समुच्चय में से हैं जिसे टीम ने ख़ुद चुना और औपचारिक रूप दिया, न कि प्रसिद्ध परिकल्पनाओं को गिराने की कोई सामान्य क्षमता। मैड्रिड के स्वायत्त विश्वविद्यालय के पाब्लो आया कोल्ल उन्हीं टिप्पणियों में गिनती के बजाय पद्धति की ओर इशारा करते हैं: मूल्य गणितीय खोजें उपजाने के दोहराए जा सकने वाले तरीक़े में है, उन नौ में नहीं।
स्पेन के गणितीय विज्ञान संस्थान के निदेशक ख़ावियर अरामायोना वह समस्या उठाते हैं जो मशीन-जाँचे प्रमाणों के पढ़े जाने से तेज़ आने पर पैदा होती है: एआई से बने कई परिणाम सत्यापित हैं और फिर भी पूरी तरह समझे नहीं गए। वायादोलिद विश्वविद्यालय के तेओदोरो कालोंखे ने इसे उच्च गुणवत्ता का शोधपत्र और एक शुरुआती प्रयास कहा, जिसमें सुधार की काफ़ी गुंजाइश है।
दूसरी प्रयोगशाला से तुलना
इस काम ने जो रास्ता लिया वही कहानी का हिस्सा है। डीपमाइंड ने शोधपत्र छपने से पहले एर्दोश के हल सार्वजनिक किए और फिर काम को सहकर्मी समीक्षा से गुज़ारा। ओपनएआई ने दूसरा रास्ता चुना और सैकड़ों एआई-जनित प्रमाण एक भंडार पर डाल दिए, जिसके बाद इसी महीने गणितज्ञों के एक समूह ने कंपनी के बहिष्कार की माँग की।
ध्यान इस पर रहे कि लीन फ़ाइलें बाहरी जाँच में टिकती हैं या नहीं, और नौ में से कोई औपचारिक कथन उस एर्दोश समस्या से अलग कुछ कहता निकलता है या नहीं जिसका नाम उस पर लगा है। यह जाँच अब किसी के लिए भी उपलब्ध है, और यही डीपमाइंड के चुने रास्ते के पक्ष में व्यावहारिक तर्क है।
