Axiom Math ने Stacks Project को वेरिफाई किया, AI स्लॉप पर लगाम

कंपनी के AI एजेंट्स ने लगभग 7,654 पन्नों की इस लाइब्रेरी को करीब 1.6 करोड़ लाइन के कंप्यूटर-चेक्ड कोड में बदला। गणितज्ञ प्रूफ को Lean नाम की प्रोग्रामिंग भाषा में लिखते हैं और proof assistant उसे लाइन-दर-लाइन जाँचता है। जाँच पास होने पर प्रूफ तार्किक रूप से सही माना जाता है।

चुनौती यह थी कि Stacks के प्रमेय और परिभाषाएँ आपस में जुड़ी हैं और हर नतीजा पिछले नतीजों पर टिका है। CEO Carina Hong के अनुसार शुरू में टीम को भरोसा नहीं था कि यह काम हो पाएगा। टीम ने एजेंट्स को ढीला-सा ढाँचा दिया, और वे खुद काम चुनकर समानांतर रूप से चलते रहे। कंपनी ने गणित के लिए अपने मॉडल भी ट्रेन किए हैं।

सॉफ्टवेयर के लिए क्यों मायने रखता है

Axiom के Ashvin Swaminathan के अनुसार औपचारिक गणित में बीजगणितीय ज्यामिति एक बड़े “ब्लैक होल” जैसी थी, जिस पर Lean में नया काम जाँचने वाले शोधकर्ताओं के पास भरोसेमंद आधार नहीं था। कंपनी का तर्क है कि हर वेरिफाइड नतीजा आगे के प्रूफ के लिए ईंट बनता है। Terence Tao भी कह चुके हैं: “जितने ज्यादा formalized प्रूफ होंगे, उतने ज्यादा बनाए जा सकेंगे।”

निशाने पर केवल गणितज्ञ नहीं हैं। जैसे-जैसे AI एजेंट्स ज्यादा कोड लिख रहे हैं, बग और सुरक्षा खामियों से मुक्त कोड की गारंटी देना कठिन होता जा रहा है। Axiom का मानना है कि भविष्य के सॉफ्टवेयर को वेरिफाइड नींव पर खड़ा होना होगा। कंपनी का मूल्यांकन 1.6 अरब डॉलर है और मार्च में उसने Menlo Ventures के नेतृत्व में 20 करोड़ डॉलर की Series A जुटाई थी। Hong ने अन्य कोडिंग कंपनियों को इसी स्तर पर formalization करने की खुली चुनौती दी है।