एक 2 अक्टूबर के World Science Festival साक्षात्कार में, गणितज्ञ Tristan Buckmaster ने AI से बने एक परिणाम का वर्णन किया, जिसे वे सही मानते हैं लेकिन दूसरे गणितज्ञों के लिए पढ़ना कठिन है। उनका विवरण हालिया Navier–Stokes घोषणा के बाद एक अधिक विशिष्ट प्रश्न उठाता है: जब पढ़ने योग्य व्याख्या के लिए और काम चाहिए, तो शोध समुदाय औपचारिक तर्क की जाँच कैसे करे?

Buckmaster, Levent Alpöge के साथ अपने काम में चिकने बल वाले त्रि-आयामी Euler समीकरणों पर चर्चा कर रहे थे। उनका परिणाम 8 सितंबर के OpenAI दावे से अलग है, जो चिकने बल वाले Navier–Stokes समीकरणों के बारे में है। Navier–Stokes में श्यानता शामिल है; Euler में नहीं। OpenAI ने सीमित समय में विघटन के अपने दावे के लिए एक शोधपत्र और Lean औपचारिक रूप प्रकाशित किया। Millennium Prize का संचालन करने वाली संस्था ने कोई पुरस्कार घोषित नहीं किया।

बड़ा बदलाव

  • क्या बदला:Buckmaster ने अलग forced-Euler परिणाम स्थापित करने के लिए AI-निर्मित तर्कों और Lean के उपयोग का अपना अनुभव बताया है, साथ ही यह भी कि ऐसे प्रमाण गणितज्ञों को समझाने के लिए अभी कितना काम चाहिए।
  • यह क्यों महत्त्वपूर्ण है:औपचारिक जाँच यह स्थापित कर सकती है कि कूटबद्ध तर्क निर्दिष्ट परिभाषाओं और निर्भरताओं से निकलता है। गणितज्ञों को यह भी समझना होता है कि प्रमेय क्या कहता है, उसके विचार कैसे काम करते हैं और वह किनके पुराने काम पर आधारित है।
  • क्या देखना है:OpenAI के Navier–Stokes दावे का Clay द्वारा मूल्यांकन, प्रमाण के पढ़ने योग्य विवरण और लेखकीय श्रेय तथा पहुँच पर सार्वजनिक चर्चा दिखाएगी कि इस परिणाम का आकलन कैसे होता है। परिणाम पर Buckmaster का भरोसा विशेषज्ञ की राय है, पुरस्कार का निर्णय नहीं।

जाँचे गए तर्क को भी व्याख्या चाहिए

उस साक्षात्कार में, बक्मास्टर कहते हैं कि उनके Euler परिणाम के लिए AI द्वारा तैयार पहले प्रमाण में उपयोगी विचारों के साथ अप्रासंगिक गणनाएँ और कठिन गद्य मिला हुआ था। उनकी टीम ने पहले अलग-अलग चरणों की जाँच के लिए दूसरे एजेंटों का उपयोग किया, फिर औपचारिक जाँच के लिए तर्क को Lean में बदला। वे कहते हैं कि खराब प्रस्तुति के बावजूद प्राप्त प्रमाण सही था। यह विवरण उनके उनका Euler कार्य; इसे OpenAI के अलग Navier–Stokes शोधपत्र के हर हिस्से की उनकी स्वतंत्र पुष्टि नहीं समझना चाहिए।

व्यावहारिक अंतर यह है। Lean निर्दिष्ट प्रमाण-परिवेश में सटीक रूप से औपचारिक किए गए कथन की जाँच करता है। इससे लंबा तर्क अपने-आप उस शोधकर्ता के लिए पठनीय नहीं हो जाता जो उसकी विधि फिर इस्तेमाल करना चाहता है। Buckmaster ने Brian Greene को बताया कि अन्य AI प्रणालियाँ उन अंशों को समझ सकीं जिन्हें वे मुश्किल से पढ़ पाते थे, और AI से उन्हें सामान्य गणितीय भाषा में बदलने को कहना काम का हिस्सा बन गया। उन्होंने यह भी कहा कि प्रकाशित PDF पढ़ने में कठिन होने के बावजूद वे Navier–Stokes तर्क के विचार समझ सके। ये उनके आकलन हैं, BIG CHANGE द्वारा प्रमाण-जाँच नहीं; हमने Lean फ़ाइलें नहीं चलाईं और किसी प्रमेय की निर्णायक समीक्षा नहीं की।

NYU Courant की 14 सितंबर की रिपोर्ट Buckmaster और Alpöge की उपलब्धि को चिकने बल और सीमित-ऊर्जा प्रारंभिक आँकड़ों वाले forced 3D Euler में सीमित समय में नियमितता के ह्रास के रूप में बताती है। इसमें कहा गया है कि सहयोग के तीन शोधपत्र Lean में औपचारिक किए गए और परिणाम Diego Córdoba तथा Luis Martínez-Zoroa द्वारा शुरू की गई शोध-रणनीति का हिस्सा है। योगदान का श्रेय तय करते समय ये बातें महत्त्वपूर्ण हैं: मॉडल-निर्मित प्रमाण मौजूदा गणितीय राह को आगे बढ़ा सकता है, बिना उसे स्थापित करने वाले लोगों को मिटाए।

तेज़ी से आगे बढ़ती घटनाक्रम में दो परिणाम

OpenAI का कहना है कि उसकी आंतरिक एजेंट प्रणाली ने पहले बिना बाहरी बल वाला Euler परिणाम बनाया, फिर उसी काम की दिशा को अपने अलग Navier–Stokes निर्माण में इस्तेमाल किया। उसकी घोषणा Buckmaster और Alpöge के forced Euler परिणाम की प्राथमिकता स्वीकार करती है, साथ ही कहती है कि उसका प्रमाण स्वतंत्र रूप से विकसित हुआ। साक्षात्कार में Buckmaster गणितीय तंत्रों को संबंधित बताते हैं और कहते हैं कि श्यानता संभालने के लिए OpenAI ने सिकुड़ते भँवर का विचार जोड़ा। दोनों विवरण मानते हैं कि दावे अलग समीकरणों और प्रमाण-चरणों से जुड़े हैं; वे कालक्रम या बौद्धिक श्रेय के हर प्रश्न का निपटारा नहीं करते।

यूरोपीय गणितीय सोसाइटी ने घोषणा का स्वागत किया, साथ ही पहले के काम पर ज़ोर देते हुए लेखकीय श्रेय, योगदान और आंतरिक मॉडल तक पहुँच पर ध्यान देने की अपील की। 11 सितंबर की Clay प्रतिक्रिया में कहा गया कि Navier–Stokes समस्या प्रतीत होता है कि हल हो चुकी है और उपलब्धि का मूल्यांकन तथा श्रेय तय करने में जानबूझकर जल्दबाज़ी नहीं की जाएगी। Buckmaster ने Greene से कहा कि उन्हें विश्वास है कि OpenAI के पास समाधान है। दोनों बातें साथ सच हो सकती हैं: विशेषज्ञ का सकारात्मक आकलन और संस्था की जारी समीक्षा।

हाल में OpenAI की तीन अन्य गणितीय पांडुलिपियों को वापस लेना एक अलग घटना है। उनके द्वारा बताई गई चिह्न-संबंधी त्रुटि दावों की अलग-अलग जाँच करने का कारण है; यह इस बात का प्रमाण नहीं कि Navier–Stokes प्रमाण में भी वही त्रुटि है। BIG CHANGE की रिपॉज़िटरी-जाँच मार्गदर्शिका बताती है कि पांडुलिपि के संस्करण और प्रमाण-सामग्री कैसे खोजें; हमारी समीक्षा-क्षमता पर राय कहती है कि व्याख्या और जाँच के लिए समर्पित सहायता चाहिए। पहला Navier–Stokes लेख इस घटनाक्रम की शुरुआत दर्ज करता है। यह साक्षात्कार एक सक्रिय गणितज्ञ का विवरण जोड़ता है कि AI प्रणाली द्वारा तर्क बनाए जाने के बाद क्या होता है।

इतने महत्त्वपूर्ण दावे के लिए अगली उपयोगी प्रकाशित सामग्री सटीक, पढ़ने योग्य विवरण, जाँचे जा सकने वाले औपचारिक साक्ष्य और स्वतंत्र गणितीय प्रतिक्रियाएँ होंगी। हर चीज़ की भूमिका अलग है। प्रमाण का उम्मीदवार बनाने की गति इन कामों को और ज़रूरी करती है, जबकि Clay की घोषित प्रक्रिया उन्हें सावधानी से पूरा करने की गुंजाइश देती है।

स्रोत और आगे पढ़ें