Diversifying to Verify: When Task-Equivalent Programs Differ in Verifiability
यह शोध पत्र Diversify2Verify पेश करता है, जो एक LLM-आधारित पाइपलाइन है जो यह प्रदर्शित करती है कि कैसे विविध, कार्य-तुल्य प्रोग्राम कार्यान्वयन उत्पन्न करना स्वचालित सत्यापन सफलता दरों में महत्वपूर्ण सुधार करता है, उन वेरिएंट्स की पहचान करके जो औपचारिक प्रमाण (formal proof) के लिए अधिक अनुकूल हैं।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक ऐसा रोबोट बनाने की कोशिश कर रहे हैं जो गणित की एक पहेली को हल कर सके। आपके पास एक सुपर-स्मार्ट AI सहायक (एक लार्ज लैंग्वेज मॉडल) है जो कोड लिखने में माहिर है। आमतौर पर, हम AI से पूछते हैं: "इस पहेली को हल करने के लिए कोड लिखो," और फिर हम देखते हैं कि क्या रोबोट कुछ टेस्ट रन पास करता है। यदि वह पास हो जाता है, तो हम कहते हैं, "बहुत अच्छा!"
लेकिन फॉर्मल वेरिफिकेशन (औपचारिक सत्यापन) की दुनिया में, कुछ टेस्ट पास करना काफी नहीं है। यह एक पुल बनाने जैसा है और फिर उस पर केवल एक खिलौना कार चलाकर देखना है। वास्तव में सुरक्षित होने के लिए, आपको एक गणितीय प्रमाण (प्रूफ) चाहिए कि वह पुल किसी भी कार को, किसी भी समय, किसी भी स्थिति में थामे रखेगा। इसे ही पेपर "डिडक्टिव वेरिफिकेशन" (निगमनात्मक सत्यापन) कहता है।
समस्या क्या है? AI से ऐसा कोड लिखवाना जो न केवल सही हो बल्कि सिद्ध करने में आसान (easy to prove) भी हो, यह बेहद कठिन काम है। कभी-कभी AI एक ऐसा समाधान लिख देता है जो पूरी तरह से काम तो करता है, लेकिन वह इतना उलझा हुआ या अजीब तरह से संरचित होता है कि "प्रूफ चेकर" (एक टूल जिसे Why3 कहा जाता है) भ्रमित हो जाता है और उसे सत्यापित नहीं कर पाता।
बड़ा विचार: सिर्फ एक तरीके से कोशिश न करें
लेखक, शर्ली यू और रुबेन मार्टिन्स ने एक सरल प्रश्न पूछा: क्या होगा अगर हम केवल एक समाधान के लिए न पूछें, बल्कि एक ही समाधान के कई अलग-अलग संस्करणों के लिए पूछें?
इसे एक जिद्दी जार (डिब्बे) को खोलने की कोशिश करने जैसा समझें।
- वर्जन A: आप अपने दाहिने हाथ से ढक्कन घुमाने की कोशिश करते हैं।
- वर्जन B: आप अपने बाएं हाथ से घुमाने की कोशिश करते हैं।
- वर्जन C: आप चम्मच से ढक्कन पर थपथपाने की कोशिश करते हैं।
- वर्जन D: आप इसे गर्म पानी के नीचे चलाने की कोशिश करते हैं।
हो सकता है कि "दाहिने हाथ का घुमाव" (पहला कोड जो AI लिखता है) प्रूफ चेकर की पकड़ के लिए बहुत फिसलन भरा हो। लेकिन "बाएं हाथ का घुमाव" का आकार ऐसा हो सकता है जो चेकर के तर्क (logic) में पूरी तरह फिट बैठ जाए। पेपर इस दृष्टिकोण को Diversify2Verify कहता है। एक पूर्ण समाधान की उम्मीद करने के बजाय, वे एक ही कार्य के चार अलग-अलग "फ्लेवर" (प्रकार) तैयार करते हैं:
- एरे + इम्पैरेटिव (Array + Imperative): जैसे लोगों की एक कतार में एक-एक करके आगे बढ़ना और उनके नाम चेक करना।
- एरे + रिकर्सिव (Array + Recursive): जैसे "टेलीफोन" का खेल जहाँ आप कार्य को सहायकों की एक श्रृंखला में आगे बढ़ाते हैं।
- लिस्ट + इम्पैरेटिव (List + Imperative): जैसे इंडेक्स कार्ड के ढेर को पलटते हुए देखना।
- लिस्ट + रिकर्सिव (List + Recursive): जैसे एक रूसी नेस्टिंग डॉल (Russian nesting doll) जहाँ प्रत्येक डॉल के अंदर अगली डॉल होती है।
प्रयोग: 73 पहेलियाँ, 292 प्रयास
टीम ने एक विशेष प्लेग्राउंड बनाया जिसमें 73 अलग-अलग प्रोग्रामिंग पहेलियाँ (ज्यादातर संख्याओं, सूचियों और एरे से संबंधित) थीं। प्रत्येक पहेली के लिए, उन्होंने AI को उन चारों "फ्लेवर" को जेनरेट करने के लिए कहा। इससे उन्हें टेस्ट करने के लिए 292 अलग-अलग कोड प्रयास मिले।
उन्होंने केवल AI को कोड लिखने ही नहीं दिया; उन्होंने एक सख्त तीन-चरणीय प्रक्रिया स्थापित की:
- चरण 1 (द कॉन्ट्रैक्ट/अनुबंध): सबसे पहले, उन्होंने AI से एक "कॉन्ट्रैक्ट" (एक औपचारिक नियम पुस्तिका) लिखवाया जो यह वर्णन करे कि कोड को क्या करना चाहिए, बिना इस बात की चिंता किए कि वह इसे कैसे करेगा। उन्होंने इस नियम पुस्तिका को उदाहरणों के विरुद्ध जांचा ताकि यह सुनिश्चित हो सके कि यह समझ में आता है। एक बार नियम पुस्तिका स्वीकार हो जाने के बाद, इसे फ्रीज (स्थिर) कर दिया गया। बाद में नियमों को बदलना वर्जित था!
- चरण 2 (द कोड/कोड): इसके बाद, उन्होंने प्रत्येक चार फ्लेवर के लिए वास्तविक कोड लिखने के लिए AI का उपयोग किया, यह सुनिश्चित करते हुए कि वह कुछ बुनियादी टेस्ट रन पास करता है।
- चरण 3 (द प्रूफ/प्रमाण): अंत में, उन्होंने यह सिद्ध करने का प्रयास किया कि प्रत्येक कोड संस्करण फ्रीज किए गए कॉन्ट्रैक्ट का पालन करता है। यदि प्रमाण विफल हो जाता, तो उन्होंने AI को प्रमाण को ठीक करने के लिए एक संकेत (रिपेयर) दिया, लेकिन केवल प्रमाण के लिए, कोड या नियमों के लिए नहीं।
परिणाम: विविधता की जीत
जब उन्होंने गणनाएँ कीं, तो परिणाम कुछ इस प्रकार थे:
- "वन-शॉट" विफलता: यदि आप AI द्वारा लिखा गया पहला कोड लेते हैं और उसे सिद्ध करने की कोशिश करते हैं, तो केवल 96 में से 292 (लगभग 32.9%) सफल हुए। यह तीन में से एक से भी कम है!
- रिपेयर (सुधार) की शक्ति: जब उन्होंने AI को दो बार प्रमाण ठीक करने की कोशिश करने दी, तो संख्या बढ़कर 154 में से 292 (लगभग 52.7%) हो गई।
- विविधता की शक्ति (असली विजेता): जब उन्होंने पूरे 73 पहेलियों को देखा, तो उन्होंने पाया कि 49 पहेलियों के लिए (एक 67.1% सफलता दर), कम से कम एक संस्करण को सही सिद्ध किया जा सका।
यह मुख्य निष्कर्ष है: कार्य-तुल्य कार्यान्वयन (Task-equivalent implementations) सत्यापन योग्यता (verifiability) के मामले में काफी भिन्न हो सकते हैं। दूसरे शब्दों में, दो कोड जो बिल्कुल एक ही काम करते हैं, उनके सिद्ध होने की सुगमता में जमीन-आसमान का अंतर हो सकता है।
जो उन्होंने खारिज किया (यह क्या नहीं है)
पेपर बहुत सावधानी से स्पष्ट करता है कि वह क्या दावा नहीं करता है:
- यह बेहतर कोड के बारे में नहीं है: उन्होंने यह नहीं पाया कि "एरे लिस्ट से बेहतर हैं" या "रिकर्सन लूप्स से बेहतर है।" वास्तव में, परिणाम मिले-जुले थे। रिकर्सिव कोड को इम्पैरेटिव (लूप-आधारित) कोड की तुलना में सिद्ध करना आम तौर पर आसान था, लेकिन कुल मिलाकर एरे और लिस्ट का प्रदर्शन समान रहा। मुख्य बात सबसे अच्छा स्टाइल चुनना नहीं थी; बल्कि विकल्प (options) होना था।
- यह नियमों को बदलने के बारे में नहीं है: उन्होंने सुधार चरण के दौरान AI को "कॉन्ट्रैक्ट" (लक्ष्य) बदलने से सख्ती से रोका। यदि AI ने प्रमाण को आसान बनाने के लिए लक्ष्य बदलने की कोशिश की, तो उसे विफलता माना गया। वे मूल लक्ष्य को सिद्ध करना चाहते थे, न कि किसी कमजोर लक्ष्य को।
- यह हर चीज़ के लिए जादुई समाधान नहीं है: अध्ययन में केवल पूर्णांक (integers), एरे और लिस्ट से जुड़ी पहेलियों को देखा गया। वे यह दावा नहीं करते कि यह फ्लोटिंग-पॉइंट नंबरों, जटिल 3D ग्राफिक्स या इंटरनेट से बात करने वाले प्रोग्रामों के लिए भी काम करेगा।
वे कितने आश्वस्त हैं?
लेखक अपने मापन को लेकर आश्वस्त हैं लेकिन बड़े चित्र को लेकर सतर्क हैं।
- मापा गया: उनके पास ठोस आंकड़े हैं। उन्होंने टूल्स चलाए, सफलताओं को गिना और देखा कि विविधता ने व्यक्तिगत आर्टिफ़ैक्ट्स के लिए सफलता दर को 32.9% से बढ़ाकर 52.7% और कार्यों के लिए 67.1% कर दिया।
- सुझाया गया: वे सुझाव देते हैं कि इम्पैरेटिव कोड (लूप्स) को सिद्ध करना कठिन क्यों था, क्योंकि इसके लिए "लूप इनवेरिएंट्स" (लूप के अंदर क्या हो रहा है इसके नियम) की आवश्यकता होती है, जिन्हें स्वचालित रूप से आविष्कार करना AI के लिए कठिन है। उन्हें संदेह है कि यदि वे AI को इन नियमों का अनुमान लगाने के लिए बेहतर उपकरण देते हैं, तो यह अंतर कम हो सकता है।
- अभी सिद्ध नहीं हुआ (अभी तक): उन्होंने स्वीकार किया कि उन्होंने यह सिद्ध नहीं किया कि "एरे कॉन्ट्रैक्ट" और "लिस्ट कॉन्ट्रैक्ट" गणितीय रूप से समान हैं। उन्होंने बस यह मान लिया कि वे कार्य विवरण के आधार पर एक ही अर्थ रखते हैं। उन्होंने यह भी नोट किया कि उनका "जज" (एक AI जो नियमों की जाँच करता है कि क्या वे पहेली से मेल खाते हैं) कोई पूर्ण मानव विशेषज्ञ नहीं है, इसलिए कुछ सूक्ष्म गलतियाँ निकल सकती हैं।
मुख्य सीख (Takeaway)
पेपर सुझाव देता है कि जब हम AI से "सत्यापित" (verified) सॉफ्टवेयर लिखने के लिए कहते हैं, तो हमें केवल एक उत्तर की उम्मीद नहीं करनी चाहिए और भाग्य के भरोसे नहीं रहना चाहिए। इसके बजाय, हमें एक विकल्पों का मेनू मांगना चाहिए। एक ही समस्या को हल करने के विभिन्न तरीकों को उत्पन्न करके, हम अपनी सफलता की संभावना को बढ़ाते हैं, जिससे हमें वह संस्करण मिल सके जिसे प्रूफ चेकर वास्तव में समझ सके।
यह एक ताले में फिट होने वाली चाबी खोजने जैसा है। यदि आपके पास केवल एक चाबी है, तो आप फंस सकते हैं। लेकिन यदि आपके पास चाबियों का एक पूरा छल्ला है, भले ही वे सभी एक ही दरवाजे को खोलते हों, तो उनमें से एक के ताले में पूरी तरह फिट होने की संभावना लगभग निश्चित है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।