Anthropic ने अपने साझेदार Theorem के साथ मिलकर AI मॉडल «Claude» का इस्तेमाल करते हुए यह साबित करने की कोशिश की कि मौजूदा सॉफ्टवेयर कोड सही ढंग से काम करता है। इसके लिए Google की सुरक्षा परियोजना «OSS-Fuzz» में शामिल 123 ओपन-सोर्स लाइब्रेरी को चुना गया। बताया गया है कि कुछ ही हफ्तों में प्रमाण के लिए करीब 18 करोड़ लाइनों का कोड तैयार हुआ और सैकड़ों ऐसे बग भी मिले, जिन्हें पारंपरिक परीक्षणों में नहीं पकड़ा जा सका था।
«टेस्ट पास हुआ» और «सही साबित हुआ» के बीच की दूरी
सॉफ्टवेयर की गुणवत्ता जांचने की बात हो, तो ज्यादातर लोगों के मन में टेस्ट का खयाल आता है। इसमें सॉफ्टवेयर को तय इनपुट देकर यह देखा जाता है कि क्या वह अपेक्षित नतीजा देता है। लेकिन टेस्ट सिर्फ «आजमाए गए दायरे» की जांच कर सकता है। इससे यह पता नहीं चलता कि उन हालात में सॉफ्टवेयर कैसे काम करेगा जिन्हें आजमाया ही नहीं गया।
यहीं औपचारिक सत्यापन काम आता है। इसमें प्रोग्राम के व्यवहार को गणितीय समस्या के रूप में देखा जाता है और यह साबित किया जाता है कि तय शर्तों के दायरे में वह हमेशा सही ढंग से काम करेगा। सिद्धांत रूप में यह तरीका बेहद कारगर है, लेकिन इसमें लगने वाला श्रम बहुत ज्यादा था। छोटे से OS कर्नेल «seL4» का सत्यापन करने में ही विशेषज्ञों की टीम ने कुल मिलाकर 20 व्यक्ति-वर्ष लगाए थे। इसलिए इसका इस्तेमाल यात्री विमानों के नियंत्रण सॉफ्टवेयर जैसे बेहद खास मामलों तक सीमित रहा है।
इस बार Anthropic की Frontier Red Team ने Theorem के साथ मिलकर यह प्रमाण तैयार करने का काम Claude को सौंपा। उससे नया कोड नहीं लिखवाया गया। इसके बजाय, पहले से मौजूद सॉफ्टवेयर पर क्रैश की जांच करने वाले टेस्टों को गणितीय समस्याओं में बदला गया। फिर Claude ने संकलन के बाद बने मशीन कोड तक का विश्लेषण कर बड़ी संख्या में प्रमाण तैयार किए।
प्रमाणों की «जांच» करने वाला अलग प्रोग्राम
अगर AI अपने लिखे प्रमाण को खुद ही «पास» बता दे, तो उसकी बात पर भरोसा करना मुश्किल होगा। इस मामले में जांच की व्यवस्था खास है। तैयार किए गए प्रमाणों की Rocq नाम का एक स्वतंत्र सत्यापन प्रोग्राम अपने आप जांच करता है। Anthropic के मुताबिक, इस प्रक्रिया में मानव समीक्षकों की लगभग जरूरत नहीं पड़ती।
शोध दल इसे प्रमाण तैयार करने की «पूरी तरह स्वायत्त» प्रक्रिया कहता है। हालांकि, प्रमाणों के लिए इस्तेमाल किए गए टूल और औपचारिक आधार Theorem के लोगों ने बनाए थे। इसे इस तरह समझना ज्यादा सही होगा कि AI ने सब कुछ शून्य से नहीं बनाया, बल्कि इंसानों द्वारा तैयार किए गए ढांचे में बड़ी मात्रा में प्रमाण तेजी से लिखे।
प्रमाण तैयार करते समय मिले सैकड़ों बग
प्रमाण तैयार करने की प्रक्रिया में Claude को सैकड़ों बग मिले और उसे उन्हें खुद ठीक करने की भी अनुमति थी। शोधकर्ताओं के मुताबिक, इनमें से ज्यादातर बग सिर्फ बेहद बड़ी इनपुट फाइलों या किसी खास क्रम में मेमरी तक पहुंचने जैसी सीमित परिस्थितियों में सामने आते हैं। इसलिए यह हैरानी की बात नहीं कि वे आम टेस्टों में पकड़ में नहीं आए।
इसके कुछ ठोस उदाहरण भी दिए गए हैं। व्यापक रूप से इस्तेमाल होने वाले एक PDF रीडर के सत्यापन में एक हफ्ते के भीतर उतने ही सुरक्षा बग मिले, जितने आम तौर पर उस सॉफ्टवेयर में एक साल में रिपोर्ट होते हैं। बताया गया है कि एक अन्य एप्लिकेशन में ऐसा तार्किक दोष भी मिला, जिस पर 10 साल से ज्यादा समय तक किसी का ध्यान नहीं गया था।
एक और अहम बात यह है कि अगर प्रमाण अंत तक पूरा न हो, तो उसका क्या होता है। Anthropic का कहना है कि प्रमाण तैयार करने में विफल रहने पर भी, कोशिश के दौरान असली बग सामने आ सकते हैं। यानी प्रमाण तैयार करना सिर्फ «पास» होने का प्रमाणपत्र हासिल करने का तरीका नहीं, बल्कि बग खोजने वाली जांच-पड़ताल का साधन भी है। ऐसा लगता है कि यह पारंपरिक टेस्टों की जगह लेने के बजाय उनकी कमियों को पूरा कर सकता है।
«औपचारिक रूप से सत्यापित» होने का दायरा समझें
फिर भी, «औपचारिक रूप से सत्यापित» होने का मतलब «कोई बग नहीं» मान लेना जोखिम भरा है। Anthropic भी मानता है कि प्रमाण केवल कड़ी शर्तों के दायरे में लागू होता है। इसमें एक खास प्रोसेसर कॉन्फिगरेशन, सिंगल-थ्रेड में चलने वाला प्रोग्राम और 64MB से छोटी इनपुट फाइलें शामिल हैं। जबकि असल दुनिया में लाइब्रेरी कई तरह के हार्डवेयर और सेटिंग्स पर चलती हैं।
इसकी लागत भी कम नहीं है। बताया गया है कि कुछ मामलों में एक-एक प्रमाण तैयार करने में कई अरब टोकन लग सकते हैं। पूरी परियोजना की लागत सार्वजनिक नहीं की गई है। हालांकि, छोटे पैमाने पर किए गए अतिरिक्त प्रयोगों से पता चला कि प्रमाणों का दोबारा इस्तेमाल किया जा सकता है और नए मॉडल ज्यादा दक्ष होते जा रहे हैं। बताया गया है कि Opus 5.5 को आधे प्रमाण हल करने के लिए Opus 5 की तुलना में करीब 40% कम टोकन की जरूरत पड़ती है।
सवाल अब «क्या AI प्रोग्राम लिख सकता है» नहीं रहा
अगर AI कोड लिखने के साथ-साथ कुछ शर्तों के तहत उसकी शुद्धता की गारंटी भी दे सके, तो सवाल पूछने का तरीका बदल जाता है। सवाल «क्या AI प्रोग्रामिंग कर सकता है» नहीं, बल्कि «क्या AI अपने लिखे कोड की सुरक्षा साबित कर सकता है» बन जाता है। AI से तैयार कोड की विश्वसनीयता को लेकर चिंतित डेवलपमेंट टीमों के लिए यह बदलाव अहम है। अगर AI खुद अपने कोड की जांच कर सके, तो इससे मानव समीक्षकों पर काम का बोझ घट सकता है और सिर्फ सत्यापन ही नहीं, बल्कि विकास की पूरी प्रक्रिया की लागत भी कम हो सकती है।
Anthropic का अनुमान है कि निकट भविष्य में AI के जरिए औपचारिक सत्यापन, सामान्य टेस्टों जितना ही आम हो जाएगा। Theorem के रोडमैप में glibc, OpenSSL और cURL जैसे अहम बुनियादी सॉफ्टवेयर भी शामिल हैं।
यहाँ अहम बात प्रमाण की “सामग्री” नहीं, बल्कि उसकी “मान्यताओं” को समझने की क्षमता होगी। प्रमाण किन परिस्थितियों और किस तरह के इनपुट को ध्यान में रखकर तैयार किया गया है? ऐसे दौर में, जब जाँच का काम भी AI को सौंपा जा रहा है, उन मान्यताओं की पुष्टि करने की मानवीय समझ ही सुरक्षा की आखिरी ढाल साबित हो सकती है।
コメント