LongTails AI एजेंट ने ऑप्टिमाइज़ेशन की 30 से ज़्यादा नई प्रमेयें सिद्ध कीं

Lean 4 से हर प्रमाण की जाँच

सिस्टम की मुख्य खूबी यह है कि वह हर प्रमाण को औपचारिक सत्यापन भाषा Lean 4 से अपने आप जाँचता है। AI को गणित में इस्तेमाल करने की एक जानी-पहचानी समस्या यह है कि मॉडल ऐसा तर्क दे सकता है जो देखने में ठोस लगे, पर उसमें गलती हो या वह किसी और समस्या को हल कर रहा हो। LongTails शर्तों और लक्ष्य के औपचारिक विवरण से शुरू करता है और जाँचता है कि प्रमाण उनसे मेल खाता है या नहीं।

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

क्यों मायने रखता है

ऑप्टिमाइज़ेशन का मतलब बहुत से विकल्पों में से सबसे अच्छा चुनना है, चाहे लक्ष्य सबसे तेज़ तरीका हो, सबसे कम लागत हो या सबसे अधिक सटीकता। सिद्ध प्रमेयें बताती हैं कि कोई विधि कितनी तेज़ चलेगी और किन शर्तों में काम करेगी। इससे जरूरी गणनाओं का अनुमान पहले से लगाया जा सकता है। सिफ़ारिश सिस्टम से लेकर बड़े भाषा मॉडल तक की ट्रेनिंग ऐसे ही तरीकों पर टिकी है, इसलिए ज़्यादा कुशल एल्गोरिदम से ट्रेनिंग का समय, कंप्यूटिंग लागत और डेटा सेंटर की ऊर्जा खपत घट सकती है। इनका उपयोग डिलीवरी रूट की योजना, पावर ग्रिड के लोड वितरण, नए अणुओं और सामग्रियों की खोज और निवेश जोखिम प्रबंधन में भी हो सकता है।

LongTails का कोड सार्वजनिक है, ताकि दूसरे शोध समूह भी इसका उपयोग कर सकें। परियोजना के एक प्रतिभागी के मुताबिक, फ़्रेमवर्क ने कुछ ही दिनों में वह हासिल कर लिया जो उन्होंने अपने पूरे करियर में किया था। टीम आगे और प्रमेयें सिद्ध करेगी, समस्याओं की जटिलता बढ़ाएगी और मिले एल्गोरिदम को व्यावहारिक अनुप्रयोगों में परखेगी।