🔢 mathematics

Prover-Adversary games for systems over (non-deterministic) branching programs

यह शोध पत्र डिटरमिनिस्टिक और नॉन-डिटरमिनिस्टिक ब्रांचिंग प्रोग्राम्स के लिए प्रूफ सिस्टम्स को कैरेक्टराइज़ करने हेतु पुडलाक-बस शैली के प्रूवर-एडवर्सरी गेम्स पेश करता है, जो इन गेम्स और eLDT एवं eLNDT प्रूफ सिस्टम्स के बीच पॉलिनॉमियल इक्विवेलेंस स्थापित करते हुए इमरमैन-सेलेप्सेनीي थ्योरम का एक प्रूफ कॉम्प्लेक्सिटी वर्ज़न व्युत्पन्न करता है।

मूल लेखक: Anupam Das, Avgerinos Delkos

प्रकाशित 2026-02-27

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

CC BY 4.0

मूल लेखक: Anupam Das, Avgerinos Delkos

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

यहाँ इस शोध पत्र (paper) का सरल भाषा, उपमाओं (analogies) और रूपकों (metaphors) के साथ विवरण दिया गया है।

बड़ी तस्वीर: "20 सवाल" का खेल बनाम एक नियम पुस्तिका (Rulebook)

कल्पना कीजिए कि आप यह साबित करने की कोशिश कर रहे हैं कि एक जटिल मशीन (जैसे कि एक कंप्यूटर प्रोग्राम) कभी क्रैश नहीं होगी, या वह हमेशा एक विशिष्ट परिणाम ही देगी।

कंप्यूटर विज्ञान की दुनिया में, इसे करने के दो मुख्य तरीके हैं:

नियम पुस्तिका (प्रूफ सिस्टम): आप तर्क के लंबे, औपचारिक चरणों की एक सूची लिखते हैं, जैसे कि एक गणित की पाठ्यपुस्तक, जो चरण-दर-चरण यह सिद्ध करती है कि मशीन क्यों काम करती है।
खेल (प्रूवर-एडवर्सरी गेम्स): आप एक चालाक प्रतिद्वंद्वी के खिलाफ एक खेल खेलते हैं। आप मशीन के बारे में सवाल पूछते हैं, और प्रतिद्वंद्वी "हाँ" या "नहीं" में उत्तर देता है। यदि आप प्रतिद्वंद्वी को दो ऐसी बातें कहने के लिए मजबूर कर सकते हैं जो एक-दूसरे का खंडन करती हों (जैसे कि एक ही समय में "लाइट चालू है" और "लाइट बंद है"), तो आप जीत जाते हैं।

इस पेपर का लक्ष्य:
लेखक, अनुपम दास और अवगेरिनोस डेलकोस, यह दिखाना चाहते थे कि एक विशिष्ट प्रकार के कंप्यूटर प्रोग्राम (जिसे ब्रांचिंग प्रोग्राम्स कहा जाता है) के लिए, ये दोनों तरीके वास्तव में बराबर शक्तिशाली हैं। यदि आप खेल जीत सकते हैं, तो आप एक छोटा प्रमाण (proof) लिख सकते हैं। यदि आप एक छोटा प्रमाण लिख सकते हैं, तो आप खेल जीत सकते हैं।

उन्होंने दो प्रकार के प्रोग्रामों पर ध्यान केंद्रित किया:

डिटरमिनिस्टिक (BP): एक मशीन जो एक ही, सीधे पथ का अनुसरण करती है। जैसे एक एकल पटरी पर चलने वाली ट्रेन।
नॉन-डिटरमिनिस्टिक (NBP): एक मशीन जो "अनुमान" लगा सकती है या एक साथ कई रास्ते ले सकती है। जैसे एक भूलभुलैया (maze) में चलने वाला व्यक्ति जो एक साथ हर दरवाजे को आज़मा सकता है।

चुनौती: "नेगेशन" (Negation) की समस्या

डिटरमिनिस्टिक मशीन (ट्रेन) वाला हिस्सा आसान था।
यदि आपके पास एक ट्रेन की पटरी है, तो एक "उल्टा" ट्रैक बनाना आसान है। यदि ट्रेन बाईं ओर जाती है, तो उल्टा पथ दाईं ओर जाएगा। लेखकों ने दिखाया कि इन सरल मशीनों के लिए, खेल और नियम पुस्तिका पूरी तरह से मेल खाते हैं।

कठिन हिस्सा नॉन-डिटरमिनिस्टिक मशीन (भूलभुलैया) था।
भूलभुलैया में, मशीन कई रास्ते ले सकती है। किसी चीज़ को गलत साबित करने के लिए, आपको यह साबित करना होगा कि कोई भी रास्ता निकास तक नहीं ले जाता है।

समस्या: आप एक "उल्टा" भूलभुलैया कैसे बनाएंगे जो यह सिद्ध करे कि "कोई भी रास्ता निकास तक नहीं ले जाता" बिना अनंत लूप (infinite loop) में फंसे?
उपमा: कल्पना कीजिए कि आप एक विशाल, बदलती हुई भूलभुलैया में एक विशिष्ट दरवाजे के बंद होने का प्रमाण देने की कोशिश कर रहे हैं। ऐसा करने के लिए, आपको उस तक जाने वाले हर एक रास्ते की जांच करनी होगी। यदि भूलभुलैया बहुत बड़ी है, तो एक-एक करके हर रास्ते की जांच करने में अनंत काल लग जाएगा।

सफलता: "जादुई काउंटर" (इम्मरमैन-ज़लेप्सेनियी)

लेखकों ने इस कठिन समस्या को हल करने के लिए इम्मरमैन-ज़लेप्सेनियी थ्योरम नामक एक प्रसिद्ध गणितीय विचार का उपयोग किया।

रूपक: "सटीक गणना" (Exact Count) की ट्रिक
कल्पना कीजिए कि आप 1,000 लोगों के कमरे में हैं और आपको यह जानने की आवश्यकता है कि क्या उनमें से ठीक 50 लोगों ने लाल टोपियाँ पहनी हैं।

पुराना तरीका: आप हर किसी से पूछते हैं, "क्या आपने लाल टोपी पहनी है?" और गिनती करते हैं। यदि आपकी गिनती गलत हो जाती है, तो आपको फिर से शुरू करना पड़ता है।
लेखकों का तरीका: उन्होंने महसूस किया कि आपको यह जानने की ज़रूरत नहीं है कि कौन लाल टोपी पहने हुए है। आपको बस एक जादु적인 "काउंटर" की आवश्यकता है जो कहे, "मैंने 50 लाल टोपियाँ गिनी हैं।"
- यदि काउंटर कहता है "50," और आपको एक लाल टोपी मिलती है, तो काउंटर "51" कहेगा (जो गलत है, इसलिए आप जानते हैं कि कुछ गड़बड़ है)।
- यदि काउंटर कहता है "50," और आपको कोई लाल टोपी नहीं मिलती है, तो आप जानते हैं कि आप सुरक्षित हैं।

लेखकों ने एक "पार्शियल नेगेशन" (Partial Negation) टूल बनाया। पूरी भूलभुलैया को एक साथ उलटने के बजाय, उन्होंने एक ऐसा टूल बनाया जो कहता है: "यदि इस समूह में ठीक K लोग सच बोल रहे हैं, तो यह विशिष्ट पथ अवरुद्ध है।"

प्रत्येक संभावित "सच बोलने वालों" की संख्या (0, 1, 2... N तक) के लिए ऐसा करके, वे सभी संभावनाओं को कवर कर सके। उन्होंने सिद्ध किया कि भले ही भूलभुलैया जटिल हो, फिर भी आप इसका एक छोटा, कुशल "नियम पुस्तिका" (प्रमाण) लिख सकते हैं, बशर्ते आप इस "जादुई काउंटर" ट्रिक का उपयोग करें।

यह क्यों मायने रखता है?

जटिलता को सरल बनाना: यह एक अस्त-व्यस्त, भ्रमित करने वाले खेल को एक साफ, तार्किक प्रमाण में बदल देता है। यह दिखाता है कि "अनुमान लगाना" (non-determinism) उतना डरावना नहीं है जितना कि हम सोचते थे; हम अभी भी इसके बारे में कुशलता से तर्क कर सकते हैं।
"लॉगस्पेस" (Logspace) कनेक्शन: कंप्यूटर विज्ञान में, कठिनाई का एक पदानुक्रम (hierarchy) होता है।
- L (लॉगस्पेस): आसान समस्याएँ (जैसे सूची को सॉर्ट करना)।
- NL (नॉन-डिटरमिनिस्टिक लॉगस्पेस): कठिन समस्याएँ (जैसे भूलभुलैया सुलझाना)।
- परिणाम: लेखकों ने दिखाया कि "अल्टरनेटिंग" समस्याओं (जहाँ आपको अनुमान लगाना होता है और फिर जांचना होता है और फिर से अनुमान लगाना होता है) के लिए डिज़ाइन किया गया सिस्टम वास्तव में मानक "नॉन-डिटरमिनिस्टिक" सिस्टम से अधिक कठिन नहीं है।
- उपमा: यह यह सिद्ध करने जैसा है कि एक ऐसा खेल जहाँ आपको पासवर्ड का अनुमान लगाना होता है, फिर सुरक्षा प्रश्न का अनुमान लगाना होता है, फिर एक पिन का अनुमान लगाना होता है, वास्तव में केवल पासवर्ड का अनुमान लगाने से अधिक कठिन नहीं है। "पदानुक्रम" (hierarchy) ढह जाता है।

संक्षेप में (Summary in a Nutshell)

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

संक्षेप में: उन्होंने "20 सवालों" के खेल और एक औपचारिक गणितीय प्रमाण के बीच एक पुल बनाया, यह दिखाते हुए कि जब कंप्यूटर "अनुमान" भी लगा रहा हो, तब भी हम नियमों को पूरी तरह से ट्रैक रख सकते हैं।

यहाँ अनूपम दास और अवगेरिनोस डेलकोस के शोध पत्र "Prover-Adversary Games for Systems over (Non-Deterministic) Branching Programs" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र L (लॉगस्पेस) और NL (नॉन-डिटरमिनिस्टिक लॉगस्पेस) जैसी जटिलता श्रेणियों (complexity classes) के लिए प्रूफ़ सिस्टम को प्रोवर-एडवर्सरी गेम्स (Prover-Adversary games) का उपयोग करके लक्षणित करने की चुनौती को संबोधित करता है, जो पुडलाक और बस द्वारा पेश किया गया एक ढांचा है।

संदर्भ: बस, दास और नॉप के पिछले कार्य ने eLDT (डिटरमिनिस्टिक ब्रांचिंग प्रोग्राम्स, BPs के लिए) और eLNDT (नॉन-डिटरमिनिस्टिक ब्रांचिंग प्रोग्राम्स, NBPs के लिए) प्रूफ़ सिस्टम पेश किए थे। ये सिस्टम एक्सटेंशन वेरिएबल्स का उपयोग करके ब्रांचिंग प्रोग्राम्स की dag-संरचना का प्रतिनिधित्व करने वाले सूत्रों (formulas) के बारे में तर्क देते हैं।
अंतराल (The Gap): जबकि प्रूफ़ सिस्टम (DAG-जैसे) और गेम्स (Tree-like) अक्सर समकक्ष होते हैं, नॉन-डिटरमिनिस्टिक सिस्टम के लिए इस समानता को स्थापित करना कठिन है।
- डिटरमिनिस्टिक सेटिंग्स में, भाषा सरल निर्माणों के माध्यम से बूलियन संयोजनों (नेगेशन सहित) के लिए बंद (closed) होती है।
- नॉन-डिटरमिनिस्टिक सेटिंग्स में, एक NBP के नेगेशन (negation) की गणना करना गैर-तुच्छ (non-trivial) है। इसके लिए इमरमैन-ज़ेलेपसेनी (Immerman-Szelepcsényi) प्रमेय ($coNL = NL$) की आवश्यकता होती है, जो बताता है कि एक NL भाषा का पूरक (complement) NL में ही होता है।
- मौजूदा प्रूफ़ सिस्टम गेम-थ्योरिटिक ढांचे के भीतर इस नेगेशन को कुशलतापूर्वक औपचारिक रूप देने में संघर्ष करते हैं (जहाँ रणनीतियाँ प्रूफ आकार के सापेक्ष लॉगरिदमिक गहराई में होनी चाहिए)।

लेखक $eLDT $और$ eLNDT$ के अनुरूप बहुपद रूप से (polynomially) $DB $और$ NB$ गेम्स को परिभाषित करने और NBPs के नेगेशन से जुड़ी तकनीकी बाधा को हल करने का लक्ष्य रखते हैं।

2. कार्यप्रणाली (Methodology)

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

A. प्रोवर-एडवर्सरी गेम्स को परिभाषित करना

वे दो गेम्स, DB (डिटरमिनिस्टिक) और NB (नॉन-डिटरमिनिस्टिक) पेश करते हैं, जहाँ:

खिलाड़ी (Players): प्रोवर (प्रश्न पूछता है) बनाम एडवर्सरी (बूलियन मान असाइन करता है)।
क्वेरी (Queries): क्वेरीज़ ब्रांचिंग प्रोग्राम्स का प्रतिनिधित्व करने वाले सूत्रों के बूलियन संयोजन हैं (जैसे, $A \land \neg B$ )।
जीत की स्थिति (Winning Condition): प्रोवर तब जीतता है जब एडवर्सरी के असाइनमेंट एक "सरल विरोधाभास" (जैसे, $0 \to 1$ , या एक निर्णय विरोधाभास जैसे $ApB \to 1, p \to 0, A \to 0$ ) की ओर ले जाते हैं।
रणनीति (Strategy): एक जीतने वाली रणनीति एक बाइनरी ट्री है। ट्री की गहराई ट्री के आकार के लघुगणक (logarithm) के अनुरूप होती है।

B. प्रूफ़्स को रणनीतियों में अनुवादित करना

लेखक सिद्ध करते हैं कि $eLDT $या$ eLNDT $में किसी भी प्रूफ़ को$ DB $या$ NB$ में एक जीतने वाली रणनीति में परिवर्तित किया जा सकता है।

तंत्र (Mechanism): वे प्रूफ़ ट्री पर 'डिवाइड-एंड-कॉन्कर' दृष्टिकोण का उपयोग करते हैं। एक सिक्वेंट (sequent) को एक एकल क्वेरी माना जाता है। रणनीति प्रूफ़ में पहले "गलत" सिक्वेंट को खोजती है।
परिणाम: यदि एक प्रूफ़ का आकार $N$ है, तो $O(\log N)$ राउंड वाली एक जीतने वाली रणनीति मौजूद होती है।

C. रणनीतियों को प्रूफ़्स में अनुवादित करना (मुख्य चुनौती)

विपरीत दिशा (रणनीति $\to$ प्रूफ़) इस शोध पत्र का मुख्य तकनीकी योगदान है।

डिटरमिनिस्टिक केस ( $DB \to eLDT$ ): सीधा है। चूंकि डिटरमिनिस्टिक ब्रांचिंग प्रोग्राम्स नेगेशन के तहत बंद हैं ( $\neg(ApB) \iff \neg A p \neg B$ ), गेम क्वेरीज़ को सीधे प्रूफ़ नियमों में अनुवादित किया जा सकता है।
नॉन-डिटरमिनिस्टिक केस ( $NB \to eLNDT$ ): इसके लिए एक NBP के नेगेशन को औपचारिक रूप देने की आवश्यकता है।
- चरण 1: डी मॉर्गन नॉर्मल फॉर्म: रणनीतियों को ऐसे रूप में परिवर्तित किया जाता है जहाँ नेगेशन केवल परमाणु (atomic) ब्रांचिंग प्रोग्राम्स पर लागू होता है (जटिल बूलियन संरचनाओं के भीतर कोई नेगेशन नहीं)।
- चरण 2: काउंटिंग के माध्यम से आंशिक नेगेशन: एक NBP $B$ को $eLNDT$ के भीतर नकारने के लिए, लेखक इमरमैन-ज़ेलेपसेनी प्रमेय का एक नॉन-यूनिफॉर्म संस्करण औपचारिक रूप देते हैं।
- निर्माण (The Construction): वे "k-deciders" ( $A B^k_i C$ ) पेश करते हैं। ये नए एक्सटेंशन वेरिएबल्स हैं जो प्रोग्रामों के एक सेट में सत्य इनपुट्स की एक निश्चित संख्या $k$ के सापेक्ष एक उप-प्रोग्राम $B_i$ के नेगेशन की गणना करते हैं।
- काउंटिंग तंत्र: वे यह गिनने के लिए "थ्रेशोल्ड प्रोग्राम्स" (पिछले कार्यों से) का उपयोग करते हैं कि कितने इनपुट सत्य हैं। प्रूफ़ सिस्टम सत्य इनपुट्स की संख्या ( $k$ ) पर इंडक्शन (induction) करता है ताकि सभी संभावनाओं को समाप्त किया जा सके, जो प्रभावी रूप से ग्लोबल नेगेशन का अनुकरण (simulate) करता है।

3. प्रमुख योगदान (Key Contributions)

eLDT/eLNDT का गेम कैरेक्टराइजेशन:
यह शोध पत्र $eLDT/eLNDT $प्रूफ़ सिस्टम और नए परिभाषित गेम्स$ DB/NB$ के बीच बहुपद समानता (polynomial equivalence) स्थापित करता है। यह ब्रांचिंग प्रोग्राम्स पर आधारित प्रूफ़ सिस्टम के लिए एक कैनोनिकल "ट्री-लाइक" लक्षण वर्णन प्रदान करता है।
eLNDT में इमरमैन-ज़ेलेपसेनी का औपचारिकीकरण:
लेखक $eLNDT $प्रूफ़ सिस्टम के भीतर$ coNL = NL$ प्रमेय का एक अभिनव, नॉन-यूनिफॉर्म औपचारिकीकरण प्रदान करते हैं।
- मानक एल्गोरिथम प्रमाणों के विपरीत, वे आंशिक नेगेशन (k-deciders) का निर्माण करते हैं जो सत्य इनपुट्स की एक विशिष्ट संख्या के सापेक्ष कार्य करते हैं।
- वे NBP संरचना में सीधे काउंटिंग को एनकोड करने से बचते हैं; इसके बजाय, वे सत्य इनपुट्स की संख्या पर इंडक्शन करने की प्रूफ़ सिस्टम की क्षमता पर भरोसा करते हैं।
coNL = NL का प्रूफ़ कॉम्प्लेक्सिटी एनालॉग:
विकसित मशीनरी का उपयोग करते हुए, वे सिद्ध करते हैं कि $eLNDT $प्रणाली **$ \exists\forall $-अल्टरनेटिंग ब्रांचिंग प्रोग्राम्स** (एक बार नॉन-डिटरमिनिज्म के साथ प्रोग्राम) पर आधारित$ eL\exists\forall DT$ प्रणाली का पॉलीनोमियल सिमुलेशन करती है।
- यह लॉगस्पेस पदानुक्रम (Logspace Hierarchy) के पहले स्तर ($NL$) में पतन (collapse) का एक प्रूफ़-कॉम्प्लेक्सिटी संस्करण है।

4. प्रमुख परिणाम (Key Results)

प्रमेय 4.1: आकार $N$ के $eLNDT $(या$ eLDT $) प्रूफ़,$ NB $(या$ DB $) में$ O(\log N)$ राउंड वाली जीतने वाली रणनीतियों में अनुवादित होते हैं।
प्रमेय 6.1: आकार $N$ की $NB $(या$ DB $) रणनीतियाँ,$ eLNDT $(या$ eLDT $) में$ poly(N)$ आकार के प्रूफ़ में अनुवादित होती हैं।
प्रमेय 5.7 (औपचारिक इमरमैन-ज़ेलेपसेनी): NBPs के किसी भी सेट के लिए, एक्सटेंशन वेरिएबल्स (k-deciders) और $eLNDT$ में बहुपद-आकार के प्रूफ़ मौजूद हैं जो सत्य इनपुट्स की एक निश्चित संख्या के सापेक्ष एक NBP के निर्णय का सही ढंग से अनुकरण करते हैं।
प्रमेय 7.3: $eLNDT$, $eL\exists\forall DT$ का बहुपद रूप से अनुकरण (polynomially simulates) करता है। यह दर्शाता है कि NL के लिए प्रूफ़ सिस्टम $\exists\forall$ -BPs के दूसरे स्तर को संभालने के लिए पर्याप्त शक्तिशाली है।

5. महत्व (Significance)

गेम्स और थ्योरी को जोड़ना: यह कार्य "डैग-लाइक" प्रूफ़ सिस्टम (जो कॉम्प्लेक्सिटी में मानक हैं) और "ट्री-लाइक" गेम सिस्टम (जो बाउंडेड अरिथमेटिक और इंटरैक्टिव प्रूफ में मानक हैं) के बीच के अंतर को सफलतापूर्वक पाटता है। यह $L$ और $NL$ के लिए प्रूफ़ के संरचनात्मक गुणों को समझने के लिए महत्वपूर्ण है।
नॉन-डिटरमिनिज्म को संभालना: यह प्रूफ़ कॉम्प्लेक्सिटी में एक लंबे समय से चली आ रही तकनीकी कठिनाई को हल करता है: नॉन-डिटरमिनिस्टिक सेटिंग्स में प्रूफ़ आकार को बढ़ाए बिना नेगेशन को कैसे संभालें। "k-decider" निर्माण एक परिष्कृत उपकरण है जो नेगेशन की जटिलता को प्रोग्राम स्तर के बजाय प्रूफ़ स्तर पर अलग करता है।
पदानुक्रम पतन (Hierarchy Collapse): $\exists\forall$ -BPs के साथ $eLNDT $के सिमुलेशन का परिणाम, ट्यूरिंग मशीन सिमुलेशन से स्वतंत्र, प्रूफ़ कॉम्प्लेक्सिटी के क्षेत्र के भीतर$ coNL = NL$ के एक ठोस, सिंटैक्टिक प्रमाण प्रदान करता है।
भविष्य की दिशाएँ: लेखक सुझाव देते हैं कि इन गेम्स का उपयोग $eL(N)DT$ की अन्य प्रूफ़ सिस्टम जैसे कि OBDD-आधारित सिस्टम के साथ तुलना करने और इमरमैन-ज़ेलेपसेनी प्रमेय की बाउंडेड अरिथमेटिक स्ट्रेंथ की जांच करने के लिए किया जा सकता है।

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