Compiling High-Level Neural Network Specifications into VNN-LIB Queries

यह डैगिट, कोके और एटकी के शोध पत्र "Compiling High-Level Neural Network Specifications into VNN-LIB Queries" का विस्तृत तकनीकी सारांश है।

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

पारंपरिक सॉफ्टवेयर के औपचारिक सत्यापन (formal verification) में उच्च-स्तरीय विनिर्देश भाषाओं (जैसे Dafny, F*) द्वारा क्रांति ला दी गई है, जो निम्न-स्तरीय SMT-LIB प्रश्नों में संकलित होती हैं। हालाँकि, न्यूरल नेटवर्क सत्यापन में ऐसा समान बुनियादी ढांचा (infrastructure) की कमी है। वर्तमान उपकरणों के लिए उपयोगकर्ताओं को निम्न-स्तरीय प्रारूपों (जैसे VNN-LIB) में विनिर्देश लिखने की आवश्यकता होती है जो सॉल्वर के आंतरिक प्रतिनिधित्व के करीब होते हैं।

मुख्य चुनौती, जिसे "एम्बेडिंग गैप" (embedding gap) कहा जाता है, SMT-LIB और VNN-LIB के बीच मौलिक अंतरों से उत्पन्न होती है:

• चर प्रतिबंध (Variable Restrictions): VNN-LIB प्रश्नों को केवल नेटवर्क के प्रत्यक्ष इनपुट और आउटपुट का प्रतिनिधित्व करने वाले एक निश्चित, परिमित चर सेट तक सीमित रखता है। यह उपयोगकर्ता-परिभाषित तर्क के लिए मनमाने मध्यवर्ती चर (intermediate variables) पेश नहीं कर सकता।
• रूपांतरण जटिलता (Transformation Complexity): उच्च-स्तरीय विनिर्देशों में अक्सर उपयोगकर्ता चर शामिल होते हैं (जैसे, सामान्यीकृत इनपुट, क्वांटिफाइड टेंसर) जिन्हें नेटवर्क चरों में गणितीय रूप से रूपांतरित किया जाना चाहिए। SMT-LIB में, एक कंपाइलर आसानी से नए चर घोषित कर सकता है। VNN-LIB में, कंपाइलर को उपयोगकर्ता चरों को नेटवर्क चरों के रूप में व्यक्त करने के लिए (जैसे, $a_0$ के लिए $x_0 = a_0 + a_1$ को हल करना) समवर्ती समीकरणों को हल करना होगा।
• स्केलेबिलिटी (Scalability): सहज चर उन्मूलन (जैसे, गॉसियन एलिमिनेशन) $O(n^3)$ है और बड़े टेंसरों (जैसे, $n=784$ के साथ MNIST इनपुट) के लिए अव्यवहार्य हो जाता है।
• अभिव्यक्ति सीमाएँ (Expressivity Limitations): मौजूदा उच्च-स्तरीय उपकरण (जैसे, DNNV, CAISAR) उपयोगकर्ताओं को टेम्पलेट्स या तर्क के उपसमुच्चयों तक सीमित रखकर इन जटिलताओं से बचते हैं, जिससे डेटा नॉर्मलाइजेशन, फर्स्ट-क्लास क्वांटिफायर, या कई नेटवर्क अनुप्रयोगों से जुड़े गुणों को व्यक्त करने में बाधा आती है।

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

लेखक एक नवीन संकलन एल्गोरिदम प्रस्तुत करते हैं जो एक उच्च-स्तरीय विनिर्देश भाषा (फर्स्ट-ऑर्डर लॉजिक का एक अंश जो टेंसरों के साथ विस्तारित है) को अनुकूलित VNN-LIB प्रश्नों के एक वृक्ष (tree) में अनुवादित करता है। इस प्रक्रिया में तीन मुख्य चरण शामिल हैं:

A. स्रोत और लक्ष्य भाषाएँ (Source and Target Languages)

• स्रोत भाषा (Source Language): यह क्वांटिफायर (exists, forall), टेंसर संचालन (स्टैकिंग, इंडेक्सिंग, अंकगणित), और नेटवर्क अनुप्रयोगों का समर्थन करती है। यह नेटवर्क में प्रवेश करने से पहले उपयोगकर्ता चरों को रूपांतरित करने की अनुमति देती है।
• लक्ष्य भाषा (Target Language): VNN-LIB 2.0, जिसमें नेटवर्क घोषणाएं और केवल नेटवर्क इनपुट/आउटपुट पर अभिकथन (assertions) शामिल हैं। कंपाइलर जटिल तार्किक संरचनाओं को संभालने के लिए प्रश्नों का एक वृक्ष (conjunctions/disjunctions) आउटपुट करता है।

B. मध्यवर्ती भाषा और संकलन प्रवाह (Intermediate Language and Compilation Flow)

संकलन, चर उन्मूलन को अनुकूलित करने के लिए प्रोटो-क्वेरीज़ (proto-queries) (निहित रूप से विसंयुक्त बाधाओं की सूची) की एक मध्यवर्ती भाषा के माध्यम से आगे बढ़ता है।

1. क्वांटिफायर उन्मूलन (Quantifier Elimination):
   • exists क्वांटिफायर को प्रोटो-क्वेरीज़ में बॉडी को संकलित करके और फिर उपयोगकर्ता चर को हटाकर समाप्त किया जाता है।
   • forall क्वांटिफायर को बॉडी को नकार कर (De Morgan's laws) exists में परिवर्तित किया जाता है।
   • प्रतिबंध: एल्गोरिदम वैकल्पिक क्वांटिफायर (जैसे, $\exists \forall$) का समर्थन नहीं करता है, क्योंकि वर्तमान सॉल्वर केवल संतुष्टि (satisfiability) को संभालते हैं।
2. चर उन्मूलन (Variable Elimination - Algorithm 7):
   • कंपाइलर एक अमूर्त बीजीय सॉल्वर (algebraic solver) (जैसे, लीनियर अंकगणित सॉल्वर) का उपयोग करके उपयोगकर्ता चरों के लिए समाधान खोजने का प्रयास करता है।
   • अनुकूलन 1 (प्रत्यक्ष प्रतिस्थापन - Direct Substitution): यदि सॉल्वर एक समानता पाता है (जैसे, $u = x_1$), तो यह उपयोगकर्ता चर को सीधे प्रतिस्थापित करता है, जिससे तत्व-वार विस्तार (element-wise expansion) से बचा जा सके।
   • अनुकूलन 2 (पदानुक्रमित अपघटन - Hierarchical Decomposition): यदि प्रत्यक्ष समाधान विफल रहता है, तो एल्गोरिदम गहराई-प्रथम (depth-first) तरीके से चाइल्ड चरों (टेंसर तत्वों) को पुनरावर्ती रूप से समाप्त करता है। यह उन सामान्य मामलों में $O(n^3)$ के विस्फोट को रोकता है जहाँ बाधाएं स्पार्स (sparse) हैं या उच्च टेंसर स्तरों पर हल करने योग्य हैं।
3. नेटवर्क अनुप्रयोग अनुकूलन (Network Application Optimization - Algorithm 9):
   • कंपाइलर अनावश्यक नेटवर्क अनुप्रयोगों का पता लगाता है। यदि एक ही नेटवर्क के दो अनुप्रयोगों के इनपुट प्रमाणित रूप से समान हैं (विनिर्देश में समानता बाधाओं से प्राप्त), तो उन्हें एक एकल अनुप्रयोग में विलय कर दिया जाता है।
   • यह समानता बाधाओं द्वारा प्रेरित टेंसर इंडेक्स के पदानुक्रम पर तुल्यता वर्गों (equivalence classes) की गणना करके प्राप्त किया जाता है।

C. शुद्धता (Soundness)

एल्गोरिदम संख्यात्मक रूप से शुद्ध (numerically sound) है। यह अंतर्निहित बीजीय सॉल्वर की शुद्धता पर निर्भर करता है। यदि सॉल्वर संख्यात्मक डोमेन (जैसे, Reals या Floats) को सही ढंग से संभालता है, तो संकलन मूल विनिर्देश के अर्थ (semantics) को सुरक्षित रखता है।

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

1. पहला सामान्य-उद्देश्य वाला कंपाइलर: उच्च-स्तरीय FOL विनिर्देशों को VNN-LIB प्रश्नों में संकलित करने में सक्षम पहला एल्गोरिदम।
2. वर्धित अभिव्यक्ति (Enhanced Expressivity): समर्थित भाषा खंड में ऐसी विशेषताएं शामिल हैं जो पहले न्यूरल नेटवर्क विनिर्देश उपकरणों में उपलब्ध नहीं थीं:
   • नेटवर्क इनपुट से पहले उपयोगकर्ता चरों का मुक्त रूपांतरण।
   • फर्स्ट-क्लास क्वांटिफायर।
   • कई नेटवर्कों के मनमाने नेस्टेड अनुप्रयोग (हाइपर-प्रॉपर्टीज जैसे कि मोनोटोनिसिटी या टीचर-स्टूडेंट डिस्टिलेशन का समर्थन करना)।
   • गैर-रेखीय बाधाएं (सॉल्वर पर निर्भर)।
3. अनंत रूप से इष्टतम प्रदर्शन (Asymptotically Optimal Performance): एल्गोरिदम सामान्य विनिर्देशों के लिए इनपुट टेंसरों के आकार के सापेक्ष रैखिक समय जटिलता प्राप्त करता है, जो सहज दृष्टिकोणों के घातीय विस्फोट (exponential blow-up) से बचता है।
4. कार्यान्वयन: एल्गोरिदम को Vehicle फ्रेमवर्क के भीतर लागू किया गया है और यह ओपन-सोर्स है।

4. परिणाम और प्रदर्शन मूल्यांकन (Results and Performance Evaluation)

लेखकों ने तीन बेंचमार्क श्रेणियों पर अपने कंपाइलर का मूल्यांकन किया:

• ACAS Xu: विमान टक्कर बचाव के लिए एक बड़ा, व्याख्या योग्य विनिर्देश।
• Robustness: मानक $\epsilon$-बॉल मजबूती गुण।
• Monotonicity: कई नेटवर्क अनुप्रयोगों से जुड़े गुण।

मुख्य निष्कर्ष:

• रैखिक स्केलिंग (Linear Scaling): मजबूती और मोनोटोनिसिटी विनिर्देशों के लिए संकलन समय इनपुट तत्वों की संख्या के साथ रैखिक रूप से स्केल होता है। यह अनुकूलतम है क्योंकि आउटपुट क्वेरी में एसेर्शन की संख्या भी रैखिक है।
• गति (Speed): पूरा ACAS Xu विनिर्देश (10 गुण) 0.47 सेकंड में 42 क्वेरी में संकलित हुआ।
• एब्लेशन अध्ययन (Ablation Study): पदानुक्रमित अनुकूलन को हटाने (तत्व-वार समाधान के लिए मजबूर करना) से संकलन समय छोटे नेटवर्कों के लिए भी अव्यवहार्य हो गया, जो प्रस्तावित एल्गोरिदम की आवश्यकता को प्रमाणित करता है।

5. महत्व (Significance)

यह कार्य न्यूरल नेटवर्क सत्यापन में मानव-पठनीय इरादे (intent) और सॉल्वर-स्तर के एनकोडिंग के बीच के महत्वपूर्ण अंतर को पाटता है।

• सुलभता (Accessibility): यह गैर-विशेषज्ञों के लिए बाधा को कम करता है, जिससे उन्हें "एम्बेडिंग गैप" को मैन्युअल रूप से प्रबंधित किए बिना सटीक, सॉल्वर-स्वतंत्र विनिर्देश लिखने की अनुमति मिलती है।
• वास्तविक दुनिया की प्रयोज्यता (Real-World Applicability): डेटा नॉर्मलाइजेशन को विनिर्देश का हिस्सा बनाने की अनुमति देकर, उपयोगकर्ता वास्तविक दुनिया की इकाइयों (जैसे, मीटर/सेकंड, रेडियन) में बाधाएं लिख सकते हैं, न कि केवल सामान्यीकृत टेंसर मानों में।
• इंजीनियरिंग अनुशासन (Engineering Discipline): यह न्यूरल नेटवर्क सत्यापन को एक विशिष्ट अनुसंधान क्षेत्र से एक स्केलेबल इंजीनियरिंग अनुशासन की ओर ले जाता है, जैसा कि पारंपरिक सॉफ्टवेयर सत्यापन में मौजूद है।

संक्षेप में, यह शोध पत्र उच्च-स्तरीय तर्क को प्रतिबंधात्मक VNN-LIB प्रारूप में संकलित करने की एल्गोरिथम चुनौतियों के लिए एक मजबूत सैद्धांतिक और व्यावहारिक समाधान प्रदान करता है, जिससे न्यूरल नेटवर्क का अधिक अभिव्यंजक, कुशल और सुलभ औपचारिक सत्यापन संभव होता है।