P: Joint Program-and-Proof Planning for Verified Code Generation
यह शोध पत्र को प्रस्तुत करता है, जो एक LLM-आधारित एजेंटिक वर्कफ़्लो है जो क्रमिक पीढ़ी (sequential generation) की अक्षमताओं को दूर करने के लिए प्रोग्राम और उनके औपचारिक प्रमाणों (formal proofs) को संयुक्त रूप से नियोजित करता है, जिससे एक नए रिपॉजिटरी-व्युत्पन्न डेटासेट जिसे Lean4-Commit0 कहा जाता है, सहित सत्यापित कोड जनरेशन बेंचमार्क पर अत्याधुनिक प्रदर्शन और महत्वपूर्ण लागत कटौती प्राप्त होती है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक सुपर-स्मार्ट रोबोट को कहानी लिखना सिखा रहे हैं। आप रोबोट को एक प्रॉम्प्ट देते हैं, और वह एक कहानी निकाल कर देता है। लेकिन यहाँ एक पेच है: आप केवल एक कहानी नहीं चाहते; आप एक ऐसी कहानी चाहते हैं जो गणितीय रूप से सत्य होने की गारंटी देती हो, जिसमें कोई प्लॉट होल (कथानक की खामी) न हो, कोई ऐसा जादू न हो जो भौतिकी के नियमों को तोड़ दे, और कोई ऐसा पात्र न हो जो बिना किसी स्पष्टीकरण के गायब हो जाए। यह वेरिफाइड कोड जनरेशन (verified code generation) की दुनिया है। यह कंप्यूटर विज्ञान का वह कोना है जहाँ हम आर्टिफिशियल इंटेलिजेंस से न केवल सॉफ्टवेयर लिखने के लिए कहते हैं, बल्कि उससे ऐसा सॉफ्टवेयर लिखने की मांग करते हैं जो अपने साथ अपना स्वयं का "प्रूफ ऑफ करेक्टनेस" (सत्यता का प्रमाण) लेकर आए—एक गणितीय प्रमाण जो कहता है, "मैं वादा करता हूँ कि यह कोड ठीक वैसा ही करेगा जैसा मैंने कहा था, हर संभव स्थिति के लिए।"
लंबे समय तक, इसे करने का मानक तरीका एक दो-चरणीय नृत्य की तरह था: पहले रोबोट कोड (कहानी) लिखता है, और फिर, रोबोट-प्रूफ-रीडर्स की एक अलग टीम यह जाँचने की कोशिश करती है कि क्या कहानी समझ में आ रही है। यदि प्रूफ-रीडर्स को कोई प्लॉट होल मिलता है, तो वे कहानी को सुधारने के लिए लेखक के पास वापस भेज देते हैं। लेखक कहानी को पैच करता है, उसे वापस भेजता है, और यह चक्र चलता रहता है। लेकिन यह पेपर सुझाव देता है कि यह "लिखो-फिर-जाँचो" वाला नृत्य अक्सर अनाड़ी और अक्षम होता है। यह एक पुल बनाने और फिर, पुल पूरा होने के बाद, यह महसूस करने जैसा है कि आप सपोर्ट बीम लगाना भूल गए हैं, जिससे आपको उसे गिराकर फिर से बनाना पड़ता है। इस पेपर के लेखक एक नया तरीका प्रस्तावित करते हैं: कोड और प्रमाण को अलग-अलग लिखने के बजाय, रोबोट को एक ही समय में पूरे पुल की योजना बनानी चाहिए—सड़क और उसके सपोर्ट दोनों की—यह सुनिश्चित करते हुए कि वे पहले ही स्केच में एक साथ पूरी तरह फिट बैठें।
समस्या: "लिखो-फिर-जाँचो" का जाल
पेपर, जिसका शीर्षक "Joint Program-and-Proof Planning for Verified Code Generation" है, सत्यापित सॉफ्टवेयर लिखने के तरीके में आने वाली एक निराशाजनक बाधा को हल करता है। वर्तमान में, अधिकांश सिस्टम "प्रोग्राम-देन-प्रूफ" वर्कफ़्लो का पालन करते हैं। यह एक शेफ से एक जटिल भोजन पकाने के लिए कहने जैसा है और फिर, भोजन मेज पर आने के बाद, एक फूड क्रिटिक से यह साबित करने के लिए पूछना कि क्या सामग्री ताज़ा थी और खाना पकाने की विधि सुरक्षित थी। यदि क्रिटिक को कोई समस्या मिलती है (जैसे अधपका चिकन), तो शेफ को वापस जाकर, व्यंजन को फिर से पकाना पड़ता है और उम्मीद करनी पड़ती है कि इस बार क्रिटिक को यह पसंद आएगा।
लेखकों का तर्क है कि यह क्रमिक दृष्टिकोण त्रुटिपूर्ण है। जब AI पहले कोड लिखने के लिए प्रतिबद्ध होता है, तो वह एक ऐसी संरचना चुन सकता है जो सतह पर तो ठीक दिखती है, लेकिन उसे सिद्ध करना एक दुःस्वप्न बन जाता है। उदाहरण के लिए, कल्पना करें कि AI एक सूची में सबसे बड़ी संख्या खोजने का प्रोग्राम लिखता है। यह एक ऐसा तरीका चुन सकता है जो लिखने में छोटा और तेज़ है, लेकिन इसे सिद्ध करने के लिए एक अत्यंत जटिल, छिपे हुए गणितीय नियम की आवश्यकता होती है। एक बार कोड लिखे जाने के बाद, AI फंस जाता है: उसे या तो उस विशिष्ट कोड से मेल खाने के लिए एक बहुत कठिन प्रमाण बनाना होगा या कोड को फाड़कर फिर से शुरू करना होगा। इससे बहुत सारा समय, पैसा और "रिपेयर लूप" बर्बाद होता है जहाँ AI कोड और प्रमाण को बार-बार पैच करता रहता है, लेकिन वे कभी एक-दूसरे में फिट नहीं हो पाते।
समाधान: P3 (द "हैंड-इन-हैंड" प्लानर)
इसे ठीक करने के लिए, शोधकर्ता P3 पेश करते हैं, जो एक नया वर्कफ़्लो है जहाँ AI एक मास्टर आर्किटेक्ट की तरह कार्य करता है जो एक भी ईंट रखने से पहले भवन और सुरक्षा निरीक्षण दोनों का ब्लूप्रिंट तैयार करता है।
सीधे कोड लिखने में कूदने के बजाय, P3 पहले एक एकीकृत योजना (unified plan) बनाता है। यह योजना एक उच्च-स्तरीय स्केच है जो एक साथ दो प्रश्नों के उत्तर देता है:
- कोड कैसे काम करेगा? (एक "प्रोग्राम स्केच")
- हम इसे कैसे सिद्ध करेंगे? (एक "प्रूफ स्केच")
योजना समाधान की संरचना तय करती है। यह कोड के लिए सही "आकार" चुनती है (जैसे रिकर्सिव लूप या फोल्ड के बीच चयन करना) और साथ ही उन मिलान करने वाले गणितीय नियमों (इनवेरिएंट्स) को चुनती है जो उस आकार को सुरक्षित सिद्ध करने के लिए आवश्यक हैं। यह एक पुल बनाने का निर्णय लेने जैसा है: "हम सस्पेंशन केबल्स का उपयोग करके एक पुल बनाएंगे, इसलिए हमारी प्रूफ योजना में उन केबल्स के तनाव (tension) की जाँच करना शामिल होना चाहिए।"
एक बार यह साझा योजना लॉक हो जाने के बाद, AI विवरणों को "एलबोरेट" (विस्तारित) करता है। यह वास्तविक कोड और वास्तविक प्रमाण लिखता है, लेकिन यह केवल एक पूर्व-सहमत ब्लूप्रिंट के रिक्त स्थानों को भर रहा होता है। यदि प्रमाण विफल हो जाता है, तो AI को पता होता है कि कहाँ देखना है क्योंकि संरचना पहले ही तय की जा चुकी थी। यदि योजना ही खराब है (उदाहरण के लिए, पुल का डिज़ाइन असंभव है), तो AI को समाप्त किए गए निर्माण को पागलों की तरह पैच करने के बजाय, योजना चरण पर वापस जाकर ब्लूप्रिंट को फिर से बनाने के लिए कहा जाता है।
नया परीक्षण क्षेत्र: Lean4Commit0
लेखकों ने महसूस किया कि इन AI सिस्टमों के लिए पिछले परीक्षण बहुत आसान थे, जैसे रोबोट को टेक्स्टबुक से गणित की पहेलियाँ हल करने के लिए कहना। वास्तविक दुनिया का सॉफ्टवेयर अधिक अव्यवस्थित होता है। अपने नए तरीके का ठीक से परीक्षण करने के लिए, उन्होंने एक नया बेंचमार्क बनाया जिसे Lean4Commit0 कहा जाता है।
उन्होंने 108 वास्तविक दुनिया की ओपन-सोर्स सॉफ्टवेयर लाइब्रेरीज़ (जो Python, Rust, C/C++, और Java में लिखी गई हैं) को खंगाला और उनकी मुख्य विशेषताओं को "वेरिफाइड कोड" चुनौतियों में बदल दिया। साधारण "दो संख्याओं को जोड़ने" वाले कार्यों के बजाय, इन चुनौतियों में प्रोग्राम के विभिन्न हिस्सों के बीच जटिल संबंध शामिल हैं। उदाहरण के लिए, एक कॉन्फ़िगरेशन सिस्टम में, वे AI को यह सिद्ध करने के लिए कह सकते हैं कि "यदि आप एक सेटिंग को 'High' पर सेट करते हैं और फिर बाद में उसे 'Low' पर सेट करते हैं, तो सिस्टम सही ढंग से 'Low' सेटिंग को याद रखता है।" इन कार्यों के लिए AI को यह समझने की आवश्यकता होती है कि विभिन्न फंक्शन एक-दूसरे से कैसे बात करते हैं, जिससे ये कार्यों को टेक्स्टबुक समस्याओं की तुलना में बहुत कठिन बना देता है।
उन्होंने क्या पाया: स्मार्ट प्लानिंग जीतती है
टीम ने तीन अलग-अलग बेंचमार्क: Verina, AlgoVeri, और अपने नए Lean4Commit0 पर चार सबसे शक्तिशाली उपलब्ध AI मॉडल्स (Codex, Gemini, और Claude के संस्करणों सहित) के विरुद्ध P3 का परीक्षण किया।
परिणाम स्पष्ट थे: साथ मिलकर योजना बनाना अलग-अलग लिखने से बेहतर काम करता है।
- सफलता दर (Success Rate): P3 ने हर एक टेस्ट में अन्य सभी तरीकों की तुलना में अधिक कार्यों को हल किया। कठिन कार्यों पर, इसने मौजूदा सर्वोत्तम तरीकों की तुलना में सफलता दर में 4.6 से 11.2 प्रतिशत अंक का सुधार किया।
- दक्षता (Efficiency): यह केवल अधिक समस्याओं को हल करने के बारे में नहीं था; यह उन्हें तेज़ी से और सस्ते में हल करने के बारे में भी था। कठिन कार्यों पर, P3 ने API कॉल्स की लागत को 40% तक कम कर दिया और समय को 37% तक कम कर दिया। ऐसा इसलिए क्योंकि AI ने असंभव चीजों को सिद्ध करने या संरचनात्मक रूप से गलत कोड को फिर से लिखने में समय बर्बाद नहीं किया।
- "संयुक्त" लाभ (The "Joint" Advantage): यह साबित करने के लिए कि "संयुक्त योजना" ही असली सफलता का मंत्र था, उन्होंने एक परीक्षण चलाया जहाँ AI ने कोड की योजना बनाई लेकिन पहले से प्रमाण की योजना नहीं बनाई। इस "केवल-कोड-योजना" पद्धति ने P3 की तुलना में खराब प्रदर्शन किया, जिससे पुष्टि हुई कि कोड की योजना बनाते समय ही प्रमाण के बारे में सोचना ही अंतर पैदा करता है।
एक वास्तविक उदाहरण: रेड-ब्लैक ट्री (Red-Black Tree)
यह दिखाने के लिए कि यह व्यवहार में कैसे काम करता है, लेखकों ने कंप्यूटर विज्ञान की एक क्लासिक समस्या को देखा: एक "रेड-ब्लैक ट्री" (डेटा को कुशलतापूर्वक व्यवस्थित करने के लिए उपयोग किया जाने वाला एक जटिल डेटा स्ट्रक्चर) से एक नोड को हटाना।
- पुराना तरीका (Program-then-Proof): AI ने नोड को हटाने के एक विशिष्ट तरीके के लिए प्रतिबद्धता जताई। यह तरीका इतना संरचनात्मक रूप से अव्यवस्थित निकला कि प्रमाण के लिए केवल छेदों को भरने के लिए 6,300 से अधिक लाइनों के कोड की आवश्यकता थी, या वह पूरी तरह विफल हो गया।
- P3 का तरीका: AI ने पहले विलोपन (deletion) की योजना बनाई। उसने महसूस किया कि एक अलग संरचनात्मक दृष्टिकोण को सिद्ध करना आसान होगा। वह उस योजना पर टिका रहा और उसने समस्या को मात्र 1,105 लाइनों में हल कर दिया।
यह क्यों महत्वपूर्ण है
यह पेपर सुझाव देता है कि AI के लिए वास्तव में विश्वसनीय सॉफ्टवेयर लिखने के लिए, हमें "कोड" और "प्रमाण" को दो अलग-अलग नौकरियों के रूप में देखना बंद करना होगा। कोड को डिजाइन करते समय ही AI को कोड की गणितीय सुरक्षा के बारे में सोचने के लिए मजबूर करके, हमें ऐसा सॉफ्टवेयर मिलता है जो न केवल निर्माण के समय ही सही (correct by construction) होता है, बल्कि उसे बनाना सस्ता और तेज़ भी होता है। यह "बाद में ठीक करें" से "पहली बार में ही सही बनाएं" की ओर एक बदलाव है, जो यह सुनिश्चित करता है कि जिस सॉफ्टवेयर पर हम भरोसा करते हैं वह उतना ही ठोस हो जितना कि वह गणित जो यह सिद्ध करता है कि वह काम करता है।
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।