आर्टिफिशियल इंटेलिजेंस की मदद से सॉफ्टवेयर को पूरी तरह बग-फ्री बनाने की तैयारी, गणितीय फॉर्मूलों पर टिके स्टार्टअप्स में करोड़ों डॉलर का निवेश

सॉफ्टवेयर में गलतियों और सुरक्षा खामियों को खत्म करने के लिए औपचारिक सत्यापन का सहारा लिया जा रहा है, जिसे अब एआई स्टार्टअप्स गणितीय फॉर्मूलों के जरिए तेज और किफायती बनाने में जुटे हैं।

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

इसका आप पर असर
सॉफ्टवेयर कोड को गणितीय रूप से प्रमाणित करने की तकनीक आम उपयोगकर्ताओं के डिजिटल जीवन और डेटा सुरक्षा को अधिक पुख्ता बनाएगी।

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

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

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

सवाल-जवाब

1. सॉफ्टवेयर में औपचारिक सत्यापन यानी फॉर्मल वेरिफिकेशन क्या होता है?
यह एक ऐसी तकनीक है जिसमें सॉफ्टवेयर कोड को गणितीय समीकरणों में बदलकर तार्किक रूप से यह साबित किया जाता है कि उसमें कोई बग या सुरक्षा खामी नहीं है।

2. क्या सामान्य टेस्टिंग से सॉफ्टवेयर पूरी तरह सुरक्षित नहीं हो सकता?
सामान्य टेस्टिंग में खरबों परीक्षणों के बावजूद कई अप्रत्याशित और सूक्ष्म गलतियां छूट जाती हैं, जिन्हें केवल गणितीय सत्यापन ही पूरी सटीकता से पकड़ सकता है।

3. स्टार्टअप &Truth और हारमोनिक ने अब तक कितना फंड जुटाया है?
&Truth ने निवेशकों से 70 मिलियन डॉलर जुटाए हैं, जबकि हारमोनिक को अब तक 295 मिलियन डॉलर की फंडिंग मिल चुकी है।

4. वर्तमान में किन प्रमुख उत्पादों में इस तकनीक का इस्तेमाल हो रहा है?
बोइंग के विमानों, अमेज़न के वेब सर्वरों और 2.5 बिलियन से अधिक सक्रिय एप्पल उपकरणों के कुछ सुरक्षा-संबंधी सॉफ्टवेयर में इसका उपयोग किया गया है।

5. विशेषज्ञ औपचारिक सत्यापन को लेकर किस बात से सावधान करते हैं?
विशेषज्ञों का कहना है कि यह तकनीक उपयोगकर्ता की मानवीय गलतियों और हार्डवेयर की अचानक खराबी को नहीं रोक सकती, इसलिए इसके साथ व्यापक टेस्टिंग भी जरूरी है।

https://trendkia.com/ai/ai-ki-madada-se-sophtaveyara-ko-puri-taraha-baga-phri-banane-ki-taiyari-ganitiya-phormulon-para-tike-startaapsa-men-karoron-dolara-53403
TrendKia — Har trend, sabse pehle.