VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean
यह शोधपत्र VeriSoftBench प्रस्तुत करता है, जो ओपन-सोर्स सॉफ्टवेयर वेरिफिकेशन प्रोजेक्ट्स से लीन 4 (Lean 4) के 500 प्रूफ ऑब्लिगेशन्स का एक रिपॉजिटरी-स्केल बेंचमार्क है, जो यह प्रकट करता है कि वर्तमान LLMs गणितीय से कोड-केंद्रित परिवेश में स्थानांतरित होने में संघर्ष करते हैं और प्रमाण स्वचालन (proof automation) की सफलता पर क्रॉस-फाइल डिपेंडेंसीज के महत्वपूर्ण प्रभाव को उजागर करता है।
मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें
कल्पना कीजिए कि आप एक प्रतिभाशाली लेकिन अनुभवहीन प्रशिक्षु (apprentice) को एक जटिल मशीन ठीक करना सिखाने की कोशिश कर रहे हैं।
पुराना तरीका (Math Benchmarks)
लंबे समय तक, शोधकर्ताओं ने इन AI "प्रशिक्षुओं" का परीक्षण Mathlib के माध्यम से किया। Mathlib को एक विशाल, पूरी तरह से व्यवस्थित पुस्तकालय की तरह समझें जिसमें गणित के सार्वभौमिक तथ्य मौजूद हैं। यह ऐसा है जैसे प्रशिक्षु को एक विशाल पाठ्यपुस्तक दी गई हो जहाँ हर परिभाषा मानक है, हर अध्याय क्रमांकित है, और समस्याओं के उत्तर हमेशा एक ही अनुमानित स्थानों पर मिलते हैं।
- समस्या: वास्तविक दुनिया का सॉफ़्टवेयर गणित की पाठ्यपुस्तक जैसा नहीं होता। यह एक अस्त-व्यस्त, फैले हुए निर्माण स्थल (construction site) जैसा है जहाँ हर इमारत का अपना अनूठा ब्लूप्रिंट, कस्टम उपकरण और अजीब स्थानीय नियम होते हैं जो कहीं और नहीं मिलते।
नई चुनौती: VeriSoftBench
लेखकों को एहसास हुआ कि AI गणित की समस्याओं को हल करने में तो बहुत अच्छा हो रहा है, लेकिन वास्तविक दुनिया के सॉफ़्टवेयर सत्यापन (software verification) में बुरी तरह विफल हो रहा है। इसलिए, उन्होंने Veriस्थी-सॉफ्टबेंच (VeriSoftBench) बनाया।
VeriSoftBench को 500 अलग-अलग "प्रूफ पहेलियों" वाला एक विशाल, अराजक गोदाम समझें।
- प्रत्येक पहेली एक वास्तविक, ओपन-सोर्स सॉफ़्टवेयर प्रोजेक्ट (जैसे कि एक सुरक्षित ब्लॉकचेन या एक कंपाइलर) से जुड़ा एक विशिष्ट कार्य है।
- एक पहेली को हल करने के लिए, AI केवल एक मानक नियम नहीं देख सकता। उसे गोदाम में घूमना होगा, उस विशिष्ट, कस्टम-मेड टूल को खोजना होगा जिसे प्रोजेक्ट ने कल ही बनाया है, यह समझना होगा कि वह टूल तीन फाइलों दूर स्थित दूसरे टूल से कैसे जुड़ता है, और फिर यह समझना होगा कि वर्तमान समस्या को हल करने के लिए उसका उपयोग कैसे किया जाए।
- यह सुडोकू पहेली हल करने (मानक नियम) और एक कार के इंजन को ठीक करने के बीच का अंतर है, जहाँ मैनुअल उस एक विशेष कार मॉडल के लिए एक गुप्त कोड में लिखा गया है।
प्रयोग: प्रशिक्षु की मदद करने के दो तरीके
शोधकर्ताओं ने यह देखने के लिए AI का परीक्षण दो अलग-अलग स्थितियों में किया कि वह इस अराजकता को कैसे संभालता है:
- "क्यूरेटेड" बॉक्स (एक सहायक गुरु):
कल्पित करें कि एक गुरु पहेली को देखता है, केवल वही सटीक उपकरण और ब्लूप्रिंट ढूंढता है जिनकी AI को आवश्यकता है, और उन्हें एक साफ, छोटा बॉक्स सौंप देता है।
- परिणाम: AI ठीक-ठाक था (लगभग 40% सफलता)। वह पहेली को हल कर सका जब उसके लिए सही उपकरण खोजने की कठिन मेहनत पहले ही कर दी गई थी।
- "पूरा गोदाम" (एक भारी भरकम डुबकी):
कल्पित करें कि आप AI को लाखों अन्य उपकरणों, ब्लूप्रिंट और रैंडम पुर्जों के साथ पूरे गोदाम में छोड़ देते हैं, और कहते हैं, "शुभकामनाएं, जो चाहिए ढूंढ लो!"
- परिणाम: AI भ्रमित हो गया। सफलता दर काफी कम हो गई। सूचना की भारी मात्रा (noise) ने सही संकेत (signal) को ढूंढना कठिन बना दिया।
प्रमुख खोजें ("अहा!" क्षण)
- गणित विशेषज्ञ, सॉफ़्टवेयर विशेषज्ञ नहीं हैं: वे AI मॉडल जो गणित की समस्याओं को हल करने में चैंपियन हैं (जैसे कि Mathlib पर प्रशिक्षित), वे इन सॉफ़्टवेयर पहेलियों के सामने पूरी तरह विफल रहे। वे एक शतरंज के ग्रैंडमास्टर की तरह थे जो पोकर खेलने की कोशिश कर रहा हो; उनके कौशल का यहाँ कोई लाभ नहीं मिला।
- "डोमिनो प्रभाव" की कठिनाई: पहेली जितनी कठिन होती, उसमें उतने ही अधिक "ट्रांजिटिव डिपेंडेंसीज़" (transitive dependencies) होते थे।
- उपमा: एक रेसिपी (विधि) की कल्पना करें। एक सरल रेसिपी के लिए आटा और अंडे चाहिए। लेकिन एक जटिल रेसिपी के लिए आटा चाहिए, लेकिन उस आटे के लिए एक विशिष्ट प्रकार का गेहूं चाहिए, जो एक विशिष्ट उर्वरक पर निर्भर करता है, जो एक विशिष्ट वर्षा पैटर्न पर निर्भर करता है।
- VeriSoftBench में, किसी समस्या को हल करने के लिए, AI को अक्सर कोड में 10 या 20 कस्टम परिभाषाओं की एक श्रृंखला का पीछा करना पड़ता है। श्रृंखला जितनी लंबी होगी, AI के भटकने की संभावना उतनी ही अधिक होगी।
- संदर्भ (Context) एक दोधारी तलवार है: AI को बहुत अधिक जानकारी देना (पूरा गोदाम) पर्याप्त जानकारी देने (क्यूरेटेड बॉक्स) से भी बदतर था। हालांकि, "परफेक्ट" टूल बॉक्स के साथ भी, AI संघर्ष करता रहा। इसका मतलब है कि समस्या केवल सही जानकारी ढूंढने की नहीं है; बल्कि जटिल, कस्टम लॉजिक के माध्यम से तर्क करने की है जिसे AI ने पहले कभी नहीं देखा है।
यह क्यों महत्वपूर्ण है?
वर्तमान में, AI "पाठ्यपुस्तक" वाले गणित में बहुत अच्छा है लेकिन वास्तविक दुनिया की इंजीनियरिंग में बहुत खराब है। यह पेपर एक अलार्म बजाता है: यदि हम चाहते हैं कि AI हमें सुरक्षित, बग-मुक्त सॉफ़्टवेयर (जैसे कि सेल्फ-ड्राइविंग कारों या चिकित्सा उपकरणों के लिए) लिखने में मदद करे, तो हम केवल इसे गणित की समस्याओं पर प्रशिक्षित नहीं कर सकते। हमें इसे उन अस्त-व्यस्त, कस्टम कोडबेस में नेविगेट करना सिखाना होगा जहाँ नियम चलते-फिरते बनाए जाते हैं।
संक्षेप में:
पेपर कहता है, "हमने एक नया परीक्षण बनाया जो वास्तविक सॉफ़्टवेयर इंजीनियरिंग की नकल करता है। हमने पाया कि वर्तमान AI एक ऐसे छात्र की तरह है जिसने फाइनल परीक्षा में टॉप किया लेकिन वह एक लीक होने वाले नल को ठीक नहीं कर सकता क्योंकि नल में एक कस्टम पुर्जा लगा है जिसे उसने पहले कभी नहीं देखा। हमें उन्हें व्यवस्थित क्लासरूम के बजाय, अस्त-व्यस्त वर्कशॉप में नेविगेट करना सिखाने की आवश्यकता है।"
अपने क्षेत्र के पेपरों की भीड़ में उलझे हुए हैं?
आपके रिसर्च कीवर्ड से मेल खाने वाले सबसे नए और अलग सोच वाले पेपरों का रोज़ाना Digest पाएँ—तकनीकी सारांश के साथ, आपकी भाषा में।