हाल की गणितीय दुनिया में एक चौंकाने वाली खबर में, तियुन्हुआ विश्वविद्यालय के पूर्व छात्रों के एक समूह ने AI की मदद से 162 ऐसे गणितीय प्रमेयों को सफलतापूर्वक साबित किया है, जिन्हें पहले कोई हल नहीं कर सका। इससे भी अधिक आश्चर्यजनक बात यह है कि इस बुद्धिमान एजेंट का नाम LeanAgent है, जिसने ताओ झेएक्सियान द्वारा बहुपद फ्रेमैन-रुज़्सा अनुमान के औपचारिक चुनौती को भी पार कर लिया! यह हमें यह सोचने पर मजबूर करता है कि बुनियादी विज्ञान के शोध के तरीके AI द्वारा पूरी तरह से बदल दिए गए हैं।
जैसा कि हम जानते हैं, वर्तमान भाषा मॉडल (LLM) हालांकि प्रभावशाली हैं, लेकिन अधिकांश अभी भी स्थिर हैं और नए ज्ञान को ऑनलाइन सीखने में असमर्थ हैं, उच्च गणितीय प्रमेयों को साबित करना तो और भी कठिन है। हालाँकि, कैलटेक, स्टैनफोर्ड विश्वविद्यालय और वाशिंगटन विश्वविद्यालय की शोध टीम द्वारा संयुक्त रूप से विकसित LeanAgent, एक ऐसा AI सहायक है जिसमें जीवनभर सीखने की क्षमता है, जो लगातार सीखने और प्रमेयों को साबित करने में सक्षम है।
LeanAgent विभिन्न गणितीय कठिनाइयों का सामना करने के लिए सावधानीपूर्वक डिज़ाइन किए गए अध्ययन पथ का उपयोग करता है, गतिशील डेटाबेस का प्रबंधन करके निरंतर गणितीय ज्ञान को सुनिश्चित करता है, ताकि जब वह नया ज्ञान सीखता है, तो वह पहले से सीखी गई क्षमताओं को न भूले। प्रयोगों से पता चला है कि इसने 23 विभिन्न Lean कोड रिपॉजिटरी से 162 पहले असंभव गणितीय प्रमेयों को साबित किया है, और इसका प्रदर्शन पारंपरिक बड़े मॉडल की तुलना में 11 गुना अधिक है, जो वास्तव में आश्चर्यजनक है!
ये प्रमेय उच्च गणित के कई क्षेत्रों को कवर करते हैं, जिनमें अमूर्त बीजगणित और बीजगणितीयTopology जैसे कठिन प्रश्न शामिल हैं। LeanAgent न केवल सरल अवधारणाओं से शुरू कर सकता है, बल्कि धीरे-धीरे जटिल विषयों पर विजय प्राप्त कर सकता है, बल्कि स्थिरता और विपरीत स्थानांतरण में भी उत्कृष्ट प्रदर्शन प्रदर्शित करता है।
हालांकि, ताओ झेएक्सियान की चुनौती अभी भी AI के लिए निराशाजनक है। हालांकि इंटरएक्टिव प्रमेय प्रमाणक (ITPs) जैसे Lean, गणितीय प्रमाणों को औपचारिक और सत्यापित करने में महत्वपूर्ण भूमिका निभाते हैं, लेकिन ऐसे प्रमाण प्रक्रिया का निर्माण अक्सर जटिल और समय लेने वाला होता है, जिसमें विस्तृत कदम और बड़ी मात्रा में गणितीय कोड रिपॉजिटरी की आवश्यकता होती है। जैसे o1 और Claude जैसे उन्नत बड़े मॉडल गैर-औपचारिक प्रमाणों का सामना करते समय भी गलतियाँ कर सकते हैं, जो गणितीय प्रमाणों की सटीकता और विश्वसनीयता में LLM की कमी को उजागर करता है।
अतीत के शोध ने LLM का उपयोग करके पूर्ण प्रमाण चरण उत्पन्न करने का प्रयास किया, जैसे LeanDojo, जो विशेष डेटा सेट पर बड़े मॉडल को प्रशिक्षित करके एक प्रमेय प्रमाणक बनाने के लिए विकसित किया गया था। हालाँकि, औपचारिक प्रमेय प्रमाण के लिए डेटा अत्यंत दुर्लभ है, जो इस विधि के व्यापक उपयोग को सीमित करता है। एक अन्य परियोजना ReProver, Lean प्रमेय प्रमाण कोड रिपॉजिटरी mathlib4 के लिए अनुकूलित मॉडल है, हालांकि यह 100,000 से अधिक औपचारिक गणितीय प्रमेयों और परिभाषाओं को कवर करता है, लेकिन यह केवल अंडरग्रेजुएट गणित की सीमा तक सीमित है, इसलिए जब अधिक जटिल प्रश्नों का सामना करना पड़ता है, तो इसका प्रदर्शन खराब होता है।
यह ध्यान देने योग्य है कि गणितीय अनुसंधान की गतिशीलता AI के लिए एक बड़ा चुनौती प्रस्तुत करती है। गणितज्ञ अक्सर एक साथ या बारी-बारी से कई परियोजनाओं पर काम करते हैं, जैसे कि ताओ झेएक्सियान कई शोध क्षेत्रों को एक साथ आगे बढ़ाते हैं, जिसमें PFR अनुमान और वास्तविक संख्या के सममित औसत शामिल हैं। ये उदाहरण वर्तमान AI प्रमेय प्रमाण विधियों की एक महत्वपूर्ण कमी को दर्शाते हैं: एक ऐसा AI सिस्टम की कमी जो विभिन्न गणितीय क्षेत्रों में स्व-adaptive सीखने और सुधारने में सक्षम हो, विशेष रूप से जब Lean डेटा सीमित हो।
इसीलिए, LeanDojo की टीम ने LeanAgent का निर्माण किया, जो एक नई जीवनभर सीखने की रूपरेखा है, जिसका उद्देश्य उपरोक्त चुनौतियों का समाधान करना है। LeanAgent का कार्यप्रवाह प्रमेय की जटिलता को व्युत्पन्न करने, अध्ययन पाठ्यक्रम तैयार करने, अध्ययन प्रक्रिया में स्थिरता और लचीलापन को संतुलित करने के लिए क्रमिक प्रशिक्षण के माध्यम से, और बिना प्रमाणित प्रमेयों की खोज के लिए सर्वोत्तम प्राथमिकता पेड़ खोज का उपयोग करता है।
LeanAgent का किसी भी बड़े मॉडल के साथ संयोजन में उपयोग करके इसकी सामान्यीकरण क्षमता को बढ़ाने के लिए “रिक्ति” का उपयोग करता है। इसका नवाचार यह है कि यह निरंतर विस्तारशील गणितीय ज्ञान का प्रबंधन करने के लिए एक अनुकूलित गतिशील डेटाबेस का उपयोग करता है, और Lean प्रमाण संरचना पर आधारित पाठ्यक्रम सीखने की रणनीति का उपयोग करता है, जो अधिक जटिल गणितीय सामग्री को सीखने में सहायता करता है।
AI के विनाशकारी भूलने की समस्या का सामना करने के लिए, शोधकर्ताओं ने एक क्रमिक प्रशिक्षण विधि का उपयोग किया, जिससे LeanAgent नए गणितीय ज्ञान के अनुकूलन में सक्षम हो सके, जबकि पहले के अध्ययन को न भूलें। यह प्रक्रिया प्रत्येक नए डेटा सेट पर वृद्धि प्रशिक्षण में शामिल होती है, जो स्थिरता और लचीलापन के सर्वोत्तम संतुलन को सुनिश्चित करती है।
इस क्रमिक प्रशिक्षण के माध्यम से, LeanAgent प्रमेयों को साबित करने में उत्कृष्ट प्रदर्शन करता है, सफलतापूर्वक 162 ऐसे कठिन प्रश्नों को साबित किया है, जो पहले मानव द्वारा हल नहीं किए गए थे, विशेष रूप से अमूर्त बीजगणित और बीजगणितीयTopology के चुनौतीपूर्ण प्रमेयों पर अपना कौशल दिखाया है। नए प्रमेयों को साबित करने की क्षमता में, यह स्थिर ReProver की तुलना में 11 गुना अधिक है, और ज्ञात प्रमेयों को साबित करने की क्षमता को बनाए रखता है।
LeanAgent प्रमेय प्रमाणन के दौरान क्रमिक सीखने के लक्षण प्रदर्शित करता है, सरल प्रमेयों से धीरे-धीरे अधिक जटिल प्रमेयों की ओर बढ़ता है, जिससे यह गणितीय ज्ञान में गहराई का प्रमाण देता है। उदाहरण के लिए, इसने समूह सिद्धांत और रिंग सिद्धांत से संबंधित बुनियादी बीजगणित संरचना के प्रमेय को साबित किया, जो गणित की गहरी समझ को दर्शाता है। कुल मिलाकर, LeanAgent अपनी शक्तिशाली निरंतर सीखने और सुधारने की क्षमता के साथ गणितीय समुदाय में रोमांचक संभावनाएँ लेकर आया है!
पेपर का पता: https://arxiv.org/pdf/2410.06209
