💻 computer science

GPU-Accelerated Search and Certification of Bounded Indistinguishability in Finite Kripke Semantics

यह शोध पत्र एक GPU-त्वरित ढांचे को प्रस्तुत करता है जो व्यापक स्तर पर पूर्ण मोडल फॉर्मूला मूल्यांकन और काउंटरमॉडल प्रमाणन करने के लिए परिमित क्रिप्के सिमेंटिक्स (Kripke semantics) को बिटमास्क के रूप में एनकोड करता है, जो रिफ्यूटेबिलिटी (refutability) पर कड़े बंधों को प्रकट करता है, सिमेंटिक मिराज (semantic mirages) को संश्लेषित करता है, और ग्राफिक्स-समर्थित सिमेंटिक अन्वेषण को सक्षम बनाता है।

मूल लेखक: Faruk Alpay, Baris Basaran

प्रकाशित 2026-06-16

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

CC BY 4.0

मूल लेखक: Faruk Alpay, Baris Basaran

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

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

यह शोध पत्र एक विशाल, उच्च-गति वाला प्रयोग है जिसे एक सुपर-फास्ट कंप्यूटर चिप (GPU) का उपयोग करके इस प्रश्न का उत्तर देने के लिए डिज़ाइन किया गया है। यहाँ बताया गया है कि उन्होंने क्या किया और क्या पाया, सरल उपमाओं (analogies) का उपयोग करते हुए।

1. समस्या: "नन्ही दुनिया" का जाल (The "Tiny World" Trap)

तर्कशास्त्र में एक नियम है जो कहता है कि यदि कोई निर्देश गलत है, तो आप इसे एक "काउंटरएक्जांपल" (counterexample) के साथ गलत साबित कर सकते हैं—यानी एक विशिष्ट परिदृश्य जहाँ यह विफल हो जाता है। आमतौर पर, हम जानते हैं कि ऐसे परिदृश्य मौजूद हैं, लेकिन गणित कहता है कि वे असंभव रूप से विशाल हो सकते हैं (जैसे अरबों घरों वाला एक शहर)।

शोधकर्ताओं ने पूछा: क्या हमें गलती खोजने के लिए वास्तव में एक शहर की आवश्यकता है, या क्या हम इसे एक छोटे से गाँव में भी खोज सकते हैं? और इससे भी महत्वपूर्ण: यदि दो निर्देश एक गाँव में समान दिखते हैं, तो शहर को कितना बड़ा होना चाहिए कि वे अलग तरह से व्यवहार करने लगें?

2. उपकरण: "बिटमास्क" सुपर-स्कैनर (The "Bitmask" Super-Scanner)

इसकी जांच करने के लिए, उन्होंने एक विशेष स्कैनर बनाया। एक-एक करके परिदृश्य की जांच करने के बजाय (जैसे कोई इंसान किताब पढ़ता है), उन्होंने संभावनाओं की पूरी दुनिया को पूर्णांकों (integers/numbers) में बदल दिया।

उपमा: कल्पना कीजिए कि लाइट स्विच की एक पंक्ति है। यदि एक स्विच "ऑन" है, तो एक स्थिति सत्य है; यदि "ऑफ" है, तो वह असत्य है।
चाल: उन्होंने इन हजारों स्विचों को एक ही संख्या में समाहित कर दिया। फिर, उन्होंने इन स्विचों को एक साथ लाखों अलग-अलग "दुनियाओं" के लिए चालू-बंद करने के लिए कंप्यूटर के ग्राफिक्स कार्ड (GPU) का उपयोग किया।
परिणाम: वे केवल 45 मिनट में 163 ट्रिलियन (1.63 × 10¹⁴) अलग-अलग परिदृश्यों की जांच कर सके। यह ताश की एक गड्डी के हर संभावित क्रम की जांच करने जैसा है, और वह भी कॉफी बनाने के समय में।

3. खोज 1: छोटी गलतियाँ आम हैं (Small Mistakes are Common)

उन्होंने हजारों सरल तर्क फॉर्मूलों का परीक्षण किया।

निष्कर्ष: अधिकांश फॉर्मूले जो "गलत" (invalid) हैं, वे बहुत जल्दी विफल हो जाते हैं। वास्तव में, उनमें से अधिकांश के लिए, आपको उन्हें गलत साबित करने के लिए केवल एक या दो "कमरों" (दुनियाओं) वाली दुनिया की आवश्यकता होती है।
रूपक (Metaphor): पुरानी गणित की किताबें कहती थीं, "इसे गलत साबित करने के लिए, आपको 128 कमरों वाले एक हवेली की आवश्यकता हो सकती है।" शोधकर्ताओं ने पाया कि व्यवहार में, आपको गलती पकड़ने के लिए लगभग हमेशा केवल एक अलमारी (1 या 2 कमरे) की आवश्यकता होती है। "हवेली" का अनुमान बहुत अधिक निराशावादी था।

4. खोज 2: "सिमेंटिक मिराज" (The "Semantic Mirage" - मायावी जुड़वाँ)

सबसे रोमांचक हिस्सा उन दो फॉर्मूलों को खोजना था जो लंबे समय तक अभेद्य (indistinguishable) रहते हैं।

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

5. खोज 3: "मैप" बनाम "सर्च इंजन" (The "Map" vs. The "Search Engine")

उन्होंने इन तर्क फॉर्मूलों को एक 2D मानचित्र (जैसे स्कैटर प्लॉट) पर देखने की भी कोशिश की ताकि यह देखा जा सके कि क्या मनुष्य केवल चित्र देखकर अंतर पहचान सकते हैं।

परिणाम: मानचित्र बहुत अव्यवस्थित था। यह घास के ढेर में सुई खोजने जैसा था जहाँ 99% सुइयाँ एक के ऊपर एक रखी हुई थीं।
निष्कर्ष: यह मानचित्र विचार उत्पन्न करने (उम्मीदवार खोजने) के लिए अच्छा है, लेकिन यह एक खोज इंजन (discovery engine) नहीं है। आप केवल चित्र देखकर यह नहीं कह सकते, "आह, वह रहा अंतर!" आपको अभी भी मानचित्र द्वारा सुझाए गए विशिष्ट उम्मीदवारों की जांच करने के लिए सुपर-फास्ट कंप्यूटर की आवश्यकता होगी। कंप्यूटर न्यायाधीश है; मानचित्र केवल एक सुझाव बॉक्स है।

6. "सर्टिफिकेट" प्रणाली (The "Certificate" System)

यह सुनिश्चित करने के लिए कि सुपर-फास्ट कंप्यूटर कोई गलती न करे (चूंकि यह इतना तेज़ है कि यह कोई चरण छोड़ सकता है), उन्होंने एक अलग, धीमी लेकिन बहुत सावधान "रेफरी" प्रोग्राम बनाया।

यह कैसे काम करता है: तेज़ कंप्यूटर एक संभावित त्रुटि पाता है और उसे एक "सर्टिफिकेट" (एक नोट जिसमें लिखा है: "यहाँ फॉर्मूला है, यहाँ दुनिया है, यहाँ प्रमाण है") सौंप देता है।
जांच: धीमा रेफरी सर्टिफिकेट को पढ़ता है और कहता है, "हाँ, यह सही है।"
महत्व: इसका मतलब है कि परिणाम 100% भरोसेमंद हैं। उन्हें केवल एक तेज़ उत्तर नहीं मिला; उन्हें एक सत्यापित (verified) उत्तर मिला।

सारांश

यह शोध पत्र एक सुपर-फास्ट ग्राफिक्स कार्ड का उपयोग करके छोटी दुनियाओं में तर्क नियमों का व्यापक रूप से परीक्षण करने के बारे में है। उन्होंने खोजा कि:

अधिकांश तर्क त्रुटियाँ बहुत छोटी दुनिया (1 या 2 कमरे) में पकड़ी जाती हैं।
उन्हें तर्क नियमों का एक विशिष्ट जोड़ा मिला जो 6-कमरों वाली दुनिया तक पहुँचने तक समान दिखता है, और उन्होंने सिद्ध किया कि यही वह सटीक बिंदु है जहाँ वे अलग होते हैं।
दृश्य मानचित्र (visual maps) आपको यह समझने में मदद करते हैं कि कहाँ देखना है, लेकिन पुष्टि करने के लिए आपको अभी भी कंप्यूटर की आवश्यकता होती है कि आपने क्या देखा।

यह ब्रूट फोर्स (सब कुछ जांचना) को स्मार्ट गणित के साथ जोड़कर यह खोजने की कहानी है कि दो चीजें ठीक किस क्षण एक-दूसरे से अलग होना बंद करती हैं।

तकनीकी सारांश: परिमित क्रिपके सिमेंटिक्स में GPU-त्वरित खोज और सीमित अविभेद्यता का प्रमाणन

समस्या विवरण
यह शोध पत्र मोडल लॉजिक और फाइनाइट मॉडल थ्योरी से संबंधित दो मौलिक प्रश्नों को संबोधित करता है जो निर्णयात्मक (decidable) तो हैं लेकिन गणनात्मक रूप से महंगे हैं:

न्यूनतम प्रति-मॉडल आकार (Minimal Countermodel Size): अमान्य मोडल फॉर्मूला के लिए, मानक एक्सपोनेंशियल बाउंड्स (जो FMP और फिल्ट्रेशन द्वारा प्रदान किए जाते हैं) की तुलना में व्यवहार में न्यूनतम प्रति-मॉडल (countermodels) कितने बड़े होते हैं?
सीमित अविभेद्यता (Bounded Indistinguishability): एक परिमित मॉडल को कितना बड़ा होना चाहिए ताकि वह उन दो फॉर्मूलों के बीच अंतर कर सके जो सभी छोटे मॉडलों पर समान प्रतीत होते हैं? लेखक एक जोड़ी फॉर्मूलों को k-अविभेद्य (k-indistinguishable) के रूप में परिभाषित करते हैं यदि वे आकार $\le k$ के सभी फ्रेम्स पर सहमत होते हैं लेकिन आकार $k+1$ के एक फ्रेम पर भिन्न हो जाते हैं।

जबकि BDD-आधारित सिम्बोलिक मॉडल चेकिंग एकल फॉर्मूला के लिए बड़े स्टेट स्पेस को संकुचित करती है, यह कार्य इसके विपरीत शासन (regime) को लक्षित करता है: कई फॉर्मूलों का कई छोटे फ्रेम्स के विरुद्ध एक पूर्ण जनगणना (complete census)।

कार्यप्रणाली
लेखक परिमित क्रिपके मूल्यांकन की बिटवाइज़ प्रकृति का लाभ उठाते हैं ताकि GPU पर व्यापक समानांतरता (massive parallelism) सक्षम की जा सके।

बिटमास्क एनकोडिंग (Bitmask Encoding): दुनियाओं (worlds) को पूर्णांकों के रूप में और वैल्यूएशन्स (valuations) को बिटमास्क के रूप में एनकोड किया जाता है। बूलियन कनेक्टिव्स बिटवाइज़ ऑपरेशन्स में मैप होते हैं, जबकि मोडल ऑपरेटर्स ( $\Box$ और $\Diamond$ ) को सक्सेसर मास्क (successor masks) के कंटेनमेंट और इंटरसेक्शन परीक्षणों में कम किया जाता है (लेम्मा 1)। यह $(frame \times valuation)$ ट्रुथ टेंसर को भौतिक रूप (materialize) बनाने की आवश्यकता को समाप्त करता है।
फ्यूज्ड CUDA कर्नेल (Fused CUDA Kernel): एक एकल कर्नेल एक ही पास में एक निश्चित आकार के सभी फ्रेम्स के विरुद्ध फॉर्मूलों के एक पूरे संग्रह का मूल्यांकन करता है। थ्रेड्स को फ्रेम्स असाइन किए जाते हैं, जो लूप इंडिसेस के माध्यम से वैल्यूएशन्स के माध्यम से पुनरावृत्ति करते हैं (वैल्यूएशन एरे से बचते हुए) और एटोमिक कंटेंशन को कम करने के लिए शेयर्ड मेमोरी का उपयोग करके परिणामों को कम करते हैं।
सत्यापन आर्किटेक्चर (Verification Architecture): यह सिस्टम एक "फास्ट सर्च, स्लो चेक" प्रतिमान का उपयोग करता है। GPU गहन सूचीकरण (exhaustive enumeration) करता है, जबकि एक अलग, पारदर्शी रिकर्सिव CPU इवैल्यूएटर (जो बिटमास्क इंजन से स्वतंत्र है) प्रत्येक रिपोर्ट किए गए प्रति-मॉडल (countermodel) को सत्यापित करता है। यह सुनिश्चित करता है कि त्वरक (accelerator) के कार्यान्वयन विवरणों की परवाह किए बिना परिणाम विश्वसनीय हों।
सक्रिय संश्लेषण (Active Synthesis): निष्क्रिय सूचीकरण के परे, लेखक उम्मीदवार फॉर्मूला जोड़ियों (जैसे, $(\Box\Diamond)^m\top$ ) को उत्पन्न करने के लिए एक सक्रिय संश्लेषण प्रोटोकॉल का उपयोग करते हैं और "सिमेंटिक मिराज" (semantic mirages - अविभेद्य जोड़ियाँ) को खोजने के लिए एडवर्सरियल फ्रेम जनरेशन (Erdős–RényN, SCC बॉटलनेक्स, आदि) और मिनिमलिटी प्रमाणों के लिए SAT सॉल्वर का उपयोग करते हैं।
प्रतिनिधित्व-निर्देशित पुनर्प्राप्ति (Representation-Guided Retrieval): शोध पत्र एक "सिमेंटिक एटलस" (विफलता प्रोफाइल का डेंसिटी मैट्रिक्स) का निर्माण करता है और उम्मीदवार पुनर्प्राप्ति के लिए विभिन्न डाइमेंशनैलिटी रिडक्शन तकनीकों (PCA, UMAP, spectral) का मूल्यांकन करता है। महत्वपूर्ण रूप से, विज़ुअलाइज़ेशन को उम्मीदवार-जनरेशन इंटरफेस के रूप में माना जाता है, न कि स्टैंडअलोन डिस्कवरी इंजन के रूप में; प्रत्येक उम्मीदवार को गहन खोज के माध्यम से पुनः सत्यापित किया जाता है।

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

सत्यता और जटिलता: लेखक बिटमास्क इवैल्यूएटर के लिए शुद्धता प्रमाण (थ्योरम 1) प्रदान करते हैं और एक जटिलता विश्लेषण प्रस्तुत करते हैं जो दिखाता है कि दृष्टिकोण ट्रुथ टेंसर को स्टोर करने से बचता है (प्रपोजिशन 1)। सभी 20,990 उत्पन्न प्रमाणों को स्वतंत्र रूप से सत्यापित किया गया था।
छोटे न्यूनतम प्रति-मॉडल (Small Minimal Countermodels): 5,624 कॉन्स्टेंट-फ्री फॉर्मूलों (7 नोड्स, 2 वेरिएबल्स तक) के संग्रह में, अध्ययन में पाया गया कि न्यूनतम प्रति-मॉडल आश्चर्यजनक रूप से छोटे हैं।
- लॉजिक K में प्रत्येक रिफ्यूटेबल फॉर्मूला अधिकतम 2 दुनियाओं पर खंडित होता है (प्रपोजिशन 3)।
- मानक फिल्ट्रेशन बाउंड ( $2^{|Sub(\phi)|}$ ) अनुभवजन्य रूप से ढीली है; 7-नोड वाले फॉर्मूलों के लिए, बाउंड 128 दुनियाओं का सुझाव देती है, लेकिन अधिकतम देखा गया मान 2 था (कोरोलरी 1)।
सीमित अविभेद्यता का संश्लेषण: लेखकों ने सफलतापूर्वक एक प्रमाणित 5-इंडीस्टिंगुइशेबल जोड़ी ( $\alpha_2 = (\Box\Diamond)^2\top$ $α_{2} = (□◊)^{2} ⊤$ और $\alpha_3 = (\Box\Diamond)^3\top$ $α_{3} = (□◊)^{3} ⊤$ ) का संश्लेषण किया। ये फॉर्मूले आकार $\le 5$ $\leq 5$ के सभी फ्रेम्स पर सहमत होते हैं लेकिन एक विशिष्ट 6-वर्ल्ड पाथ द्वारा अलग किए जाते हैं (प्रपोजिशन 5)।
- इस सेपरेशन को गहन GPU सूचीकरण और सिम्बोलिक SAT प्रमाणों (टेबल 3) दोनों द्वारा पुष्ट किया गया था।
- एडवर्सरियल फ्रेम सिंथेसिस ने 90 सत्यापित सेपरेशन का उत्पादन किया, जिनमें से 78 नॉन-टेम्पलेट (अर्थात सरल पाथ या साइकिल नहीं) थे।
सिस्टम प्रदर्शन:
- फ्यूज्ड H100 कार्यान्वयन ने 60.2 बिलियन मूल्यांकन प्रति सेकंड की निरंतर दर प्राप्त की (45 मिनट में 1.63 $\times$ 10 $^{14}$ कुल मूल्यांकन)।
- यह एक मैच की गई वर्कलोड पर एक बिट-पैरेलल OpenMP CPU की तुलना में 47.1 $\times$ तेज़ और एक स्पष्ट AVX-512 CPU बेसलाइन की तुलना में 7.06 $\times$ तेज़ था।
- हार्डवेयर कैलिब्रेशन ने 18.87 सोर्स-लेवल uint32 TOPS और 98.3% माध्य NVML बिजी टाइम प्राप्त किया।
प्रतिनिधित्व और पुनर्प्राप्ति:
- 5.4 मिलियन उम्मीदवार जोड़ियों के पुनर्प्राप्ति कार्य में, टाइट नेबरहुड बजट ( $k=16$ ) के लिए रॉ हाई-डायमेंशनल फीचर्स ने सबसे अच्छा प्रदर्शन किया, जबकि 2D PCA एटलस ने व्यापक बजट ( $k=1024$ ) के लिए सबसे अच्छा प्रदर्शन किया।
- हालांकि, लेखक जोर देते हैं कि 2D विज़ुअलाइज़ेशन अत्यधिक क्लटर (100k स्केल पर 98.6% बिंदु एक ही बिन साझा करते हैं) से ग्रस्त हैं और स्टैंडअलोन डिस्कवरी टूल नहीं हैं। पाइपलाइन प्रतिनिधित्व-निर्देशित प्रस्ताव के बाद गहन सत्यापन पर निर्भर करती है।
कोरेस्पोंडेंस रिकवरी (Correspondence Recovery): इंजन ने सभी साल्क्विल्ड एक्सिओम्स (T, D, 4, 5, B, आदि) के लिए फर्स्ट-ऑर्डर फ्रेम कंडीशंस को सफलतापूर्वक रिकवर किया और सही ढंग से पहचाना कि मैककिंसी एक्सिओम (McKinsey axiom) का परीक्षण किए गए लाइब्रेरी में कोई फर्स्ट-ऑर्डर कोरेस्पोंडेंटेंट नहीं है, जो स्थापित सिद्धांत के विरुद्ध सिस्टम को मान्य करता है।

महत्व और दायरा
शोध पत्र का दावा है कि यह सामान्य मोडल लॉजिक के लिए नए निर्णय प्रक्रिया (जो PSPACE-complete बना हुआ है) के रूप में नहीं, बल्कि "स्मॉल-मॉडल शासन" और अविभेद्यता की सीमाओं को खोजने के लिए एक पुनरुत्पादक प्रोटोकॉल (reproducible protocol) के रूप में महत्वपूर्ण है।

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

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