Testing Deep Learning Libraries via Neurosymbolic Constraint Learning
यह शोध पत्र सेंटॉर (Centaur) प्रस्तुत करता है, जो एक नवीन न्यूरोसिम्बोलिक तकनीक है जो सीड इनपुट्स से औपचारिक API बाधाओं (constraints) को सीखने के लिए लार्ज लैंग्वेज मॉडल्स और SMT सॉल्वर्स का उपयोग करती है ताकि डीप लर्निंग लाइब्रेरीज़ के लिए वैध और विविध टेस्ट केस उत्पन्न किए जा सकें, जिससे मौजूदा विधियों की तुलना में बग डिटेक्शन और कोड कवरेज में महत्वपूर्ण सुधार होता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक रोबोट को एक बहुत ही जटिल केक बनाना सिखाने की कोशिश कर रहे हैं, जिसके लिए एक नई, रहस्यमयी रेसिपी बुक का उपयोग करना है। वह किताब (डीप लर्निंग लाइब्रेरी) बहुत बड़ी है, लेकिन निर्देश अस्पष्ट हैं। इसमें लिखा है जैसे "मैदा डालें," लेकिन यह नहीं बताता कि कितनी चीनी के साथ कितना मैदा डालना चाहिए, या क्या होगा यदि आप एक बहुत छोटे चम्मच से ढेर सारा बैटर मिलाने की कोशिश करते हैं। यदि आप गलत अनुमान लगाते हैं, तो रोबोट रसोई में तबाही मचा सकता है, या इससे भी बुरा, ऐसा केक बना सकता है जो दिखने में तो ठीक हो लेकिन स्वाद में बहुत खराब हो।
यह बिल्कुल वही समस्या है जिसका सामना शोधकर्ताओं ने डीप लर्निंग लाइब्रेरीज़ (जैसे PyTorch और TensorFlow) के साथ किया था। ये वे "रेसिपी बुक्स" हैं जो आधुनिक AI को शक्ति प्रदान करती हैं। ये शक्तिशाली हैं लेकिन छिपे हुए खतरों (बग्स) से भरी हुई हैं। समस्या यह है कि इन लाइब्रेरीज़ के मैनुअल अक्सर अधूरे, बिखरे हुए या भ्रमित करने वाली भाषा में लिखे होते हैं।
यहाँ आता है Centaur, एक नया टूल जिसे इन लाइब्रेरीज़ का परीक्षण करने के लिए शोधकर्ताओं द्वारा विकसित किया गया है। Centaur को एक सुपर-स्मार्ट जासूस के रूपas सोचें जो सोचने के दो अलग-अलग तरीकों को जोड़ता है: एक इंसान की रचनात्मक अंतर्दृष्टि और एक कंप्यूटर का सख्त तर्क।
Centaur के दो मस्तिष्क
Centaur "न्यूरोसिम्बोलिक" (neurosymbolic) है, जिसका एक फैंसी अर्थ यह है कि इसमें दो मस्तिष्क मिलकर काम कर रहे हैं:
"न्यूरल" मस्तिष्क (रचनात्मक जासूस): यह हिस्सा एक लार्ज लैंग्वेज मॉडल (LLM) का उपयोग करता है। इसे एक बहुत ही जानकार शेफ के रूप में समझें जिसने लाखों कुकिंग ब्लॉग और रेसिपी बुक्स पढ़ी हैं। जब Centaur किसी विशिष्ट फंक्शन (जैसे "दो संख्याओं को जोड़ना") को देखता है, तो LLM अपने ज्ञान का उपयोग करके नियमों का अनुमान लगाता है। "हे," LLM कह सकता है, "आमतौर पर, यदि आप दो सूचियों (lists) को जोड़ते हैं, तो उन्हें एक ही आकार का होना चाहिए, या उनमें से एक केवल एक एकल संख्या होनी चाहिए जिसे कॉपी किया जा सके।"
- कमी: LLM रचनात्मक है लेकिन गलतियाँ कर सकता है। यह एक ऐसा नियम अनुमानित कर सकता है जो सुनने में तो अच्छा लगता है लेकिन वास्तव में सच नहीं होता।
"सिम्बोलिक" मस्तिष्क (सख्त गणित का प्रोफेसर): यह हिस्सा एक SMT सॉल्वर (एक प्रकार का लॉजिक इंजन) का उपयोग करता है। इसे एक सख्त गणित के शिक्षक के रूप में समझें जो शेफ द्वारा किए गए हर अनुमान की जाँच करता है। यदि शेफ कहता है, "आप 5 कप मैदा और 2 कप चीनी मिला सकते हैं," तो गणित का प्रोफेसर यह गणना करके देखता है कि क्या यह भौतिकी के नियमों (या इस मामले में, सॉफ्टवेयर के नियमों) को तोड़े बिना वास्तव में काम करता है।
- शक्ति: गणित का प्रोफेसर केवल "हाँ" या "नहीं" नहीं कहता। यह हजारों विशिष्ट, वैध उदाहरण (जैसे "3 कप मैदा, 1 कप चीनी") उत्पन्न कर सकता है जो यह सिद्ध करते हैं कि नियम काम करता है।
Centaur कैसे काम करता है (रेसिपी)
यहाँ वह स्टेप-बाय-स्टेप प्रक्रिया दी गई है जिसका उपयोग Centaur करता है, जिसे सरल रूप में समझाया गया है:
चरण 1: अनुमान लगाने का खेल (नियम पीढ़ी - Rule Generation)
Centaur "शेफ" (LLM) से पूछता है कि किसी विशिष्ट फंक्शन को कैसे काम करना चाहिए, इसके नियम लिखे। शेफ को अनियंत्रित होने से रोकने के लिए, Centaur उसे एक विशेष टेम्पलेट (व्याकरण) देता है जो उसे नियमों को एक विशिष्ट, तार्किक प्रारूप में लिखने के लिए मजबूर करता है। शेफ अनुमान लगा सकता है, "दोनों टेन्सर्स (tensors) का आकार समान होना चाहिए।"
चरण 2: तथ्य-जाँच (प्रतिबंध सीखना - Constraint Learning)
इसके बाद Centaur इन अनुमानों को ज्ञात "अच्छे" इनपुट्स (वैध डेटा) के एक सेट के विरुद्ध परीक्षण करता है।
- यदि नियम सभी अच्छे इनपुट्स के लिए सही रहता है, तो Centamer उसे रखता है।
- यदि नियम विफल हो जाता है, तो वह उसे बाहर निकाल देता है।
- सुधार (Refinement): कभी-कभी, शेफ दो ऐसे नियम अनुमानित करता है जिनका अर्थ बिल्कुल एक ही होता है। Centaur के पास इन डुप्लिकेट्स को पहचानने और अतिरिक्त नियमों को हटाने का एक विशेष तरीका है, ताकि वह भ्रमित न हो।
चरण 3: बड़े पैमाने पर उत्पादन (फज़िंग - Fuzzing)
अब जब Centaur के पास सत्यापित नियमों की एक सूची है, तो वह "गणित के प्रोफेसर" (SMT Solver) का उपयोग करके लाखों नए टेस्ट केस बनाता है। क्योंकि नियम गणितीय रूप से सिद्ध हैं, Centaur जानता है कि उसके द्वारा बनाया गया लगभग हर इनपुट वैध होगा। यह एक ऐसी मशीन की तरह है जो केवल परफेक्ट केक बैटर बनाती है, कभी भी जला हुआ या कच्चा बैटर नहीं बनाती।
चरण 4: क्रैश टेस्ट
Centaur इन लाखों परफेक्ट इनपुट्स को डीप लर्निंग लाइब्रेरी में डालता है। यदि लाइब्रेरी क्रैश होती है, फ्रीज होती है, या कोई अजीब उत्तर देती है, तो Centaur उसे बग के रूप में चिह्नित करता है।
यह एक बड़ी बात क्यों है?
पिछले टूल्स ने दो तरीकों से बग्स खोजने की कोशिश की:
- "रैंडम थ्रोअर" (Random Thrower): उन्होंने लाइब्रेरी पर रैंडम डेटा फेंका। यह आँखों पर पट्टी बांधकर डार्ट फेंकने जैसा है। अधिकांश डार्ट बोर्ड को मिस कर जाते हैं (अवैध इनपुट), जिससे उनका बहुत समय बर्बाद होता है।
- "कोड रीडर" (Code Reader): उन्होंने लाइब्रेरी के सोर्स कोड को पढ़ने की कोशिश की ताकि नियमों को समझा जा सके। यह घर के निर्माण के दौरान उसके ब्लूप्रिंट को पढ़ने जैसा है। यह धीमा है, और यदि ब्लूप्रिंट अस्त-व्यस्त है, तो वे खो जाते हैं।
Centaur अलग है। यह लाइब्रेरी के व्यवहार को देखकर (LLM का उपयोग करके) नियमों को सीखता है और फिर उन नियमों को सत्यापित करने के लिए गणित का उपयोग करके परफेक्ट टेस्ट केस बनाता है।
परिणाम (जो पेपर दावा करता है)
शोधकर्ताओं ने PyTorch और TensorFlow पर Centaur का परीक्षण किया, जो दो सबसे लोकप्रिय AI लाइब्रेरीज़ हैं। उन्हें यहाँ क्या मिला:
- सटीकता (Accuracy): Centaur के नियम 94% सटीक थे। इसने शायद ही कभी गलत अनुमान लगाया, और इसने वास्तव में मौजूद किसी भी नियम को मिस नहीं किया।
- दक्षता (Efficiency): जबकि अन्य टूल्स ज्यादातर अमान्य इनपुट उत्पन्न करते थे (जो बेकार होते हैं), Centaur ने 98% वैध इनपुट उत्पन्न किए। इसका मतलब है कि इसने अपना लगभग सारा समय वास्तविक परिदृश्यों के परीक्षण में बिताया, न कि असंभव चीजों पर बर्बाद किया।
- कवरेज (Coverage): Centaur ने पिछले बेहतरीन टूल्स की तुलना में कोड के अधिक हिस्सों की जांच की। इसने "डीप" बग्स पाए—सॉफ्टवेयर के मूल तर्क (core logic) में समस्याएं—न कि केवल सतह के स्तर की त्रुटियां।
- बग हंटिंग (Bug Hunting): Centaur का उपयोग करके, टीम ने इन लाइब्रेरीज़ में 26 नए बग खोजे। इनमें से 18 की डेवलपर्स द्वारा पुष्टि की गई थी। इनमें से एक को तो पेपर प्रकाशित होने से पहले ही ठीक भी कर दिया गया था!
"डीप बग्स" के लिए एक सरल उपमा
एक पुल की कल्पना करें।
- शैलो बग्स (Shallow bugs) सड़क के किनारे के गड्ढों की तरह हैं। इन्हें देखना और ठीक करना आसान है।
- डीप बग्स (Deep bugs) मुख्य सपोर्ट बीम में दरार की तरह हैं। आप इसे बाहर से नहीं देख सकते, लेकिन यदि एक भारी ट्रक इसके ऊपर से गुजरता है, तो पूरा पुल ढह सकता है।
पिछले टूल्स ने ज्यादातर गड्ढे ही ढूंढे। Centaur ने, पुल कैसे बनाया गया है इसके जटिल नियमों को समझकर, सपोर्ट बीम में दरारें खोजने में सफलता प्राप्त की।
सारांश
Centaur एक नया टेस्टिंग टूल है जो डीप लर्निंग लाइब्रेरीज़ के नियमों का अनुमान लगाने के लिए एक रचनात्मक AI का उपयोग करता है और फिर उन नियमों को सत्यापित करने और लाखों परफेक्ट टेस्ट केस बनाने के लिए एक तार्किक गणित इंजन का उपयोग करता है। यह संयोजन इसे उन छिपे हुए, खतरनाक बग्स को खोजने की अनुमति देता है जिन्हें अन्य टूल्स मिस कर देते हैं, जिससे हमारे द्वारा उपयोग किए जाने वाले AI सिस्टम अधिक सुरक्षित और विश्वसनीय बनते हैं।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।