CrypFormBench: Benchmarking Formal Analysis Capability of Large Language Models for Cryptographic Schemes
यह शोधपत्र CrypFormBench प्रस्तुत करता है, जो 677 क्रिप्टोग्राफिक स्कीमों और 7 औपचारिक सत्यापन भाषाओं (formal verification languages) के 700 उदाहरणों से बना एक व्यापक बेंचमार्क है, जिसका उद्देश्य औपचारिक सुरक्षा प्रमाणों को उत्पन्न करने और सुधारने में लार्ज लैंग्वेज मॉडल्स की वर्तमान सीमाओं का मूल्यांकन और अनावरण करना है, साथ ही उनके प्रदर्शन को बेहतर बनाने के लिए व्यावहारिक रणनीतियाँ भी प्रदान करना है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
यहाँ "CrypFormBench" पेपर का सरल भाषा और रचनात्मक उपमाओं (analogies) का उपयोग करके विवरण दिया गया है।
बड़ी तस्वीर: "अनुवादक" (Translator) की समस्या
कल्पना कीजिए कि आप एक मास्टर आर्किटेक्ट हैं जो अविश्वसनीय रूप से सुरक्षित तिजोरियाँ (क्रिप्टोग्राफिक स्कीम्स) डिजाइन करते हैं। आप अपने ब्लूप्रिंट (नक्शे) को साधारण अंग्रेजी में लिखते हैं ताकि कोई भी योजना को समझ सके। हालाँकि, इन तिजोरियों की कमियों को खोजने के लिए उन्हें वास्तव में बनाने और टेस्ट करने के लिए, आपको उन ब्लूप्रिंट्स को एक बहुत ही सख्त, प्राचीन और जटिल भाषा में अनुवादित करने की आवश्यकता होती है जिसे केवल विशिष्ट, हाई-टेक सुरक्षा रोबोट (Scyther या Tamarin जैसे फॉर्मल वेरिफिकेशन टूल्स) ही समझ सकते हैं।
यह अनुवाद करना कठिन है। इसके लिए एक ऐसे मानव विशेषज्ञ की आवश्यकता होती है जो तिजोरी के डिजाइन और रोबोट की सख्त भाषा, दोनों को जानता हो। यदि आप एक छोटा सा कॉमा भी छोड़ देते हैं या गलत शब्द का उपयोग करते हैं, तो रोबोट ब्लूप्रिंट को अस्वीकार कर देता है, या इससे भी बुरा, वह एक ऐसी तिजोरी बनाता है जो सुरक्षित दिखती है लेकिन उसमें एक छिपा हुआ बैकडोर (कमजोरी) हो सकता है।
प्रश्न: क्या लार्ज लैंग्वेज मॉडल्स (LLMs)—जो आज के AI चैटबॉट्स हैं—इन विशेषज्ञ अनुवादकों के रूप में कार्य कर सकते हैं? क्या वे एक साधारण अंग्रेजी विवरण को लेकर तुरंत एक सुरक्षा प्रोटोकॉल के लिए एकदम सही, त्रुटि-रहित कोड लिख सकते हैं?
उत्तर (इस पेपर के अनुसार): अभी पूरी तरह से नहीं। वे पढ़ने और सुधारने में बेहतर हो रहे हैं, लेकिन वे शून्य से (from scratch) लिखने में अभी भी संघर्ष करते हैं।
समाधान: CrypFormBench (AI के लिए "जिम")
यह पता लगाने के लिए कि ये AI अनुवादक वास्तव में कितने अच्छे हैं, शोधकर्ताओं ने CrypFormBench (या C.F.B.) नामक एक विशाल परीक्षण मैदान बनाया।
इसे 700 अलग-अलग वर्कआउट स्टेशनों वाले एक जिम के रूप में सोचें।
- उपकरण (Equipment): उन्होंने 700 वास्तविक दुनिया के सुरक्षा प्रोटोकॉल एकत्र किए (जैसे कि वे जिनका उपयोग आपके फोन, बैंकिंग या इंटरनेट में किया जाता है)।
- भाषाएँ (Languages): उन्होंने इन प्रोटोकॉल को 7 अलग-अलग "रोबोट भाषाओं" (SPDL, HLPSL, EasyCrypt आदि जैसी फॉर्मल भाषाएँ) में अनुवादित किया।
- परीक्षण (Tests): उन्होंने AI को केवल कोड लिखने के लिए नहीं कहा। उन्होंने पांच विशिष्ट कौशलों का परीक्षण किया:
- व्याख्या (Interpretation): "यह एक रोबोट कोड है; मुझे इसे अंग्रेजी में समझाएं।" (पढ़ना)
- जेनरेशन (Generation): "यह एक अंग्रेजी विवरण है; रोबोट कोड लिखें।" (शून्य से लिखना)
- पूर्णता (Completion): "यह एक रोबोट कोड है जिसमें खाली जगहें छोड़ी गई हैं; रिक्त स्थानों को भरें।" (आंशिक काम को ठीक करना)
- रूपांतरण (Transformation): "यह भाषा A में कोड है; इसे भाषा B में फिर से लिखें।" (रोबोट्स के बीच अनुवाद करना)
- सुधार (Correction): "इस रोबोट कोड में एक त्रुटि है; इसे ठीक करें।" (डीबगिंग)
परिणाम: AI की रिपोर्ट कार्ड
शोधकर्ताओं ने 9 सबसे स्मार्ट उपलब्ध AI मॉडल्स (GPT-4o, Claude-3.5, और DeepSeek सहित) का परीक्षण किया। यहाँ उन्हें क्या मिला:
1. "पढ़ने में अच्छा" कौशल (Interpretation & Completion)
- उपमा: कल्पना कीजिए कि एक छात्र है जो टेक्स्टबुक पढ़ने में बहुत अच्छा है और वाक्य में छूटे हुए शब्दों को भर सकता है क्योंकि संदर्भ पहले से ही वहां मौजूद है।
- परिणाम: AI इस मामले में आश्चर्यजनक रूप से अच्छा था। जब उन्हें कोड का एक हिस्सा दिया गया जिसमें कुछ भाग गायब थे, या उनसे पूछा गया कि कोड का एक हिस्सा क्या करता है, तो उन्होंने बहुत अच्छा प्रदर्शन किया। वे सुरक्षा भाषाओं के "व्याकरण" को समझते थे।
2. "लिखने में बुरा" कौशल (Generation & Transformation)
- उपमा: अब उसी छात्र से कल्पना कीजिए कि उसे एक पूरी नई टेक्स्टबुक शून्य से लिखने के लिए कहा जाए, या बिना डिक्शनरी के फ्रेंच से जापानी में एक किताब का अनुवाद करने के लिए कहा जाए। वे कल्पना (hallucinate) करने लगते हैं, नियम बनाने लगते हैं, या सख्त व्याकरण को भूल जाते हैं।
- परिणाम: यहीं पर AI विफल रहा।
- जेनरेशन (Generation): जब एक साधारण अंग्रेजी विवरण से पूरा सुरक्षा प्रोटोकॉल लिखने के लिए कहा गया, तो अधिकांश AI ने ऐसा कोड बनाया जिसे रोबोट चला भी नहीं सकते थे। यह टूटे हुए सिंटैक्स के साथ वाक्य लिखने जैसा था।
- रूपांतरण (Transformation): जब एक रोबोट भाषा से दूसरी में कोड को अनुवादित करने के लिए कहा गया, तो AI अक्सर भ्रमित हो गए। वे दोनों भाषाओं के नियमों को मिला देते थे, जिससे एक "फ्रेंकस्टीन" जैसा कोड बन जाता था जो किसी में भी काम नहीं करता था।
- स्कोर: यहाँ तक कि सबसे अच्छा AI (Claude-3.5) भी 100 में से केवल 48.7 स्कोर कर पाया। इसका मतलब है कि उनके प्रयास आधे से भी कम वास्तव में सुरक्षा उपकरणों द्वारा उपयोग करने योग्य थे।
3. "ठीक करने" का कौशल (Correction)
- उपमा: यदि आप छात्र को एक स्पष्ट टाइपो (जैसे "recieve" के बजाय "receive") वाला वाक्य देते हैं, तो वे इसे आसानी से ठीक कर सकते हैं। लेकिन यदि वाक्य व्याकरणिक रूप से सही है लेकिन तार्किक रूप से गलत है (जैसे, "तिजोरी सभी के लिए खुली है, लेकिन यह सुरक्षित है"), तो वे तर्क संबंधी त्रुटि (logic error) को खोजने में संघर्ष करते हैं।
- परिणाम: AI साधारण सिंटैक्स त्रुटियों (टाइपो) को ठीक करने में अच्छे थे। हालाँकि, वे "सिमेंटिक" त्रुटियों के साथ संघर्ष करते थे—यानी सुरक्षा प्रोटोकॉल के स्वयं के लॉजिक को ठीक करने में।
यह इतना कठिन क्यों है?
पेपर बताता है कि ये "रोबोट भाषाएँ" Python या Java की तरह नहीं हैं। ये अत्यंत सख्त हैं।
- "एक गलती" का नियम: सामान्य कोडिंग में, यदि आप एक सेमीकोलन (semicolon) भूल जाते हैं, तो कंप्यूटर बस शिकायत कर सकता है। इन सुरक्षा भाषाओं में, एक शब्द की कमी पूरे सुरक्षा प्रमाण (security proof) का अर्थ बदल सकती है, जिससे एक सुरक्षित तिजोरी असुरक्षित दिख सकती है, या इसके विपरीत।
- "संदर्भ" की समस्या: ये प्रोटोकॉल अक्सर घटनाओं की लंबी श्रृंखलाओं पर निर्भर करते हैं (जैसे, "यदि एलिस चरण 1 पर एक संदेश भेजती है, तो बॉब को चरण 2 पर जवाब देना चाहिए, लेकिन केवल तभी जब उसने चरण 0 से संदेश न देखा हो")। AI अक्सर इन लंबी श्रृंखलाओं का ट्रैक खो देते हैं।
हम क्या कर सकते हैं? ("ट्रेनिंग व्हील्स")
पेपर सुझाव देता है कि हालांकि हम अभी AI को अकेले पूरा काम करने के लिए भरोसा नहीं कर सकते, फिर भी हम उन्हें सहायक (assistants) के रूप में उपयोग कर सकते हैं यदि हम उन्हें सही मदद दें:
- Few-Shot Prompting: केवल "यह लिखें" कहने के बजाय, AI को पहले दिखाएं कि इसे कैसे लिखना है (तीन उदाहरणों के साथ)। यह एक 'चीट शीट' की तरह काम करता है।
- Pass@K: AI को कोड लिखने के 5 प्रयास करने के लिए कहें, और फिर सबसे अच्छे वाले को चुनें। इससे काम करने योग्य संस्करण मिलने की संभावना बढ़ जाती है।
- Human-in-the-Loop: AI को कोड का ड्राफ्ट तैयार करने के लिए उपयोग करें, लेकिन सुरक्षा रोबोट चलाने से पहले एक मानव विशेषज्ञ से उसकी जांच करवाएं।
मुख्य निष्कर्ष (The Bottom Line)
पेपर निष्कर्ष निकालता है कि लार्ज लैंग्वेज मॉडल्स वर्तमान में सुरक्षा कोड को समझने और ठीक करने के लिए उत्कृष्ट शोध सहायक (research assistants) हैं, लेकिन वे शून्य से नए सुरक्षा प्रोटोकॉल बनाने के लिए अभी तक विश्वसनीय आर्किटेक्ट नहीं हैं।
वे आपको मैनुअल पढ़ने और आपके टाइपो को ठीक करने में मदद कर सकते हैं, लेकिन आपको अभी भी एक मानव विशेषज्ञ की आवश्यकता है जो यह सुनिश्चित करे कि चाबियाँ सौंपने से पहले तिजोरी वास्तव में सुरक्षित है। बेंचमार्क (CrypFormBench) अब अन्य शोधकर्ताओं के लिए उपलब्ध है ताकि वे नए AI मॉडल्स को इन्हीं सख्त मानकों के विरुद्ध टेस्ट कर सकें।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।