Anthropic का Claude अब कोड लिखता है और इसे स्वचालित रूप से सुरक्षित साबित करता है
decoder ·
Anthropic ने Theorem के साथ साझेदारी की है ताकि यह दिखाया जा सके कि उसका AI मॉडल Claude मौजूदा सॉफ़्टवेयर कोड की सहीता की पुष्टि करने वाले गणितीय प्रमाणों को स्वचालित रूप से उत्पन्न कर सकता है। एक हालिया परियोजना में, Claude ने Google के OSS-Fuzz प्रोजेक्ट की 123 ओपन-सोर्स लाइब्रेरीज़ के लिए लगभग 180 मिलियन पंक्तियों के प्रमाण कोड कुछ ही हफ्तों में तैयार किया। इस स्वायत्त प्रक्रिया में क्रैश टेस्ट को गणितीय समस्याओं में बदला गया और कंपाइल्ड मैशीन कोड का विश्लेषण किया गया, जबकि परिणामों की जांच Rocq नामक एक स्वतंत्र टूल द्वारा की गई। इस सत्यापन चरण के दौरान, Claude ने सैकड़ों बग खोजे जो वर्षों तक चलने वाली रूढ़िवादी परीक्षण विधियों द्वारा छूट गए थे, जिसमें व्यापक रूप से उपयोग किए जाने वाले PDF रीडर में गंभीर सुरक्षा कमियां भी शामिल थीं। हालांकि, ये औपचारिक प्रमाण कड़े सीमाओं के अधीन हैं, जो केवल विशिष्ट प्रोसेसर आर्किटेक्चर, सिंगल-थ्रेडेड प्रोग्राम और 64 MB से कम इनपुट पर लागू होती हैं। कंप्यूटेशनल लागत अभी भी अधिक है, लेकिन Anthropic का कहना है कि नए मॉडल अधिक कुशल हो रहे हैं और समान प्रमाणों को हल करने के लिए कम टोकन की आवश्यकता होती है। कंपनी का लक्ष्य AI-संचालित औपचारिक सत्यापन को मानक सॉफ़्टवेयर परीक्षण के रूप में सामान्य बनाना है, जिससे डेवलपर्स के AI-जनित कोड पर भरोसा करने और उसकी समीक्षा करने के तरीके में संभावित रूप से परिवर्तन आएगा।
decoder