💻 computer science

Determination of the fifth Busy Beaver value

यह शोध पत्र पाँचवें बिजी बीवर मान, $S(5) = 47,176,870$ के प्रथम औपचारिक रूप से सत्यापित निर्धारण को प्रस्तुत करता है, जिसे कोक (Coq) प्रूफ़ असिस्टेंट का उपयोग करके 181 मिलियन से अधिक ट्यूरिंग मशीनों का विश्लेषण करने वाले एक व्यापक सहयोगात्मक ऑनलाइन प्रयास के माध्यम से प्राप्त किया गया है।

मूल लेखक: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Sha

प्रकाशित 2026-03-24

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

CC BY 4.0

मूल लेखक: The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Naściszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann

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

कल्पना कीजिए कि आप एक विशाल, अराजक दौड़ आयोजित कर रहे हैं। दौड़ने वाले छोटे, सरल रोबोट हैं जिन्हें ट्यूरिंग मशीन (Turing Machines) कहा जाता है। उनका दिमाग बहुत सीमित है (कुछ "अवस्थाएं" या states) और उनके पास कागज की एक लंबी, अनंत पट्टी (टेप) है जो पूरी तरह से खाली है।

दौड़ के नियम सरल हैं:

रोबोट कागज के एक स्थान को पढ़ता है, एक नया प्रतीक (0 या 1) लिखता है, बाएं या दाएं चलता है, और अपनी आंतरिक स्थिति (state) बदलता है।
यदि रोबोट ऐसी जगह पहुँच जाता है जहाँ उसे नहीं पता कि क्या करना है, तो वह रुक जाता है (halt)।
लक्ष्य? यह देखना कि कौन सा रोबोट रुकने से पहले सबसे अधिक कदम चल सकता है।

यह बीजी बीवर गेम (Busy Beaver Game) है। प्रश्न यह है: "n अवस्थाओं वाला एक रोबोट रुकने से पहले कितने अधिकतम कदम ले सकता है?"

लंबे समय तक, गणितज्ञों को 1, 2, 3 और 4 अवस्थाओं वाले रोबोटों के उत्तर पता थे। लेकिन 5 अवस्थाओं के लिए, उत्तर एक रहस्य था। यह एक ऐसी दौड़ में विजेता का अनुमान लगाने जैसा था जहाँ फिनिश लाइन इतनी दूर है कि आप उसे देख भी नहीं सकते और कुछ धावक बिना रुके हमेशा के लिए दौड़ते रह सकते हैं।

बड़ी सफलता

यह शोध पत्र The bbchallenge Collaboration नामक स्वयंसेवकों की एक विशाल ऑनलाइन टीम द्वारा 5-स्टेट रोबोटों के रहस्य को अंततः सुलझाने की कहानी है।

उन्होंने सिद्ध किया कि विजेता ठीक 47,176,870 कदम चलता है।

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

उन्होंने यह कैसे किया? (उपमा)

कल्पना कीजिए कि आपके पास 16 ट्रिलियन किताबों का एक पुस्तकालय है। प्रत्येक पुस्तक एक अलग रोबोट का वर्णन करती है। आपको उस रोबोट को खोजना है जो सबसे लंबा दौड़ता है।

समस्या: आप 16 ट्रिलियन किताबें नहीं पढ़ सकते। कुछ रोबोट लाखों वर्षों तक चलते हैं; अन्य हमेशा के लिए चलते रहते हैं।
समाधान (ट्री नॉर्मल फॉर्म): टीम ने महसूस किया कि कई रोबोट केवल "जुड़वां" हैं (वे एक ही काम करते हैं, बस उनके नाम अलग हैं)। उन्होंने इन जुड़वाओं को समूह में रखने के लिए एक वंश वृक्ष (family tree) बनाया। इससे पुस्तकालय 16 ट्रिलियन किताबों से घटकर एक प्रबंधनीय 181 मिलियन रह गया। अभी भी बहुत है, लेकिन कंप्यूटर के लिए संभव है।

इसके बाद, उन्होंने एक फिल्टरिंग मशीन (निर्णय लेने वाले 'deciders' की एक पाइपलाइन) बनाई। इसे सुरक्षा जांच बिंदुओं की एक श्रृंखला के रूप में समझें:

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

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

उनमें से एक, जिसका नाम "स्केलेट #17" (Skelet #17) था, "फाइनल बॉस" था। यह इतना जटिल था कि इसे समझाने के लिए एक समर्पित शोध पत्र की आवश्यकता थी। यही वह आखिरी मशीन थी जिसे वश में किया गया।

"क्रिप्टिड्स" (जंगल के राक्षस)

यह शोध पत्र क्रिप्टिड्स (Cryptids) के बारे में भी बात करता है। बिगफुट और लोच नेस मॉन्स्टर की दुनिया में, ये वे जीव हैं जिनके अस्तित्व के बारे में लोग सोचते हैं लेकिन वे इसे सिद्ध नहीं कर पाते।
बीजी बीवर की दुनिया में, एक क्रिप्टिड वह रोबोट है जिसके बारे में हमें लगता है कि वह हमेशा के लिए चलता रहेगा, लेकिन हम अभी तक इसे सिद्ध नहीं कर पाए हैं।

टीम ने पाया कि 6-स्टेट रोबोटों के लिए, कई क्रिप्टिड्स मौजूद हैं।
उनमें से एक प्रसिद्ध अनसुलझी गणितीय समस्या (कोलात्ज़ कंजैक्चर/Collatz Conjecture) से जुड़ा है। यह सिद्ध करना कि क्या यह रोबोट रुकता है, उस गणितीय समस्या को हल करने जितना ही कठिन है।
लेखक मजाक में कहते हैं कि गणित की "सबसे छोटी खुली समस्या" शायद एक 6-स्टेट रोबोट के भीतर छिपी हुई है।

आपको इसकी परवाह क्यों करनी चाहिए?

यह एक टीम प्रयास है: यह किसी लैब कोट पहने अकेले जीनियस द्वारा नहीं किया गया था। यह सैकड़ों लोगों (छात्रों, इंजीनियरों, शौकीनों) द्वारा किया गया था जो डिस्कॉर्ड (Discord) पर चैट कर रहे थे, कोड साझा कर रहे थे और एक-दूसरे की मदद कर रहे थे। यह एक विशाल ओपन-सोर्स सॉफ्टवेयर प्रोजेक्ट की तरह है, लेकिन गणित के लिए।
यह AI के लिए एक परीक्षण है: लेखक अब इस प्रमाण का उपयोग आर्टिफिशियल इंटेलिजेंस (AI) का परीक्षण करने के लिए कर रहे हैं। क्या एक AI इन रोबोटों के पीछे के तर्क को समझ सकता है? अब तक, AI ठीक-ठाक प्रदर्शन कर रहा है, लेकिन यह एक कठिन चुनौती है।
ज्ञान की सीमाएँ: यह शोध पत्र हमें उस सीमा को दिखाता है जिसे हम जान सकते हैं। हम 5-स्टेट के लिए उत्तर सिद्ध कर सकते हैं, लेकिन 6-स्टेट के लिए, समस्याएँ इतनी कठिन हो जाती हैं कि वे हमारे वर्तमान गणितीय नियमों के साथ असंभव हो सकती हैं।

निचोड़

टीम ने सफलतापूर्वक 5-स्टेट बीजी बीवर दौड़ के चैंपियन को खोज निकाला है। उन्होंने सिद्ध किया है कि यह ठीक 47,176,870 कदम चलता है और फिर रुक जाता है। उन्होंने यह तर्क के एक ऐसे डिजिटल किले का निर्माण करके किया जिसे कोई चुनौती नहीं दे सकता।

यह मानवीय जिज्ञासा, सहयोग और ब्रह्मांड की सीमाओं को समझने में कंप्यूटर की शक्ति की जीत है। और जबकि उन्होंने 5-स्टेट के रहस्य को सुलझा लिया है, उन्होंने 6-स्टेट की दुनिया में "क्रिप्टिड्स" का एक पूरा नया जंगल भी खोज निकाला है, जो अगली पीढ़ी के खोजकर्ताओं द्वारा हल किए जाने की प्रतीक्षा कर रहा है।

यहाँ bbchallenge सहयोग द्वारा लिखित शोध पत्र "Determination of the fifth Busy Beaver value" का विस्तृत तकनीकी सारांश दिया गया है।

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

यह शोध पत्र बजी बीवर फलन (Busy Beaver function) $S(n)$ के निर्धारण को संबोधित करता है, जिसे एक $n$ -स्टेट, 2-सिंबल ट्यूरिंग मशीन द्वारा (सभी शून्य टेप से शुरू होकर) निष्पादित किए जा सकने वाले अधिकतम चरणों की संख्या के रूप में परिभाषित किया गया है।

संदर्भ: $S(n)$ एक गैर-गणनीय (non-computable) फलन है। इस कार्य से पूर्व, केवल $S(1)$ से $S(4)$ तक को कठोरता से सिद्ध किया गया था ( $S(4)=107$ )।
चुनौती: $S(5)$ का निर्धारण करने के लिए एक विशाल खोज स्थान (search space) के हैल्टिंग व्यवहार का विश्लेषण करना आवश्यक है। जबकि विजेता मशीन (जो 1989 में खोजी गई थी) 47,176,870 चरणों तक चलती है, प्राथमिक कठिनाई यह सिद्ध करने में है कि कोई अन्य 5-स्टेट मशीन इससे अधिक समय तक नहीं चलती या बाद में समाप्त (halt) नहीं होती। इसमें लाखों मशीनों की गैर-हैल्टिंग स्थिति को सिद्ध करना शामिल है, जिनमें से कुछ जटिल, अराजक व्यवहार प्रदर्शित करती हैं जो कठिन गणितीय अनुमानों (जैसे गोल्डबैक अनुमान या रीमान परिकल्पना) की नकल करते हैं।
लक्ष्य: औपचारिक रूप से यह सिद्ध करना कि $S(5) = 47,176,870$ और $S(2, 4) = 3,932,964$ (2-स्टेट, 4-सिंबल मशीनों के लिए) एक मशीन-सत्यापित प्रमाण (machine-verified proof) का उपयोग करके।

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

लेखकों ने Coq प्रूफ असिस्टेंट का उपयोग करते हुए व्यापक सहयोगात्मक प्रयास और औपचारिक सत्यापन (formal verification) का उपयोग किया। कार्यप्रणाली तीन मुख्य स्तंभों से बनी है:

A. खोज स्थान न्यूनीकरण: ट्री नॉर्मल फॉर्म (Tree Normal Form - TNF)

समस्या को गणनात्मक रूप से सुलभ बनाने के लिए, लेखकों ने ट्री नॉर्मल फॉर्म (TNF) गणना का उपयोग किया।

न्यूनीकरण: $\approx 1.67 \times 10^{13}$ (16.7 ट्रिलियन) संभावित 5-स्टेट मशीनों के सिंटैक्टिक कुल का विश्लेषण करने के बजाय, TNF खोज स्थान को 181,385,789 अद्वितीय मशीनों तक कम कर देता है।
तकनीक: TNF केवल आवश्यकता होने पर ट्रांज़िशन को परिभाषित करके मशीनों का पुनरावर्ती (recursively) निर्माण करता है, जिससे अप्राप्य (unreachable) ट्रांज़िशन को हटा दिया जाता है और उन मशीनों को बाहर कर दिया जाता है जो केवल स्टेट्स या सिम्बल्स के क्रमपरिवर्तन (permutations) मात्र हैं।
कार्यान्वयन: संपूर्ण TNF गणना और ट्रैवर्सल को सीधे Coq के भीतर लागू किया गया था, जो पिछले तरीकों से एक महत्वपूर्ण विचलन है जो अनवेरिफाइड बाहरी गणनाओं पर निर्भर थे।

B. ड décider पाइपलाइन (The Decider Pipeline)

इस प्रमाण का मूल "ड décidéर्स" (deciders) नामक एल्गोरिदम की एक पाइपलाइन है जो यह निर्धारित करने का प्रयास करती है कि क्या कोई मशीन रुकती (halt) है या लूप (loop) बनाती है। चूंकि 'हैल्टिंग समस्या' अनिर्णय योग्य (undecidable) है, इसलिए ये आंशिक ड décidéर्स हैं; यदि एक विफल होता है, तो मशीन को अगले ड décidéर को भेज दिया जाता है।

लूप्स (एल्गोरिदम 1): स्टेट-सिंबल-हेड पोजीशन टुपल्स के पूर्ण टेप कॉन्फ़िगरेशन के बजाय इतिहास का विश्लेषण करके मानक चक्रों (Cyclers) और स्थानिक रूप से अनुवादित चक्रों (Translated Cyclers) का पता लगाता है। इसने गैर-हैल्टिंग मशीनों के 95.48% मामलों को हल किया।
n-ग्राम क्लोज्ड पोजीशन सेट (NGramCPS): यह "क्लोज्ड पोजीशन सेट" तकनीक का एक अमूर्तीकरण (abstraction) है। यह यह सिद्ध करने के लिए स्थानीय कॉन्फ़िगरेशन (टेप सिम्बल्स के n-grams) को ट्रैक करता है कि मशीन अवस्थाओं के एक बंद सेट में प्रवेश करती है जिससे वह हैल्टिंग ट्रांज़िशन तक नहीं पहुँच सकती। इसने शेष गैर-हैल्टिंग मशीनों के 99.89% मामलों को हल किया।
- संवर्द्धन (Augmentation): लेखकों ने जटिल टेप निर्भरताओं को संभालने के लिए इसे "फिक्स्ड-लेंथ हिस्ट्री" और "लीस्ट रिसेंट यूसेज (LRU)" हिस्ट्री के साथ बढ़ाया।
रिपीटेड वर्ड लिस्ट (RepWL): टेप कॉन्फ़िगरेशन का प्रतिनिधित्व करने के लिए रेगुलर एक्सप्रेशन का उपयोग करता है। यदि प्रतीकों का एक ब्लॉक एक सीमा $T$ से अधिक बार दोहराया जाता है, तो इसे एक अनंत पुनरावृत्ति माना जाता है। यह फ्रैक्टल-जैसी या आवधिक टेप वृद्धि वाली मशीनों को संभालता है।
फाइनाइट ऑटोमेटा रिडक्शन (FAR) और वेटेड FAR (WFAR):
- FAR: गैर-नियतात्मक फाइनाइट ऑटोमेटा (NFA) का उपयोग करने वाली एक co-CTL (co-Closed Tape Language) तकनीक, जो यह सिद्ध करती है कि हैल्टिंग कॉन्फ़िगरेशन का सेट प्रारंभिक कॉन्फ़िगरेशन से विलग (disjoint) है।
- WFAR: गैर-नियमित भाषाओं को संभालने के लिए वेटेड फाइनाइट ऑटोमेटा का उपयोग करते हुए एक विस्तार, जो अधिक जटिल इनवेरियंट्स वाली मशीनों के लिए गैर-हैल्टिंग प्रमाण की अनुमति देता है।
स्पोरैडिक मशीनें (Sporadic Machines): उन 13 मशीनों के लिए जिन्होंने सभी स्वचालित ड décidéर्स का विरोध किया, टीम ने गैर-हैल्टिंग के व्यक्तिगत, हस्तनिर्मित Coq प्रमाण बनाए। ये मशीनें अद्वितीय व्यवहार प्रदर्शित करती हैं (जैसे, फाइबोनैकी काउंटर्स, ग्रे कोड अस्पष्टता, और विशाल प्री-पीरियड लूप)।

C. औपचारिक सत्यापन (Coq-BB5)

प्रमाण: पूरी प्रक्रिया को Coq-BB5 नामक एक औपचारिक प्रमाण स्क्रिप्ट में समाहित किया गया है।
रिफ्लेक्शन (Reflection): प्रमाण "प्रूफ बाय रिफ्लेक्शन" का उपयोग करता है, जहाँ Coq सत्यापित एल्गोरिदम (TNF गणना और ड décidéर्स) को चलाता है और अंतिम प्रमेय (theorem) बनाने के लिए उनके आउटपुट का उपयोग करता है।
विश्वास (Trust): एकमात्र बाहरी एक्सिओम जिसका उपयोग किया गया है वह functional_extensionality_dep है, जो मानक और सुसंगत है। यह प्रमाण 13 कोर पर ~45 मिनट में संकलित (compile) होता है।

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

बजी बीवर मान का पहला औपचारिक सत्यापन: यह पहली बार है जब किसी बजी बीवर मान को मशीन-चेक्ड प्रमाण के साथ निर्धारित किया गया है, जिससे लाखों मामलों के सत्यापन में मानवीय त्रुटि की संभावना समाप्त हो गई है।
विशाल सहयोगात्मक अनुसंधान: इस परियोजना ने bbchallenge.org का उपयोग किया, जो एक ऐसा मंच है जहाँ सैकड़ों योगदानकर्ताओं (मुख्यतः गैर-अकादमिक) ने ड décidéर्स विकसित किए, "होल्डआउट्स" का विश्लेषण किया और विभिन्न भाषाओं (C++, Python, Rust, Haskell, आदि) में कोड साझा किया।
एल्गोरिदम संबंधी नवाचार:
- ट्रांसक्रिप्ट विश्लेषण का उपयोग करके लूप डिटेक्शन के लिए एल्गोरिदम 1 का विकास।
- टेप संवर्द्धन (LRU/Fixed history) के साथ NGramCPS का परिशोधन।
- अनियमित गैर-हैल्टिंग मशीनों को संभालने के लिए WFAR का परिचय।
प्रत्यक्ष Coq गणना: Coq प्रूफ असिस्टेंट के भीतर सीधे 181 मिलियन मशीनों की TNF गणना को सफलतापूर्वक लागू करना, जो पहले अत्यधिक गणना-गहन माना जाता था।

4. परिणाम (Results)

शोध पत्र निम्नलिखित मानों की पुष्टि करता है:

$S(5) = 47,176,870$ : यह सिद्ध करके कि 1989 की चैंपियन मशीन इस चरण संख्या पर रुकती है और अन्य सभी 181,385,788 मशीनें या तो पहले रुकती हैं या कभी नहीं रुकतीं।
$\Sigma(5) = 4,098$ : एक 5-स्टेट हैल्टिंग मशीन के लिए टेप पर 1 की अधिकतम संख्या।
$S(2, 4) = 3,932,964$ : 2-स्टेट, 4-सिंबल मशीनों के लिए मान।
$S(4) = 107$ : औपचारिक प्रमाणों के साथ पुनः सत्यापित, पिछले परिणामों की पुष्टि करता है।

डेटा आउटपुट:
लेखकों ने सभी 181,385,789 गणना की गई 5-स्टेट मशीनों, उनके हैल्टिंग स्टेटस और विशिष्ट ड décidéर की एक सूची निकाली है। यह डेटासेट सार्वजनिक रूप से उपलब्ध है और 5-स्टेट मशीनों पर किसी भी अवलोकन योग्य मीट्रिक की गणना करने की अनुमति देता है।

स्पोरैडिक मशीनें (Sporadic Machines):
13 "स्पोरैडिक मशीनें" (जैसे, "Skelet #1", "Skelet #17") सबसे कठिन थीं।

Skelet #1: एक ट्रांसलेटेड साइकलर जिसका प्री-पीरियड $\approx 5.41 \times 10^{51}$ चरण है।
Sकोलेट #10: एक डबल फाइबोनैकी काउंटर।
Skelet #17: पूर्णांकों की एक सूची पर जटिल ग्रे कोड रूपांतरण लागू करने वाली एक मशीन।

5. महत्व (Significance)

गणितीय सीमा (Mathematical Frontier): यह कार्य स्थापित करता है कि गणित में "सबसे छोटी खुली समस्या" (बजी बीवर के संदर्भ में) 5-स्टेट मशीनों के साथ नहीं है, बल्कि संभवतः 6-स्टेट मशीनों के साथ है (विशेष रूप से Antihydra जैसे "क्रिप्टिड्स", जो कोलेट्ज़ अनुमान से जुड़े हैं और संभवतः मानक ZF सेट थ्योरी में अप्रमाणित हैं)।
सहयोगात्मक विज्ञान: यह "ओपन-सोर्स" गणित की प्रभावकारिता को प्रदर्शित करता है, जहाँ वितरित, गैर-अकादमिक सहयोग उन समस्याओं को हल कर सकता है जो दशकों से रुकी हुई थीं।
AI बेंचमार्क: उत्पन्न ओपन प्रॉब्लम्स (क्रिप्टिड्स) और औपचारिक प्रमाण AI तर्क उपकरणों (reasoning tools) के लिए बेंचमार्क के रूप में कार्य करते हैं। शुरुआती परीक्षणों से पता चलता है कि AI सिस्टम $S(4)$ प्रमाण के पहले 100 लेम्मा में से 58% को हल करते हैं।
औपचारिक विधियाँ (Formal Methods): यह सैद्धांतिक कंप्यूटर विज्ञान में औपचारिक सत्यापन के पैमाने के लिए एक नया मानक स्थापित करता है, यह सिद्ध करता है कि विशाल कम्प्यूटेशनल खोजों को पूरी तरह से एक विश्वसनीय तार्किक ढांचे (logical framework) के साथ एकीकृत किया जा सकता है।

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