लगता है कि कृत्रिम बुद्धिमत्ता लगभग हर हफ्ते एक नया गणितीय समस्या हल कर रही है। पिछले महीने, केवल OpenAI ने ही 719 हस्तलिखित प्रतिलिपियाँ जारी कीं, जिनमें इस क्षेत्र की कुछ सबसे कठिन समस्याओं को हल करने का दावा किया गया। यहां तक कि कंप्यूटर जांच में भी गलतियां हो सकती हैं। कई वर्षों तक AI द्वारा उत्पादित अवांछित सामग्री के बाद, लोग पूछने लगे हैं कि क्या गणित अगला प्रभावित क्षेत्र बन जाएगा।
AxiomMath का अनुमान गणित के माध्यम से इस भाग्य से बचना है, जिसके लिए यह धीमा नहीं हो रहा, बल्कि एक मजबूत आधार बना रहा है। इस 16 अरब डॉलर की मूल्यांकित स्टार्टअप का लक्ष्य एक सत्यापित आधार परत बनाना है, जिस पर AI एजेंट सॉफ्टवेयर लिखने और अंततः वैज्ञानिक शोध करने के लिए निर्भर कर सकें।
बुधवार को, कंपनी ने घोषणा की कि उसने स्टैक्स प्रोजेक्ट की औपचारिक वैलिडेशन पूरी कर ली है, जो मानव द्वारा लिखे गए सबसे बड़े गणितीय उपलब्धियों में से एक है। गणितज्ञ आमतौर पर स्टैक्स की बहुत उच्च प्रशंसा करते हैं। कोलंबिया विश्वविद्यालय के गणितज्ञ पीटर वॉइट ने इसे "इसकी तुलना में लगभग कुछ भी नहीं है" कहा और इस प्रोजेक्ट की तुलना "प्रसिद्ध बुरबाकी सीरीज" से की, जो 20वीं सदी में गणित को मूल से पुनः स्थापित करने वाली श्रृंखला थी।
वॉइट के कोलंबिया के सहकर्मी जोहन डी योंग ने 2005 में स्टैक्स प्रोजेक्ट को एक ओपन सोर्स संदर्भ के रूप में शुरू किया। उसके बाद से, गणितज्ञों ने इसमें योगदान दिया है, जिसमें विश्वविद्यालय स्तरीय बीजगणित से लेकर बीजगणित, ज्यामिति और संख्या सिद्धांत के क्षेत्रों में सबसे अग्रणी विचारों तक का विस्तार हुआ है।
कंपनी के AI एजेंट समूह ने इस लगभग 7,654 पृष्ठों के डेटाबेस को लगभग 16 मिलियन पंक्तियों के कंप्यूटर-जांचने योग्य कोड में अनुवादित किया।
फॉर्मल मैथमेटिक्स का उद्देश्य यह सुनिश्चित करना है कि इसकी नींव की संरचना विश्वसनीय हो। गणितज्ञ Lean नामक एक प्रोग्रामिंग भाषा का उपयोग करके सबूतों को कोड में फिर से लिखते हैं, और फिर एक proof assistant नामक प्रोग्राम इन कोड की प्रत्येक पंक्ति की जांच करता है। यदि सबूत सफल हो जाता है, तो गणितज्ञ इस पर विश्वास कर सकते हैं कि यह तार्किक रूप से मान्य है।
इंजीनियर भी एक ही दृष्टिकोण, अर्थात् औपचारिक प्रमाणीकरण, का उपयोग करते हैं ताकि यह सुनिश्चित किया जा सके कि चिप डिज़ाइन कार्यात्मक है; फ्रांसीसी शोधकर्ताओं ने इसका उपयोग करके पारिवारिक सहायता के सॉफ़्टवेयर में वैलिडेशन की खोज की।
Stacks प्रोजेक्ट जैसे संग्रह के लिए, प्रमेयों की एक-एक करके जांच करना कार्य का एक हिस्सा है। Stacks में प्रमेय और परिभाषाएँ एक-दूसरे से जुड़ी होती हैं, और प्रत्येक पिछले सामग्री पर आधारित होती है। एक परिवार वृक्ष की तरह, Stacks में कई परिणाम पुराने परिणामों तक जा सकते हैं।
इस आपसी संबंध के कारण, Axiom को शुरुआत में यह अनिश्चित था कि यह प्रोजेक्ट संभव है या नहीं। टीम को लगभग 1.6 करोड़ पंक्तियों के Lean कोड में हर एक कनेक्शन को पूर्ण और अखंड रखना था।
एक्सियम के सीईओ करीना हॉंग ने टेकक्रंच को बताया: "वास्तविकता में, आकार और सूक्ष्मता आमतौर पर संगठित नहीं होते। [स्टैक्स] गणितीय आधार बनाने वाले गणितीय परिणामों का एक समूह है। आप चाहते हैं कि [प्रमेय] एक-दूसरे के साथ सुसंगठित हों, न कि परोक्षता की तरह। आप चाहते हैं कि इन परिभाषाओं के बीच कोई टकराव न हो।"
यह 25 वर्षीय सीईओ ने स्टैनफोर्ड विश्वविद्यालय के गणित के डॉक्टरेट प्रोग्राम से ड्रॉपआउट किया और 2025 मार्च में इस कंपनी की स्थापना की। इस वर्ष मार्च में, Axiom ने Menlo Ventures के नेतृत्व में 2 बिलियन डॉलर की A-टूर फंडिंग पूरी की।
हॉंग ने कहा: "हमें तब यकीन नहीं था कि vibe coding स्टैक्स की सुंदरता को बरकरार रख पाएगा।"
इस प्रोजेक्ट को पूरा करने के लिए, टीम ने एजेंट्स के लिए एक ढीली संरचना निर्धारित की और उन्हें समानांतर रूप से चलाया। एक्सियम तकनीकी टीम के सदस्य अश्विन स्वामिनाथन कहते हैं: “स्टैक्स के लिए, हमने एक पदानुक्रमित संरचना बनाई... लेकिन ऐसी नहीं जो हर एजेंट को बिल्कुल यह बताती हो कि वह क्या करे। एजेंट स्वयं कार्य ढूंढते हैं और उन चीजों को पहचानते हैं जिन्हें समानांतर रूप से संभाला जा सकता है।”
Axiom ने अपने मॉडल को गणित में कुशल बनाने के लिए भी प्रशिक्षित किया है। होंग कहते हैं कि यह दृष्टिकोण अधिकांश अन्य पुष्टि-आधारित स्टार्टअप्स द्वारा अपनाया नहीं गया है। शुरुआत में, टीम एक आंतरिक Lean विशेषज्ञ पर निर्भर थी जो इन एजेंट्स को मानवीय निर्णय मानदंडों को विकसित करने के लिए प्रशिक्षित करता था। समय के साथ, होंग कहते हैं, इन एजेंट्स ने खुद ही इस निर्णय क्षमता को सीख लिया है।
यह उपलब्धि औपचारिक गणित के सबसे बड़े रिक्त स्थानों में से एक को भरती है। स्वामिनाथन कहते हैं: "जब आप पहले से औपचारिक रूप से दर्ज किए गए गणित को देखते हैं, तो आपको एक विशाल ब्लैक होल दिखाई देता है। और वह ब्लैक होल बीजगणितीय ज्यामिति को कवर करता है।"
स्वामिनाथन ने कहा कि अब तक, लीन का उपयोग करके बीजीय ज्यामिति के नए कार्यों की जांच करने वाले शोधकर्ताओं के पास लगभग कोई तैयार आधार नहीं था। "अब उनके पास है।"
एक्सियम का मानना है कि प्रत्येक सत्यापित परिणाम एक ईंट बन जाता है, जिस पर भविष्य के सबूत पहले से जांचे गए गणित के आधार पर बनाए जा सकते हैं, बिना शुरुआत से शुरू किए। यूसीएलए के गणितज्ञ और फील्ड्स पुरस्कार विजेता टेरेंस टाओ ने इसे अधिक संक्षेप में इस प्रकार समझाया: "जितने अधिक आपके पास औपचारिक सबूत होंगे, आप उतने ही अधिक औपचारिक सबूत बना सकते हैं।"
एक्सियम का लक्षित दर्शक केवल गणितज्ञ ही नहीं है। डेवलपर्स लंबे समय से अपने कोड में दोष और सुरक्षा जोखिमों को दूर करने के लिए प्रयासरत हैं। जैसे-जैसे AI एजेंट अधिक सॉफ्टवेयर लिखते जा रहे हैं, यह समस्या और बड़ी होती जा रही है।
Axiom बेटिंग, भविष्य के सॉफ्टवेयर को आज के Stacks की तरह साबित आधार पर बनाया जाना चाहिए।
स्वामिनाथन ने कहा: "हम मानते हैं कि गणित वह क्षेत्र है जहाँ से आप इन चीजों को बनाना शुरू करते हैं, और यह एक स्थानांतरणीय कौशल है। एजेंट हमारे कोड को पढ़ सकते हैं, इसे समझ सकते हैं, और इस पर नए बुनियादी ढांचे का निर्माण कर सकते हैं। हमने लीन का उपयोग करके जो औपचारिकता बनाई है, वह अब एजेंट के लिए नींव का काम करती है।"
एक्सियम द्वारा स्टैक्स के निर्माण का तरीका—समानांतर कार्य करना, अपने कार्य चुनना—वही है जिसे हॉंग भविष्य में अधिकांश AI कार्यों के लिए अपेक्षा करती है। वह मानती है कि AI एजेंट को गंदगी उत्पन्न करने से बचने के लिए एक सुसंगठित, पुनःउपयोगयोग्य ज्ञान भंडार की आवश्यकता होती है।
हॉंग कहते हैं: "आप चाहते हैं कि [एजेंट] एक पुन: उपयोग योग्य भंडार रखे, जिस पर वे आगे बना सकें और सीमाओं को आगे बढ़ा सकें। यदि शुरुआत में खराब इंजीनियरिंग के चुनाव के साथ कचरा भर दिया जाए, तो उन्हें उस सीमा को विस्तारित करना मुश्किल हो जाएगा।"
होंग इस विधि पर बहुत अधिक विश्वास रखती हैं और खुले तौर पर चुनौती भी देती हैं। उन्होंने कहा, "मैं सभी प्रोग्रामिंग कंपनियों को खुले तौर पर चुनौती देती हूँ कि वे इस स्केल पर फॉर्मल वर्क करें।"