Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation

यहाँ शोध पत्र "Probabilistic Verification of Neural Networks via Efficient Probabilistic Hull Generation" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र सुरक्षा-महत्वपूर्ण प्रणालियों (safety-critical systems) में डीप न्यूरल नेटवर्क (DNNs) के लिए प्रायिकता सत्यापन (probabilistic verification) की चुनौती को संबोधित करता है।

• संदर्भ: नियतात्मक सत्यापन (deterministic verification - यह जांचना कि क्या एक विशिष्ट इनपुट किसी बाधा का उल्लंघन करता है) के विपरीत, प्रायिकता सत्यापन इस बात का अनुमान लगाता है कि एक DNN कितनी संभावना के साथ सुरक्षा बाधाओं को संतुष्ट करता है, जब इनपुट शोर (noise) के अधीन होता है जिसे एक प्रायिकता वितरण (विशेष रूप से, बहुभिन्नरूपी गाऊसी वितरण/multivariate Gaussian distributions) द्वारा मॉडल किया जाता है।
• चुनौती: मौजूदा विधियाँ इस समस्या के साथ संघर्ष करती हैं क्योंकि:
  • गाऊसी शोर (Gaussian noise) असीमित (unbounded) होता है, जिससे पारंपरिक आउटपुट रेंज विश्लेषण (जो सीमित इनपुट मानकर चलता है) अप्रभावी हो जाता है।
  • DNN की जटिलता के कारण सुरक्षा प्रायिकता की सटीक गणना करना अव्यवहार्य (intractable) है।
  • अत्याधुनिक विधियाँ डाइमेंशनलिटी के अभिशाप (curse of dimensionality) से ग्रस्त हैं, जो अक्सर इनपुट स्पेस के समान विभाजन (uniform partitioning) की मांग करती हैं, जिससे घातीय उपविभाजन (exponential subdivisions) होते हैं और महत्वपूर्ण निर्णय सीमाएँ (decision boundaries) अनदेखी रह जाती हैं।
  • कुछ मौजूदा उपकरण (जैसे, ProbStar) केवल ReLU सक्रियण कार्यों (activation functions) तक सीमित हैं।

2. कार्यप्रणाली (Methodology)

लेखक एक नया ढांचा प्रस्तावित करते हैं जो कुशल प्रायिक हल (probabilistic hulls) की पहचान करके सुरक्षित प्रायिकता के लिए एक गारंटीकृत रेंज $[L_s, U_s]$ की गणना करता है।

मुख्य अवधारणा: प्रायिक हल (Core Concept: Probabilistic Hulls)

एक प्रायिक हल, इनपुट स्पेस में एक बंद, परिबद्ध सेट (आमतौर पर एक बॉक्स) है जो गाऊसी वितरण के ओरिएंटेशन के अनुरूप होता है। ऐसे हल के भीतर एक बिंदु के गिरने की प्रायिकता की गणना त्रुटि फलन ($\text{erf}$) का उपयोग करके कुशलतापूर्वक की जा सकती है।

• सुरक्षित हल (Safe Hulls): वे क्षेत्र जहाँ DNN आउटपुट सुरक्षा गुण को सख्ती से संतुष्ट करता है।
• असुरक्षित हल (Unsafe Hulls): वे क्षेत्र जहाँ DNN आउटपुट सुरक्षा गुण का सख्ती से उल्लंघन करता है।
• लक्ष्य: "अज्ञात" प्रायिकता क्षेत्र को कम करने के लिए बड़े सुरक्षित/असुरक्षित हलों द्वारा कवर की गई प्रायिकता द्रव्यमान (probability mass) को अधिकतम करना।

तीन-चरणीय ढांचा (The Three-Step Framework)

यह दृष्टिकोण तीन नवाचारों द्वारा निर्देशित एक पुनरावृत्ति परिशोधन लूप (iterative refinement loop) पर निर्भर करता है:

1. सीमा-जागरूक नमूनाकरण (Boundary-Aware Sampling)
रैंडम यूनिफॉर्म सैंपलिंग के बजाय, यह विधि एक संयुक्त नमूनाकरण रणनीति (Combined Sampling Strategy) का उपयोग करती है:

• वितरण नमूनाकरण (Distributional Sampling): उच्च-प्रायिकता घनत्व वाले क्षेत्रों पर ध्यान केंद्रित करने के लिए इनपुट गाऊसीय वितरण के आधार पर नमूने लेना।
• यूनिफॉर्म नमूनाकरण (Uniform Sampling): संतुलित कवरेज सुनिश्चित करने के लिए क्षेत्र के हाशिये (margins) का नमूना लेना।
• अस्वीकृति/उन्मूलन (Rejection/Elimination): यदि किसी क्षेत्र में सुरक्षित और असुरक्षित दोनों नमूने मौजूद हैं (जो इंगित करता है कि एक सीमा मौजूद है), तो विधि एक उन्मूलन तंत्र लागू करती है। यह प्रत्येक नमूने के आउटपुट की सुरक्षा सीमा से दूरी की गणना करती है और उन नमूनों को संभाव्यता के आधार पर अस्वीकार कर देती है जो सीमा से "बहुत दूर" हैं। यह नमनों को निर्णय सीमा (decision boundary) के पास केंद्रित करता है।

2. रिग्रेशन ट्री-निर्देशित उपविभाजन (Regression Tree-Guided Subdivision)

• फिल्टर किए गए नमूनों का उपयोग रिग्रेशन ट्री (Regression Tree) बनाने के लिए किया जाता है।
• ट्री निर्माण इनपुट स्पेस को विभाजित करने के लिए एक अशुद्धता मीट्रिक (Mean Squared Error) को न्यूनतम करता है।
• मुख्य लाभ: यूनिफॉर्म उपविभाजन के विपरीत, यह रणनीति निर्णय सीमा के साथ अनुकूल रूप से स्थान को विभाजित करती है। यह गैर-महत्वपूर्ण क्षेत्रों में अनावश्यक उपविभाजन से बचते हुए, सीमा से दूर क्षेत्रों में बड़े "शुद्ध" सुरक्षित या असुरक्षित बॉक्स (हल) बनाती है।

3. प्रायिक प्राथमिकता के साथ पुनरावृत्ति परिशोधन (Iterative Refinement with Probabilistic Prioritization)

• एल्गोरिदम: मुख्य एल्गोरिदम तीन सेट बनाए रखता है: $R_{safe}$, $R_{unsafe}$, और $R_{unknown}$।
• चयन: प्रत्येक पुनरावृत्ति में, यह उच्चतम प्रायिकता द्रव्यमान वाले $R_{unknown}$ क्षेत्र का चयन करता है।
• सत्यापन: चयनित क्षेत्र को रिग्रेशन ट्री का उपयोग करके विभाजित किया जाता है। परिणामी लीफ नोड्स (उप-क्षेत्रों) को यह निर्धारित करने के लिए CROWN (एक रैखिक बाउंड प्रोपेगेशन टूल) का उपयोग करके सत्यापित किया जाता है कि वे सुरक्षित, असुरक्षित या मिश्रित हैं।
• समाप्ति: लूप तब तक जारी रहता है जब तक कि $R_{unknown}$ सेट का कुल प्रायिकता द्रव्यमान एक थ्रेशोल्ड $\epsilon$ से नीचे नहीं गिर जाता।
• बाउंड्स की गणना (Bounds Calculation):
  • निचला बाउंड ($L_s$): सभी सत्यापित सुरक्षित हलों की प्रायिकताओं का योग।
  • ऊपरी बाउंड ($U_s$): $1 - (\text{सभी सत्यापित असुरक्षित हलों की प्रायिकताओं का योग})$।

3. प्रमुख योगदान (Key Contributions)

1. रिग्रेशन ट्री-निर्देशित रणनीति: रिग्रेशन ट्री का उपयोग करके सुरक्षा सीमा को अनुमानित करके बड़े, उच्च-प्रायिकता वाले सुरक्षित/असुरक्षित हल उत्पन्न करने की एक विधि पेश करता है, जो यूनिफॉर्म पार्टीशनिंग की तुलना में आवश्यक उपविभाजनों की संख्या को काफी कम कर देता है।
2. सीमा-जागरूक नमूनाकरण: एक ऐसी नमूना तकनीक विकसित करता है जो रिजेक्शन सैंपलिंग का उपयोग करके इनपुट स्पेस में सुरक्षा सीमाओं की पहचान करती है, जिससे यह सुनिश्चित होता है कि रिग्रेशन ट्री निर्णय सीमा से प्रासंगिक डेटा पर निर्मित हों।
3. सामान्य प्रयोज्यता और दक्षता: यह विधि DNN को एक ब्लैक बॉक्स के रूप में मानती है, जिससे यह किसी भी सक्रियण कार्य (केवल ReLU ही नहीं) वाले नेटवर्क के लिए लागू करने योग्य बन जाती है। यह बुनियादी Branch-and-Bound (BaB) दृष्टिकोणों की तुलना में 10 गुना तक की गति वृद्धि (speedup) प्राप्त करती है और ProbStar जैसे मौजूदा उपकरणों की तुलना में अधिक सटीक बाउंड प्रदान करती है।

4. प्रयोगात्मक परिणाम (Experimental Results)

इस पद्धति का मूल्यांकन तीन बेंचमार्क पर किया गया: ACAS Xu (विमान टक्कर बचाव), Rocket Lander Controller (SpaceX Falcon 9), और डिस्टिल्ड Tanh-आधारित DNNs।

• सटीकता (Accuracy): प्रस्तावित विधि ने लगातार अधिक सटीक बाउंड (छोटा $U_s - L_s$ अंतर) उत्पन्न किए। उदाहरण के लिए, ACAS Xu पर, इसने अज्ञात प्रायिकता अंतराल को काफी कम कर दिया जबकि ProbStar में अक्सर बड़े अंतराल थे।
• दक्षता (Efficiency):
  • रनटाइम: विधि काफी तेज़ थी। Rocket Lander बेंचमार्क पर, इसने ~23 सेकंड का रनटाइम प्राप्त किया, जबकि ProbStar (पैरेलल सेटिंग में) ने ~319 सेकंड लिए।
  • स्केलेबिलिटी: बुनियादी BaB के विपरीत, जो उच्च-आयामी इनपुट (जैसे, Rocket Lander) पर टाइम-आउट हो गया था, प्रस्तावित विधि ने उन्हें सफलतापूर्वक संभाला।
  • पैरेललाइजेशन: सत्यापन के लिए GPU-त्वरित CROWN का लाभ उठाने से पर्याप्त गति मिली (औसत 4.8×)।
• सामान्य प्रयोज्यता: सफलतापूर्वक Tanh सक्रियण कार्यों वाले नेटवर्क को सत्यापित किया, एक ऐसी क्षमता जहाँ ProbStar (जो केवल ReLU तक सीमित है) विफल हो जाता है।

5. महत्व (Significance)

यह कार्य अनिश्चितता के तहत AI प्रणालियों के औपचारिक सत्यापन (formal verification) में एक महत्वपूर्ण प्रगति का प्रतिनिधित्व करता है।

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