ऐक्सिओम मैथ ने गणित में एआई की गलतियों को रोकने के लिए उठाया बड़ा कदम

कोलंबिया विश्वविद्यालय के ही जोहान डी जोंग ने साल 2005 में इस स्टैक्स प्रोजेक्ट की शुरुआत एक ओपन सोर्स संदर्भ के रूप में की थी। तब से लेकर अब तक दुनिया भर के गणितज्ञ इसमें लगातार अपना योगदान देते आ रहे हैं, जिसमें कॉलेज स्तर के बीजगणित से लेकर बीजगणितीय ज्यामिति और संख्या सिद्धांत तक के उन्नत विचार शामिल हैं। कंपनी के एआई एजेंटों के बेड़े ने इस विशाल पुस्तकालय के लगभग 7,654 पृष्ठों का अनुवाद करके कंप्यूटर द्वारा जांची गई लगभग 1.6 करोड़ लाइनों के कोड में बदल दिया है।

औपचारिक सत्यापन और कोड की प्रक्रिया

गणित को औपचारिक रूप देने का मुख्य उद्देश्य यह सुनिश्चित करना होता है कि उसके नीचे की संरचना पूरी तरह से ठोस है या नहीं। इस प्रक्रिया में गणितज्ञ किसी प्रमाण को लीन नामक प्रोग्रामिंग भाषा में कोड के रूप में लिखते हैं और फिर प्रूफ असिस्टेंट नामक एक विशेष कार्यक्रम इस कोड की एक-एक पंक्ति की जांच करता है। यदि यह प्रमाण इस जांच में खरा उतरता है, तो गणितज्ञ यह मान सकते हैं कि वह तार्किक रूप से पूरी तरह सही है।

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

आपसी जुड़ाव और विशाल जटिलता

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

मार्च 2025 में इस स्टार्टअप की स्थापना करने वाली 25 वर्षीय सीईओ करीना हाँग ने स्टैनफोर्ड विश्वविद्यालय के गणित पीएचडी कार्यक्रम को बीच में ही छोड़ दिया था। इसी साल मार्च में कंपनी ने मेनलो वेंचर्स के नेतृत्व में 20 करोड़ डॉलर का सीरीज ए फंड जुटाया था। करीना हाँग के अनुसार, शुरुआत में टीम को यह भी पूरी तरह स्पष्ट नहीं था कि वाइब कोडिंग इस विशाल परियोजना की सुंदरता और शुद्धता को सहेज पाएगी या नहीं।

समानांतर एजेंट और इन-हाउस मॉडल

इस चुनौती से पार पाने के लिए तकनीकी टीम ने अपने एआई एजेंटों को एक लचीली संरचना सौंपी और उन्हें समानांतर रूप से काम करने की छूट दी। ऐक्सिओम के तकनीकी स्टाफ के सदस्य अश्निन स्वामीनाथन ने बताया कि स्टैक्स के मामले में उन्होंने एक पदानुक्रम जरूर तय किया था, लेकिन वह ऐसा सख्त ढांचा नहीं था जो हर एक एजेंट के हर कदम को निर्देशित कर रहा हो, बल्कि एजेंट खुद अपने लिए कार्य ढूंढ रहे थे और ऐसे क्षेत्रों की पहचान कर रहे थे जिन पर वे एक साथ मिलकर काम कर सकें।

इसके अलावा कंपनी ने अपने खुद के ऐसे मॉडल भी प्रशिक्षित किए जो गणित में माहिर हों, जिसे करीना हाँग ने एक ऐसा दृष्टिकोण बताया जिसे अन्य सत्यापन स्टार्टअप्स ने नहीं अपनाया है। शुरुआत में टीम ने एजेंटों को इंसानों जैसी समझ और परख सिखाने के लिए अपने ही एक लीन विशेषज्ञ की मदद ली, लेकिन समय के साथ एजेंटों ने खुद ही इस खूबी को आत्मसात कर लिया।

बीजगणितीय ज्यामिति का नया द्वार

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

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

भविष्य की सॉफ्टवेयर सुरक्षा और खुली चुनौती

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

अश्निन स्वामीनाथन ने कहा कि उनका विश्वास है कि गणित वह क्षेत्र है जहां से इन चीजों का निर्माण शुरू किया जाना चाहिए और यह एक ऐसी कौशल है जिसे अन्य क्षेत्रों में भी स्थानांतरित किया जा सकता है। करीना हाँग इस दृष्टिकोण को लेकर इतनी आश्वस्त हैं कि उन्होंने खुले तौर पर अन्य सभी कोडिंग कंपनियों को इस पैमाने पर औपचारिक सत्यापन के क्षेत्र में काम करने की चुनौती दी है।