आर्टिफिशियल इंटेलिजन्स सॉफ्टवेअर डेव्हलपमेंटला आकार देत असल्याने, एक लहान स्टार्टअप सट्टेबाजी करत आहे की उद्योगातील पुढील मोठी अडचण कोड लिहिणार नाही – तो त्यावर विश्वास ठेवेल.
Y Combinator च्या स्प्रिंग 2025 बॅचमधून बाहेर पडलेल्या सॅन फ्रान्सिस्को-आधारित कंपनीने मंगळवारी जाहीर केले की त्यांनी AI-व्युत्पन्न सॉफ्टवेअरचे प्रमाणीकरण करणारी स्वयंचलित साधने तयार करण्यासाठी $6 दशलक्ष बीज निधी उभारला आहे. Y Combinator, e14, SAIF, Halcyon आणि रिकर्शन फार्मास्युटिकल्सचे सह-संस्थापक ब्लेक बोर्गेसन आणि ब्लॉकचेन प्लॅटफॉर्म Tezos चे सह-संस्थापक आर्थर ब्रेटमन यांच्यासह एंजल गुंतवणूकदारांच्या सहभागासह खोसला व्हेंचर्सने या फेरीचे नेतृत्व केले.
गुंतवणूक निर्णायक क्षणी येते. GitHub, Amazon आणि Google सारख्या कंपन्यांचे AI कोडिंग सहाय्यक आता वर्षाला कोट्यवधी लाइन्स कोड तयार करतात. एंटरप्राइझचा अवलंब वेगवान होत आहे. परंतु एआयने लिहिलेले सॉफ्टवेअर प्रत्यक्षात उद्दिष्टानुसार कार्य करते याची पडताळणी करण्याच्या क्षमतेने गती राखली नाही – ज्यामुळे प्रमेयचे संस्थापक व्याप्तीची विस्तृतता म्हणून वर्णन करतात. "निरीक्षण अंतर" यामुळे वित्तीय प्रणालीपासून पॉवर ग्रिडपर्यंतच्या गंभीर पायाभूत सुविधांना धोका आहे.
"आम्ही आधीच तिथे आहोत," जेसन ग्रॉस म्हणाले, प्रमेयचे सह-संस्थापक, जेव्हा आम्ही विचारले की एआय-व्युत्पन्न कोड मानवी पुनरावलोकनाच्या क्षमतेपेक्षा जास्त आहे का. "जर तुम्ही मला कोडच्या 60,000 ओळींचे पुनरावलोकन करण्यास सांगितले, तर ते कसे करायचे ते मला माहित नाही."
एआय कोड माणसांच्या पडताळणीपेक्षा वेगाने का लिहितो?
प्रमेयचे मुख्य तंत्रज्ञान औपचारिक पडताळणी एकत्र करते – एक गणितीय तंत्र जे सिद्ध करते की प्रोग्राम निर्दिष्ट केल्याप्रमाणेच वागतो – कृत्रिम बुद्धिमत्ता मॉडेल्ससह स्वयंचलितपणे पुरावे निर्माण आणि सत्यापित करण्यासाठी प्रशिक्षित केले जातात. हा दृष्टीकोन एका प्रक्रियेचे रूपांतर करतो ज्यात ऐतिहासिकदृष्ट्या डॉक्टरेट-स्तरीय अभियांत्रिकी वर्षांची आवश्यकता असते अशा काही गोष्टींमध्ये कंपनीचा दावा आहे की ते आठवड्यात किंवा अगदी दिवसात पूर्ण केले जाऊ शकते.
औपचारिक पडताळणी अनेक दशकांपासून आहे परंतु अधिक मिशन-गंभीर अनुप्रयोगांपुरती मर्यादित राहिली आहे: एव्हियोनिक्स प्रणाली, अणुभट्टी नियंत्रणे आणि क्रिप्टोग्राफिक प्रोटोकॉल. या तंत्राची उच्च किंमत- अनेकदा प्रति कोडच्या आठ ओळींच्या गणितीय पुराव्याची आवश्यकता असते- यामुळे मुख्य प्रवाहातील सॉफ्टवेअर विकासासाठी ते अव्यवहार्य बनले.
सकल हे प्रत्यक्ष जाणते. प्रमेयाची स्थापना करण्यापूर्वी, त्यांनी सत्यापित क्रिप्टोग्राफिक कोडवर काम करत MIT मधून PhD मिळवली जे आता HTTPS सुरक्षा प्रोटोकॉलला सामर्थ्य देते जे दररोज ट्रिलियन इंटरनेट कनेक्शनचे संरक्षण करते. त्यांच्या अंदाजानुसार या प्रकल्पाला पंधरा वर्षांचे काम लागले.
"कोणीही चुकीचा कोड ठेवण्यास प्राधान्य देत नाही," ग्रॉस म्हणाले. "सॉफ्टवेअर पडताळणी इतकी किफायतशीर कधीच नव्हती. पुरावे पीएचडी-स्तरीय अभियंत्यांनी लिहिले होते. आता, एआय हे सर्व लिहित आहे."
औपचारिक पडताळणी पारंपारिक चाचणी चुकवलेल्या त्रुटी कशा शोधते
सिद्धांत प्रणाली एकूण कॉलच्या तत्त्वावर कार्य करते "फ्रॅक्शनल प्रूफ विघटन." जटिल सॉफ्टवेअरसाठी संगणकीयदृष्ट्या अशक्य असलेल्या प्रत्येक संभाव्य वर्तनाची संपूर्णपणे चाचणी करण्याऐवजी- तंत्रज्ञान प्रत्येक कोड घटकाच्या महत्त्वाच्या प्रमाणात सत्यापन संसाधने वाटप करते.
या दृष्टिकोनाने अलीकडेच क्लॉड चॅटबॉटमागील एआय सेफ्टी कंपनी अँथ्रोपिक येथे चाचणी वगळलेल्या बगची ओळख पटवली. ग्रॉस म्हणाले की हे तंत्रज्ञान विकसकांना मदत करते "खूप आकडेमोड न करता आता त्यांच्या चुका शोधा."
SFBench नावाच्या अलीकडील टेक डेमोमध्ये, प्रमेयने Rocq (औपचारिक पुरावा सहाय्यक) पासून लीन (दुसरी पडताळणी भाषा) मध्ये 1,276 समस्यांचे भाषांतर करण्यासाठी AI चा वापर केला आणि नंतर स्वयंचलितपणे सिद्ध केले की प्रत्येक भाषांतर मूळच्या समतुल्य आहे. कंपनीचा अंदाज आहे की तेच काम पूर्ण करण्यासाठी मानवी संघाला अंदाजे 2.7 वर्षे काम करावे लागेल.
"सर्व समांतरपणे एजंट चालवू शकतात, परंतु आम्ही त्यांना मालिकेत देखील चालवू शकतो," ग्रॉसने स्पष्ट केले की, प्रमेयचे आर्किटेक्चर थ्रेडेड कोड हाताळते — जिथे समाधाने डझनभर फाइल्सवर एकमेकांवर अवलंबून असतात — जे संदर्भ विंडोद्वारे प्रतिबंधित पारंपारिक AI एन्कोडर्सपेक्षा जास्त कामगिरी करतात.
एका कंपनीने 1,500-पानांचे तपशील विश्वसनीय कोडच्या 16,000 ओळींमध्ये कसे बदलले
स्टार्टअप आधीच AI संशोधन प्रयोगशाळा, इलेक्ट्रॉनिक डिझाइन ऑटोमेशन आणि GPU-प्रवेगक संगणनामधील ग्राहकांसह कार्य करते. एका केस स्टडीने या तंत्रज्ञानाचे व्यावहारिक मूल्य स्पष्ट केले आहे.
एक ग्राहक 1,500-पृष्ठ पीडीएफ स्पेसिफिकेशन आणि मेमरी लीक, क्रॅश आणि इतर मायावी बग्समुळे ग्रस्त असलेल्या कालबाह्य सॉफ्टवेअर अंमलबजावणीसह प्रमेयाकडे आला. त्यांची सर्वात महत्त्वाची समस्या: 10Mbps ते 1Gbps पर्यंत कार्यप्रदर्शन सुधारणे — 100x वाढ — अतिरिक्त त्रुटींचा परिचय न करता.
प्रमेय प्रणालीने उत्पादन कोडच्या 16,000 ओळी व्युत्पन्न केल्या, ज्याचे ग्राहकाने स्वतः पुनरावलोकन न करता उपयोजित केले. आत्मविश्वास अंगभूत एक्झिक्युटेबल स्पेसिफिकेशनमधून आला आहे—काहीशे ओळी ज्यांनी मोठ्या पीडीएफ दस्तऐवजाचे सामान्यीकरण केले आहे—एक समतुल्यता तपासकासह एकत्रित केले आहे जे हे सत्यापित करते की नवीन अंमलबजावणी अपेक्षित वर्तनाशी जुळते.
"आता त्यांच्याकडे 1 Gbps वर चालणारे उत्पादन विश्लेषक आहे आणि विश्लेषणादरम्यान कोणतीही माहिती गमावली जाणार नाही या विश्वासाने ते तैनात करू शकतात." ग्रॉस म्हणाले.
गंभीर पायाभूत सुविधांसाठी AI-व्युत्पन्न सॉफ्टवेअरमध्ये निहित सुरक्षा धोके
धोरणकर्ते आणि तंत्रज्ञ गंभीर पायाभूत सुविधांमध्ये एम्बेड केलेल्या AI प्रणालींच्या विश्वासार्हतेची अधिकाधिक छाननी करत असताना निधीची घोषणा करण्यात आली आहे. सॉफ्टवेअर आधीच आर्थिक बाजार, वैद्यकीय उपकरणे, वाहतूक नेटवर्क आणि इलेक्ट्रिकल ग्रिडवर वर्चस्व गाजवत आहे. हे सॉफ्टवेअर किती लवकर विकसित होऊ शकते आणि सूक्ष्म त्रुटी किती सहजपणे पसरू शकतात हे AI वेगवान करत आहे.
सुरक्षेच्या दृष्टिकोनातून पूर्णपणे आव्हानात्मक फ्रेम. AI असुरक्षा शोधणे आणि त्यांचे शोषण करणे कमी खर्चिक बनवते म्हणून, बचावकर्त्यांना त्याला काय म्हणतात ते आवश्यक आहे "असममित संरक्षण" – संसाधनांमध्ये आनुपातिक वाढ न करता विस्तारणारे संरक्षण.
"सॉफ्टवेअर सुरक्षा हा हल्ला आणि बचाव यांच्यातील नाजूक संतुलन आहे." तो म्हणाला. "एआय हॅकिंगसह, सिस्टम हॅक करण्याची किंमत झपाट्याने कमी होते. असममित संरक्षण हा एकमेव व्यवहार्य उपाय आहे. मॉडेल सुधारणांच्या काही पिढ्यांपेक्षा जास्त काळ टिकणारे सॉफ्टवेअर सुरक्षा उपाय आम्हाला हवे असल्यास, ते पडताळणीद्वारे होईल."
नियामक संस्थांनी गंभीर प्रणालींमध्ये एआय-व्युत्पन्न कोडचे औपचारिक सत्यापन अनिवार्य केले पाहिजे का असे विचारले असता, ग्रॉसने स्पष्ट उत्तर दिले: "आता औपचारिक पडताळणी पुरेशी स्वस्त आहे, गंभीर प्रणालींबद्दल आश्वासने मिळविण्यासाठी त्याचा वापर न करणे हे घोर निष्काळजीपणा मानले जाऊ शकते."
इतर AI कोड पडताळणी स्टार्टअप्सपासून प्रमेय वेगळे काय करते?
प्रमेय अशा बाजारपेठेत प्रवेश करतो जेथे अनेक स्टार्टअप आणि संशोधन प्रयोगशाळा AI आणि औपचारिक पडताळणी दरम्यान छेदनबिंदू शोधत आहेत. ग्रॉसचे म्हणणे आहे की कंपनीचे वेगळेपण गणित किंवा इतर फील्डवर पडताळणी लागू करण्याऐवजी सॉफ्टवेअरवर देखरेख वाढविण्यावर लक्ष केंद्रित करते.
"आमची साधने सिस्टीम अभियांत्रिकी संघांसाठी उपयुक्त आहेत, जे बेअर मेटलच्या जवळ काम करतात आणि बदलांचे एकत्रीकरण करण्यापूर्वी त्यांना योग्य आश्वासनांची आवश्यकता असते," तो म्हणाला.
संस्थापक संघ ही कलात्मक दिशा प्रतिबिंबित करतो. ग्रॉसला प्रोग्रॅमिंग लँग्वेज थिअरीचा सखोल अनुभव आहे आणि व्हेरिफाईड कोड उत्पादनात मोठ्या प्रमाणावर तैनात करण्याचा सिद्ध ट्रॅक रेकॉर्ड आहे. सह-संस्थापक राजश्री अग्रवाल, एक मशीन लर्निंग संशोधन अभियंता, पडताळणी प्रक्रियेस समर्थन देणाऱ्या AI मॉडेल्सच्या प्रशिक्षणावर लक्ष केंद्रित करते.
"आम्ही औपचारिक सॉफ्टवेअर विचारांवर काम करत आहोत जेणेकरून प्रत्येकजण केवळ सामान्य सॉफ्टवेअर अभियंत्याच्या पातळीवर AI च्या कामावर देखरेख करू शकत नाही तर लिनस टोरवाल्ड्सच्या स्तरावर AI क्षमतांचा वापर करू शकतो," अग्रवाल लिनक्सच्या दिग्गज निर्मात्याचा उल्लेख करत म्हणाले.
एआय कोड प्रत्येक गोष्टीवर ताबा मिळवण्यापूर्वी त्याची पडताळणी करण्याची शर्यत
प्रमेय निधीचा वापर त्याच्या संघाचा विस्तार करण्यासाठी, प्रमाणीकरण मॉडेल्सचे प्रशिक्षण देण्यासाठी संगणकीय संसाधने वाढवण्यासाठी आणि रोबोटिक्स, अक्षय ऊर्जा, क्रिप्टोकरन्सी आणि औषध संश्लेषण यासह नवीन उद्योगांमध्ये प्रवेश करण्याची योजना आखत आहे. कंपनीत सध्या चार जण काम करतात.
स्टार्टअपचा उदय एंटरप्राइझ टेक्नॉलॉजी लीडर्सना एआय कोडिंग टूल्सचे मूल्यमापन करण्याच्या पद्धतीत बदल दर्शवतो. AI-शक्तीच्या विकासाच्या पहिल्या लाटेने उत्पादकता वाढण्याचे आश्वासन दिले – अधिक कोड, जलद. पुढच्या लाटेला काहीतरी वेगळं लागेल असा सिद्धांत मांडतो: सुरक्षेच्या खर्चावर वेग येत नाही याचा गणितीय पुरावा.
ढोबळ जोखमींचे स्पष्ट शब्दांत चित्रण करते. एआय प्रणाली नाटकीयरित्या सुधारत आहेत. हा मार्ग असाच चालू राहिल्यास, सुपरसॉफ्टवेअर आर्किटेक्चर अपरिहार्य आहे, मानवाने बनवलेल्या कोणत्याही गोष्टीपेक्षा अधिक जटिल प्रणाली डिझाइन करण्यास सक्षम आहे, असा त्याचा विश्वास आहे.
"नियंत्रणाच्या पूर्णपणे भिन्न अर्थशास्त्राशिवाय," तो म्हणाला, "ज्यावर आमचे नियंत्रण नाही अशा प्रणाली आम्ही उपयोजित करू."
मशीन कोड लिहितात. आता कोणीतरी त्याचे काम तपासावे लागेल.
