💻 computer science

A Machine-Checked Cost Analysis of the BMSSP Recurrence in Isabelle/HOL With a Non-Vacuous Size-Parametric Runtime Witness

यह शोध पत्र 2025 के नियतात्मक (deterministic) $O(m \log^{2/3} n)$ SSSP एल्गोरिदम के अंतर्निहित BMSSP पुनरावृत्ति (recurrence) का Isabelle/HOL में पहला मशीन-चेक्ड औपचारिकीकरण प्रस्तुत करता है, जो बिना किसी स्वयंसिद्ध (axioms) या अप्रमाणित धारणाओं पर निर्भर हुए, एक अनबाउंड ग्राफ परिवार पर इसके $O(|V| \cdot (\ln |V|)^{2/3})$ रनटाइम का एक गैर-रिक्त (non-vacuous), आकार-पैरामेट्रिक प्रमाण प्रदान करता है।

मूल लेखक: Arthur Ramos, David Hulak, Ruy de Queiroz

प्रकाशित 2026-07-07

📖 6 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Arthur Ramos, David Hulak, Ruy de Queiroz

मूल पेपर CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक डिलीवरी ड्राइवर हैं जो एक विशाल, फैले हुए शहर के हर घर तक पहुँचने के लिए सबसे तेज़ रास्ता खोजने की कोशिश कर रहे हैं। दशकों तक, हमारे पास जो सबसे अच्छा मैप था (डिज्कस्ट्रा का एल्गोरिदम - Dijkstra's algorithm), वह एक बहुत ही व्यवस्थित लाइब्रेरियन की तरह था जिसे दिशा-निर्देश देने से पहले हर एक पते को वर्णानुक्रम (alphabetically) में व्यवस्थित करना पड़ता था। यह सॉर्टिंग वाला चरण "बॉटलनेक" (रुकावट) था—इसमें इतना समय लगता था कि ड्राइवर चाहे कितना भी स्मार्ट क्यों न हो जाए, वह उस समय को नहीं मात दे सकता था जो केवल लिस्ट को सॉर्ट करने में लग रहा था।

2025 में, शोधकर्ताओं की एक टीम (डुआन, माओ, माओ, शू और यिन) ने गाड़ी चलाने का एक नया तरीका निकाला। पूरे शहर को एक साथ सॉर्ट करने के बजाय, उन्होंने शहर को छोटे, प्रबंधनीय मोहल्लों में विभाजित किया और रास्तों को रिकर्सिवली (recursively) हल किया। यह नई विधि, जिसे BMSSP कहा जाता है, पुराने लाइब्रेरियन वाले तरीके से अधिक तेज़ है।

यह पेपर क्या करता है:
लेखकों ने केवल इस नए ड्राइविंग तरीके के बारे में पढ़ा नहीं; उन्होंने इसे "Isabelle/HOL" नामक एक "गणितीय रोबोट" के भीतर एक डिजिटल ट्विन के रूप में बनाया। सोचिए कि Isabelle एक अत्यंत सख्त, बिना पलक झपकाए देखने वाले रेफरी की तरह है जो प्रमाण (proof) के हर एक चरण की जांच करता है ताकि यह सुनिश्चित हो सके कि वह 100% तार्किक रूप से सत्य है, जिसमें मानवीय त्रुटि या "मुझे लगता है कि यह काम करेगा" जैसे अनुमानों के लिए कोई जगह नहीं है।

यहाँ उनके काम का सरल उपमाओं (analogies) के माध्यम से विवरण दिया गया है:

1. "रोबोट रेफरी" (फॉर्मल वेरिफिकेशन)

आमतौर पर, जब कंप्यूटर वैज्ञानिक कहते हैं कि एक एल्गोरिदम तेज़ है, तो वे एक पेपर लिखते हैं जिसमें वे गणित समझाते हैं और उम्मीद करते हैं कि पाठक उसके तर्क को समझ जाएगा। यह पेपर कहता है, "हम केवल उम्मीद नहीं करते; हमने इसे सिद्ध किया है।"

उपमा: कल्पना कीजिए कि एक शेफ दावा करता है कि वह 5 मिनट में एक परफेक्ट केक बना सकता है। एक सामान्य पेपर वह होता है जहाँ शेफ रेसिपी लिखता है। यह पेपर वह है जहाँ शेफ रेसिपी को एक रोबोट को सौंपता है जो केक को बेक करता है, हर सामग्री को तौलता है, हर सेकंड का समय लेता है, और एक सर्टिफिकेट जारी करता है कि, "हाँ, यह केक बिल्कुल वैसे ही बनाया गया है जैसा वर्णित किया गया था, और इसमें ठीक 5 मिनट लगे।"
परिणाम: उन्होंने सिद्ध किया कि नया "BMSSP" ड्राइविंग तरीका सही है और गणितीय रूप से इसकी गति सीमा (speed limit) की गणना की गई है।

2. "बकेट सिस्टम" (डेटा स्ट्रक्चर)

नया एल्गोरिदम डेटा को व्यवस्थित करने का एक विशेष तरीका उपयोग करता है जिसे "बकेटेड पार्टीशन" (bucketed partition) कहा जाता है।

उपमा: कल्पना कीजिए कि आपके पास मेल (पत्रों) का एक बड़ा ढेर है। पुराना तरीका था कि सबसे कम ज़िप कोड वाला पत्र खोजने के लिए हर एक पत्र को देखना। नया तरीका बकेट्स (buckets) के एक सेट का उपयोग करता है। आपके पास एक डायरेक्टरी है जो आपको बताती है कि किस बकेट में देखना है। आप पूरे ढेर को नहीं खोजते; आप बस डायरेक्टरी और फिर विशिष्ट बकेट को खोजते हैं।
चुनौती: लेखकों को यह सिद्ध करना था कि यह बकेट सिस्टम वास्तव में उतना ही तेज़ काम करता है जितना कि पेपर में दावा किया गया है। उन्होंने इन बकेट्स का एक डिजिटल संस्करण बनाया और सिद्ध किया कि बकेट के भीतर "सर्च कॉस्ट" (खोज लागत) वास्तव में पूरे ढेर को खोजने की तुलना में बहुत कम है।

3. "मशीन के अंदर का भूत" (द नॉन-वैक्युअस विटनेस - The Non-Vacuous Witness)

यह इस पेपर का सबसे अनूठा हिस्सा है। गणित में, आप कभी-कभी किसी कथन को केवल इसलिए सत्य सिद्ध कर सकते हैं क्योंकि वह स्थिति जिसका वह वर्णन करता है, कभी घटित ही नहीं होती। इसे "वैक्युअस ट्रुथ" (vacuous truth) कहा जाता है।

उपमा: कल्पना कीजिए कि एक नियम है कि "यदि आप चंद्रमा पर उड़कर जा सकते हैं, तो आपको इनाम मिलेगा।" यदि कोई भी चंद्रमा पर नहीं उड़ सकता, तो नियम तकनीकी रूप से सत्य है (क्योंकि किसी ने इसे तोड़ा नहीं है), लेकिन यह बेकार है।
समस्या: लेखकों ने एक विशिष्ट प्रकार की सड़क (घरों की एक लंबी, सीधी रेखा) पर अपने एल्गोरिदम की गति को सिद्ध करने का प्रयास किया। पहले उन्होंने "ड्राइविंग शेड्यूल" को "घरों की संख्या" के साथ बहुत कसकर जोड़ने (couple) की कोशिश की। उन्होंने पाया कि इस विशिष्ट सड़क पर, सख्त शेड्यूल के कारण ड्राइवर पहले घर के बाद ही फंस जाएगा। प्रमाण केवल इसलिए "सत्य" होगा क्योंकि ड्राइवर यात्रा पूरी ही नहीं कर पाएगा।
समाधान: उन्होंने महसूस किया कि उन्हें शेड्यूल को थोड़ा ढीला करना होगा (ड्राइवर को उस शहर के लिए योजना बनाने देना जो वे वास्तव में चला रहे हैं उससे थोड़ा बड़ा शहर मानकर) ताकि यह सुनिश्चित हो सके कि ड्राइवर वास्तव में यात्रा पूरी कर सके।
उपलब्धि: उन्होंने सिद्ध किया कि:
1. शहर (ग्राफ का परिवार) वास्तव में बड़ा और बड़ा होता जा रहा है (यह एक निश्चित आकार का नहीं है)।
2. ड्राइवर वास्तव में यात्रा पूरी कर सकता है (रन अस्तित्व में है)।
3. लगने वाला समय वास्तव में तेज़ है, यहाँ तक कि इस अनंत सड़क पर भी।

वे इसे "नॉन-वैक्युअस साइज-पैरामेट्रिक रनटाइम विटनेस" कहते हैं। सरल भाषा में: "हमने सिद्ध किया कि एल्गोरिदम तेज़ है, और हमने यह भी सिद्ध किया कि यह वास्तव में काम करता है, और यह प्रमाण एक ऐसी स्थिति पर आधारित नहीं है जो कभी घटित ही नहीं होती।"

4. उन्होंने क्या नहीं किया

लेखक अपने काम की सीमाओं के बारे में बहुत ईमानदार हैं।

उन्होंने वास्तविक कार नहीं बनाई: उन्होंने पूरे 2025 के एल्गोरिदम को शुरू से अंत तक इस तरह सत्यापित नहीं किया कि आप इसे अपने लैपटॉप पर डाउनलोड करके समय बचाने के लिए चला सकें।
उन्होंने वास्तविक समय को नहीं मापा: उन्होंने यह नहीं मापा कि वास्तविक कंप्यूटर पर कितने सेकंड लगते हैं। उन्होंने "ऑपरेशन काउंट्स" (गणित के कितने स्टेप्स लगते हैं) को मापा।
उन्होंने यह दावा नहीं किया कि यह हर संभव सड़क के लिए काम करता है: उन्होंने सिद्ध किया कि यह विशिष्ट, अनंत "सीधी रेखा" वाली सड़कों के परिवार के लिए पूरी तरह से काम करता है। उन्होंने स्वीकार किया कि इसे हर संभव सड़क के आकार के लिए सिद्ध करना भविष्य के लिए एक कठिन कार्य है।

सारांश

यह पेपर एक गणितीय गुणवत्ता नियंत्रण रिपोर्ट है। लेखकारों ने एक बिल्कुल नए, जटिल और बहुत तेज़ एल्गोरिदम (शॉर्टेस्ट पाथ खोजने के लिए) को लिया, उसका एक परफेक्ट डिजिटल मॉडल बनाया, और एक रोबोट रेफरी का उपयोग करके दो चीजें सिद्ध कीं:

एल्गोरिदम सही उत्तर देता है।
एल्गोरिदम तेज़ है, और यह गति का दावा वास्तविक है (किसी ऐसी स्थिति का धोखा नहीं है जो कभी घटित नहीं होती)।

उन्होंने अपने स्वयं के तर्क में एक "जाल" (trap) भी पाया जहाँ एक सख्त संस्करण वाला प्रमाण विफल हो जाता, और उन्होंने दस्तावेज़ित किया कि उन्होंने उस जाल से कैसे बचा। यह एक अत्याधुनिक कंप्यूटर विज्ञान की खोज का एक कठोर, "नो-गैप्स अलाउड" (कोई कमी नहीं) सत्यापन है।

तकनीकी सारांश: BMSSP पुनरावृत्ति (Recurrence) का एक मशीन-चेक्ड लागत विश्लेषण

समस्या विवरण
यह शोध पत्र बाउंडेड मल्टी-सोर्स शॉर्टेस्ट पाथ (BMSSP) पुनरावृत्ति के औपचारिक सत्यापन (formal verification) को संबोधित करता है, जो डुआन, माओ, माओ, शू और यिन द्वारा 2025 के नियतात्मक (deterministic) एल्गोरिदम का मुख्य इंजन है, जिसने निर्देशित सिंगल-सोर्स शॉर्टेस्ट पाथ (SSSP) के लिए लंबे समय से चले आ रहे $O(m + n \log n)$ "सॉर्टिंग बैरियर" को तोड़ा है। जबकि मूल एल्गोरिदम $O(m \log^{2/3} n)$ का रनिंग टाइम प्राप्त करता है, एक प्रूफ़ असिस्टेंट में इसकी शुद्धता और, विशेष रूप से, इसके एमोर्टाइज्ड (amortized) लागत विश्लेषण को औपचारिक रूप देना महत्वपूर्ण चुनौतियाँ प्रस्तुत करता है। इनमें स्रोतों के सेट और बाउंडेड डिस्टेंस रेंज से जुड़े रिकर्सिव शुद्धता तर्क, कस्टम पार्टीशन डेटा संरचनाओं पर एमोर्टाइज्ड अकाउंटिंग की सूक्ष्मता, और "वैक्यूअस" (vacuous) एसिम्प्टोटिक थ्योरम्स का जोखिम शामिल है—ऐसे कथन जो तकनीकी रूप से सत्य तो हैं लेकिन अर्थहीन हैं क्योंकि इनपुट फैमिली सीमित है या आवश्यक रन मौजूद नहीं हैं।

कार्यप्रणाली
लेखक Isabelle/HOL (Isabelle2025-2) में एक पूर्ण औपचारिकीकरण प्रस्तुत करते हैं, जिसे मॉड्यूलरिटी और चिंताओं के कठोर पृथक्करण को सुनिश्चित करने के लिए छह अलग-अलग, स्तरित सिद्धांतों (theories) में संरचित किया गया है। यह विकास केवल HOL और HOL-Library को इम्पोर्ट करता है, इसमें कोई बाहरी एक्सिओम, sorry, या oops स्टेटमेंट नहीं है।

सिमेंटिक फाउंडेशन: लेखक परिमित भारित डाइग्राफ (finite weighted digraphs), सरल वॉक (simple walks), और डिस्टेंस मेट्रिक्स को परिभाषित करते हैं। वे अद्वितीय शॉर्टेस्ट वॉक और स्ट्रिक्ट टाई-ब्रेकिंग के संबंध में संरचनात्मक लेम्मा स्थापित करते हैं, जो सभी आगामी तर्कों का आधार बनते हैं।
रिकर्सिव शुद्धता: BMSSP पुनरावृत्ति का एक एब्स्ट्रैक्ट मॉडल औपचारिक रूप दिया गया है, जिसमें FindPivots रूटीन, बेस केसेस और पार्टीशन लूप शामिल हैं। एक मशीन-चेक्ड प्रूफ़ यह स्थापित करता है कि एब्स्ट्रैक्ट एल्गोरिदम किसी भी सुव्यवस्थित ग्राफ के लिए शॉर्टेस्ट डिस्टेंस सही ढंग से कंप्यूट करता है।
एग्जीक्यूटेबल आर्टिफैक्ट: एब्स्ट्रैक्ट मॉडल को नेचुरल-नंबर वर्टिस और वेट्स का उपयोग करके एक एग्जीक्यूटेबल फंक्शन (bmssp_distances) में रिफाइन किया गया है। लेखक bmssp_correct_strong को सिद्ध करते हैं, जो पुष्टि करता है कि एग्जीक्यूटेबल आउटपुट शॉर्टेस्ट डिस्टेंस की सिमेंटिक परिभाषा से मेल खाता है, जिसे एक विशिष्ट पांच-वर्टेक्स उदाहरण पर मूल्यांकन के माध्यम से सत्यापित किया गया है।
कॉस्ट मॉडल: एक एब्स्ट्रैक्ट पार्टीशन इंटरफेस (Insert, BatchPrepend, Pull) को कॉस्ट प्रेडिकेट्स के साथ परिभाषित किया गया है। लेखक इस एब्स्ट्रैक्ट पुनरावृत्ति के लिए $O(m \log^{2/3} n)$ का एमोर्टाइज्ड कॉस्ट एनवेलप सिद्ध करते हैं। महत्वपूर्ण रूप से, वे एक बकेटेड पार्टीशन डेटा स्ट्रक्चर को लागू करते हैं जो पेपर के लॉगरिदमिक शेड्यूल को निष्ठापूर्वक साकार करता है, और स्पीडअप के लिए आवश्यक निर्णायक $O(\log(N/M))$ इंसर्ट स्केल को सिद्ध करता है।
ऑपरेशनल रिफाइनमेंट्स: दो ऑपरेशनल लेयर्स को परिभाषित किया गया है:
- Exact-Concrete: रिकर्सिव चाइल्ड के आउटपुट को स्ट्रिक्टली इंक्रीमेंटल रेंज स्लाइस से जोड़ता है।
- Charged: आउटपुट को अलग करता है, केवल इंक्रीमेंटल स्लाइस को चार्ज करता है।
  लेखक मशीन-चेक करते हैं कि exact-concrete संबंध इच्छित इनपुट्स (विशेष रूप से पाथ फैमिलीज़ पर) पर नॉन-टोटल (non-total) है, जो एक बाधा उत्पन्न करता है जहाँ पूर्ण रन अस्तित्व में नहीं हो सकते।
साइज़-पैरामेट्रिक लेयर: लेखक यूनिट-वेट डाइरेक्टेड पाथ्स ( $P_n$ ) का एक अनबाउंडेड फैमिली कंस्ट्रक्ट करते हैं। वे सिद्ध करते हैं कि charged संबंध टोटल है और एक पूर्ण रन मौजूद है। टोटैलिटी सुनिश्चित करने के लिए, बिना एसिम्प्टोटिक क्लास को बदले, वे एक "इन्फ्लेटेड" शेड्यूल इंडेक्स ( $N = n \cdot n$ ) का उपयोग करते हैं, जो यह सुनिश्चित करता है कि बकेट कैपेसिटी पाथ को कवर करे जबकि $O(\log^{2/3} n)$ फैक्टर को सुरक्षित रखा जाए।

प्रमुख योगदान

प्रथम मेकेनाइज्ड फॉर्मलाइजेशन: यह BMSSP पुनरावृत्ति और उसके रनिंग-टाइम विश्लेषण का पहला मशीन-चेक्ड फॉर्मलाइजेशन है।
नॉन-वैक्यूअस साइज़-पैरामेट्रिक विटनेस: पेपर एक अनकंडीशनल थ्योरम प्रदान करता है जो यूनिट-वेट डाइरेक्टेड पाथ्स पर, charged रनिंग टाइम $O(|V| \cdot (\ln |V|)^{2/3})$ है। यह परिणाम नॉन-वैक्यूअस है क्योंकि लेखक स्पष्ट रूप से सिद्ध करते हैं (एक "नॉन-वैक्यूसिटी लेजर" के माध्यम से) कि फैमिली बिना किसी सीमा के बढ़ती है, एक पूर्ण रन अस्तित्व में है, और ऑपरेटिंग रिजीम वास्तविक है।
कपलिंग ऑब्स्ट्रक्शन का औपचारिक निदान: लेखक एक नाइव, टाइटली कपल्ड कॉस्ट रिलेशन (exact-concrete मॉडल) में दोष को औपचारिक रूप से पहचानते और सिद्ध करते हैं। वे प्रदर्शित करते हैं कि यह रिलेशन एल्गोरिदम को पाथ फैमिलीज़ पर अधिकतम एक स्टेप लेने के लिए मजबूर करता है, जिससे इस पर आधारित कोई भी साइज़-पैरामेट्रिक बाउंड वैक्यूअस हो जाता है। इस बाधा को एक मशीन-चेक्ड लेम्मा के रूप में रिकॉर्ड किया गया है, और मुख्य परिणाम को इस बाधा को पार करने के लिए डीकप्ल्ड charged रिलेशन का उपयोग करके निकाला गया है।
एग्जीक्यूटेबल वेरिफिकेशन: डेवलपमेंट में एक एग्जीक्यूटेबल शॉर्टेस्ट-डिस्टेंस फंक्शन शामिल है जिसमें शुद्धता का प्रमाण है जिसे बिल्ड प्रोसेस के भीतर कोड इवैल्यूएशन द्वारा सत्यापित किया गया है।

परिणाम
मुख्य थ्योरम, path_nonvac_runtime_bigo_card_V_unconditional, यह बताता है:
$(\lambda n. \text{real}(\text{path\_nonvac\_time } n)) \in O(\lambda n. \text{real}(\text{card}(\text{path\_k\_V } n)) \cdot (\ln(\text{real}(\text{card}(\text{path\_k\_V } n) + 2))^{2/3})$
यह बाउंड है:

अनकंडीशनल: इसमें रन अस्तित्व या ग्राफ गुणों के संबंध में कोई हाइपोथीसिस नहीं है।
साइज़-पैरामेट्रिक: एसिम्प्टोटिक वेरिएबल वास्तविक ग्राफ साइज ( $|V|$ ) है, न कि एक फिक्स्ड पैरामीटर।
नॉन-वैक्यूअस: यह एक लीस्ट-कॉस्ट रन के कॉस्ट को बांधता है जो सिद्ध है कि मौजूद है।

पेपर यह भी स्थापित करता है कि कंक्रीट बकेटेड स्ट्रक्चर द्वारा साकार किए गए एब्स्ट्रेक्ट कॉस्ट मॉडल के लिए $O(m \log^{2/3} n)$ का बाउंड है, जो $O(\log(N/M))$ इंसर्ट स्केल की पुष्टि करता है।

महत्व और दायरा
लेखक इस कार्य के महत्व को BMSSP पुनरावृत्ति की शुद्धता और चार्ज्ड रनिंग-टाइम विश्लेषण के एक कठोर औपचारिकीकरण के रूप में स्पष्ट रूप से फ्रेम करते हैं, न कि पूर्ण एंड-टू-एंड वेरिफिकेशन के रूप में।

क्या दावा किया गया है: पेपर दावा करता है कि उसने पुनरावृत्ति लॉजिक की शुद्धता और चार्ज्ड ऑपरेशन-कॉस्ट विश्लेषण की वैधता को सत्यापित किया है, जिसमें एक विशिष्ट अनबाउंडेड फैमिली के लिए एक नॉन-वैक्यूअस एसिम्प्टोटिक बाउंड शामिल है।
क्या दावा नहीं किया गया है: लेखक यह दावा नहीं करते हैं कि उन्होंने एक्सपोर्ट किए गए SML कोड की मशीन-स्टेप कॉम्प्लेक्सिटी को सत्यापित किया है, और न ही वे सभी ग्राफ्स या सभी रन्स के लिए यूनिवर्सल बाउंड का दावा करते हैं। वे स्पष्ट रूप से कहते हैं कि साइज़-पैरामेट्रिक एक विशिष्ट फैमिली के लीस्ट-कॉस्ट रन को बांधता है, क्योंकि इस फैमिली के लिए यूनिवर्सल बाउंड गलत है।
मेथोडोलॉजिकल योगदान: पेपर "नॉन-वैक्यूटी" को मेकेनाइज्ड कॉम्प्लेक्सिटी में एक फर्स्ट-क्लास प्रूफ ऑब्लिगेशन के रूप में महत्व देता है। यह प्रदर्शित करता है कि एसिम्प्टोटिक थ्योरम्स लॉजिकल रूप से वैध हो सकते हैं लेकिन अर्थहीन हो सकते हैं यदि इनपुट फैमिली सीमित है या रन मौजूद नहीं हैं। "नॉन-वैक्यूसिटी लेजर" (ग्रोथ, रन अस्तित्व और रिजीम रियलाइजेशन को सिद्ध करना) को भविष्य के रिकर्सिव कॉम्प्लेक्सिटी आर्गुमेंट्स के लिए एक पुन: प्रयोज्य टेम्पलेट के रूप में प्रस्तुत किया गया है।

संक्षेप में, यह कार्य BMSSP पुनर्वृत्ति के लिए एक हाई-अश्योरेंस, मशीन-चेक्ड फाउंडेशन प्रदान करता है, जो कार्यात्मक शुद्धता को कॉस्ट एनालिसिस से सावधानीपूर्वक अलग करता है और सार्थक एसिम्प्टोटिक बाउंड सुनिश्चित करने के लिए एमोर्टाइज्ड कॉम्प्लेक्सिटी को औपचारिक बनाने के खतरों का सटीक निदान करता है।

1. "रोबोट रेफरी" (फॉर्मल वेरिफिकेशन)

2. "बकेट सिस्टम" (डेटा स्ट्रक्चर)

3. "मशीन के अंदर का भूत" (द नॉन-वैक्युअस विटनेस - The Non-Vacuous Witness)

4. उन्होंने क्या नहीं किया

सारांश

इसी तरह के और पेपर