Neuro-Symbolic Software Verification: Hyper-charging Local Language Models with Symbolic Reasoning at Scale
यह शोध पत्र VerIbmc को प्रस्तुत करता है, जो एक न्यूरो-सिंबोलिक पाइपलाइन है जो सॉफ्टवेयर सत्यापन के लिए अत्याधुनिक लूप इनवेरिएंट जनरेशन प्राप्त करने हेतु सिंबोलिक इनवेरिएंट सिंथेसिस और इटरेटिव वेरीफायर फीडबैक के साथ स्थानीय ओपन-वेट लैंग्वेज मॉडल्स का लाभ उठाता है, जो मालिकाना क्लाउड-आधारित उपकरणों के लिए एक गोपनीयता-संरक्षित और लागत प्रभावी विकल्प प्रदान करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप यह सिद्ध करने की कोशिश कर रहे हैं कि एक जटिल मशीन (एक कंप्यूटर प्रोग्राम) कभी खराब नहीं होगी, चाहे उसे कितनी भी बार चलाया जाए। इस प्रमाण का सबसे कठिन हिस्सा मशीन के "लूप्स" (loops) को समझना है—वे हिस्से जहाँ मशीन एक कार्य को बार-बार दोहराती है। इस मशीन को सुरक्षित सिद्ध करने के लिए, आपको एक लूप इनवेरिएंट (Loop Invariant) खोजना होगा।
एक लूप इनवेरिएंट को ऐसे समझें जैसे कि एक "सुरक्षा नियम" जो हर बार यह सुनिश्चित करता है कि जब मशीन अपने लूप का एक नया चक्र शुरू करे, तो वह सच हो। उदाहरण के लिए, यदि एक लूप 10 से 0 तक गिनती नीचे की ओर करता है, तो सुरक्षा नियम यह हो सकता है: "संख्या हमेशा 0 और 10 के बीच रहती है।" यदि आप यह सिद्ध कर सकते हैं कि यह नियम शुरुआत में सच है, हर कदम के बाद सच रहता है, और एक सुरक्षित अंत की ओर ले जाता है, तो पूरी मशीन को सुरक्षित सिद्ध कर दिया जाता है।
समस्या यह है कि इन नियमों को स्वचालित रूप से खोजना अविश्वसनीय रूप से कठिन है। यह बिना किसी सुराग के तिजोरी का गुप्त संयोजन (combination) अनुमान लगाने जैसा है।
पुराना तरीका बनाम नया तरीका
पुराना तरीका (सिंबोलिक रीजनिंग - Symbolic Reasoning):
पारंपरिक रूप से, कंप्यूटर सख्त गणित और तर्क का उपयोग करके इन नियमों को खोजने की कोशिश करते थे। यह एक अत्यंत सटीक मुनीम की तरह है जो हर एक संख्या की जाँच करता है। यह बहुत विश्वसनीय है, लेकिन जटिल और उलझे हुए कार्यों में अक्सर अटक जाता है। यह एक भूलभुलैया को हर एक दीवार को एक-एक करके जाँचते हुए हल करने जैसा है।
"क्लाउड" का तरीका (बड़े AI मॉडल):
हाल ही में, लोगों ने इन नियमों का अनुमान लगाने के लिए विशाल आर्टिफिशियल इंटेलिजेंस (AI) मॉडल का उपयोग करना शुरू कर दिया है। ये AI एक प्रतिभाशाली, विद्वान छात्र की तरह हैं जिन्होंने लाखों कोड उदाहरण पढ़े हैं। वे बहुत तेज़ी से सही नियम का अनुमान लगा सकते हैं। हालाँकि, इनका उपयोग करने के लिए, आपको आमतौर पर अपना कोड एक विशाल, महंगे क्लाउड सर्वर पर भेजना पड़ता है (जैसे अपने गुप्त ब्लूप्रिंट किसी अजनबी को भेजना)। यह उन कंपनियों के लिए बुरा है जिन्हें अपने कोड की गोपनीयता बनाए रखने की आवश्यकता है, और इसमें बहुत पैसा खर्च होता है।
समाधान: VerIbmc (स्थानीय "सुपर-हेल्पर")
इस शोध पत्र के लेखकों ने VerIbmc नामक एक नया सिस्टम बनाया है। इसे एक स्थानीय वर्कशॉप के रूप में समझें जहाँ आप बिना अपनी इमारत छोड़े एक स्मार्ट AI सहायक का उपयोग कर सकते हैं।
VerIbmc कैसे काम करता है, इसके लिए एक सरल उपमा यहाँ दी गई है:
कल्पना कीजिए कि आप एक कठिन पहेली (लूप इनवेरिएंट) को हल करने की कोशिश कर रहे हैं।
- निश्चित जासूस (The Deterministic Detective - चरण 0 और 1): AI से मदद माँगने से पहले, VerIbmc एक सख्त, तार्किक जासूस (एक टूल जिसे ESBMC कहा जाता है) को पहेली को देखने के लिए भेजता है। जासूस पहले सरल तथ्यों की जाँच करता है। यदि पहेली आसान है, तो जासूस इसे तुरंत हल कर देता है। यदि जासूस को कुछ ठोस सुराग मिलते हैं (जैसे "संख्या हमेशा सकारात्मक रहती है"), तो वह उन्हें एक व्हाइटबोर्ड पर लिख देता है।
- स्थानीय AI सहायक (The Local AI Assistant - चरण 2): यदि जासूस अटक जाता है, तो वह स्थानीय AI सहायक को बुलाता है। लेकिन यहाँ एक तरकीब है: AI शून्य से शुरुआत नहीं करता है। जासूस AI को वे सुरागों वाला व्हाइटबोर्ड सौंप देता है जो उसने पहले से खोज लिए हैं।
- फीडबैक लूप (The Feedback Loop): AI एक पूर्ण समाधान का अनुमान लगाता है। जासूस उसकी जाँच करता है।
- यदि वह गलत है, तो जासूस केवल "नहीं" नहीं कहता। वह कहता है, "यह हिस्सा गलत है, लेकिन यह दूसरा हिस्सा वास्तव में सही है।" वह सही हिस्से को लेता है, उसे व्हाइटबोर्ड पर लिखता है, और AI को फिर से प्रयास करने के लिए कहता है, जिसमें नए सुरागों का उपयोग किया गया हो।
- यह तब तक बार-बार होता रहता है जब तक कि पहेली हल नहीं हो जाती या समय समाप्त नहीं हो जाता।
सोचने के दो तरीके (CoT बनाम ToT)
पेपर में यह भी परीक्षण किया गया कि पहेली सुलझाते समय AI को कैसे "सोचना" चाहिए:
- चेन-ऑफ-थॉट (Chain-of-Thought - CoT): AI एक सीधी रेखा में, चरण-दर-चरण सोचता है, जैसे एक एकल कहानी लिखना।
- ट्री-ऑफ-थॉट्स (Tree-of-Thoughts - ToT): AI एक पेड़ की तरह शाखाओं में फैलता है। वह एक साथ कई अलग-अलग रास्तों को आजमाता है, देखता है कि कौन सा रास्ता आशाजनक लग रहा है, और फिर अपनी पूरी ऊर्जा सबसे अच्छे रास्तों पर केंद्रित करता है। शोध में पाया गया कि सबसे मजबूत AI मॉडल के लिए, यह शाखाओं वाला तरीका बहुत अच्छा था, लेकिन छोटे, कमजोर मॉडलों के लिए, यह कभी-कभी समय बर्बाद करता था।
परिणाम: यह क्यों मायने रखता है
शोधकर्ताओं ने सैकड़ों अलग-अलग प्रोग्रामिंग पहेलियों पर इस सिस्टम का परीक्षण करने के लिए पाँच अलग-अलग "ओपन-वेट" (open-weight) AI मॉडलों का उपयोग किया (ऐसे मॉडल जिन्हें कोई भी डाउनलोड कर सकता है और अपने स्वयं के कंप्यूटर पर चला सकता है)।
- प्राथमिकता गोपनीयता (Privacy First): क्योंकि सब कुछ एक स्थानीय मशीन पर चलता है, इसलिए कोई भी कोड संगठन से बाहर नहीं जाता है। यह अपने कमरे में गणित का होमवर्क करने जैसा है, न कि किसी अजनबी को हाथ में देने जैसा।
- लागत प्रभावी (Cost Effective): आपको बड़ी क्लाउड कंपनियों को महंगी फीस देने की आवश्यकता नहीं है।
- प्रदर्शन (Performance): सबसे अच्छा सेटअप (एक बड़े स्थानीय मॉडल GPT-OSS-120B का उपयोग करके) ने 86.4% समस्याओं को हल किया। यह कई पारंपरिक उपकरणों से बेहतर है और महंगे क्लाउड-आधारित AI उपकरणों के प्रतिस्पर्धी है।
- "मुफ्त" का लाभ (The "Free" Boost): सिस्टम ने पाया कि "डिटेक्टिव" चरण (सिंबोलिक भाग) ने AI की मदद के बिना ही 75 समस्याओं को अकेले हल कर लिया। कमजोर AI मॉडल के लिए, जासूस के सुरागों ने उन्हें अकेले हल करने की तुलना में 35 अधिक समस्याएँ हल करने में मदद की।
निष्कर्ष
VerIbmc सिद्ध करता है कि सॉफ्टवेयर सुरक्षा को सत्यापित करने के लिए आपको महंगे, गोपनीयता-हनन करने वाले क्लाउड सुपरकंप्यूटर की आवश्यकता नहीं है। एक सख्त तार्किक जासूस और एक स्मार्ट, स्थानीय AI सहायक को मिलाने से, जो अपनी गलतियों से सीखता है, आप अपने स्वयं के कंप्यूटर पर शीर्ष-स्तरीय परिणाम प्राप्त कर सकते हैं। यह सॉफ्टवेयर सत्यापन को निजी, किफायती और शक्तिशाली बनाने का एक तरीका है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।