💻 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

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

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/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تدير سباقاً فوضوياً وهائلاً. المتسابقون هم روبوتات صغيرة وبسيطة تسمى آلات تورينج (Turing Machines). تمتلك هذه الروبوتات عقولاً محدودة جداً (بضع "حالات") وشريطاً طويلاً من الورق اللانهائي يبدأ فارغاً تماماً.

قواعد السباق بسيطة:

يقرأ الروبوت مكاناً ما، ويكتب رمزاً جديداً (0 أو 1)، ويتحرك يساراً أو يميناً، ويغير "مزاج" حالته الداخلية.
إذا واجه الروبوت مكاناً لا يعرف ماذا يفعل فيه، فإنه يتوقف (يتوقف عن العمل/Halt).
الهدف؟ معرفة أي روبوت يمكنه اتخاذ أكبر عدد من الخطوات قبل أن يتوقف.

هذه هي لعبة البيفر المشغول (Busy Beaver Game). السؤال هو: "ما هو أقصى عدد من الخطوات التي يمكن لروبوت يمتلك n من الحالات أن يتخذها قبل أن يتوقف؟"

لفترة طويلة، عرف الرياضيون الإجابات للروبوتات ذات 1، 2، 3، و4 حالات. ولكن بالنسبة للروبوتات ذات 5 حالات، كان الجواب لغزاً. كان الأمر يشبه محاولة تخمين الفائز في سباق خط النهاية فيه بعيد جداً لدرجة أنك لا تستطيع حتى رؤيته، وبعض العدائين قد يستمرون في الجري للأبد دون توقف.

الاختراق الكبير

هذه الورقة البحثية هي قصة كيف تمكن فريق ضخم من المتطوعين عبر الإنترنت، يسمى تعاون bbchallenge، من حل لغز الروبوتات ذات الـ 5 حالات أخيراً.

لقد أثبتوا أن الفائز يأخذ بالضبط 47,176,870 خطوة.

لكن هنا تكمن المفاجأة؛ لم يقوموا بمجرد التخمين أو تشغيل محاكاة. لقد استخدموا "محامياً رقمياً" صارماً للغاية يسمى Coq (مساعد إثبات) للتحقق من كل خطوة من خطوات منطقهم. إنه يشبه وجود قاضٍ آلي يقرأ دليل السباق بأكمله، سطراً بسطر، لضمان عدم وجود أخطاء. هذه هي المرة الأولى التي يتم فيها التحقق من رقم "بيفر مشغول" بهذه الطريقة.

كيف فعلوا ذلك؟ (التشبيه)

تخيل أن لديك مكتبة تحتوي على 16 تريليون كتاب. كل كتاب يصف روبوتاً مختلفاً. أنت بحاجة للعثور على الروبوت الذي يستمر لأطول فترة.

المشكلة: لا يمكنك قراءة 16 تريليون كتاب. بعض الروبوتات ستستمر لملايين السنين؛ وأخرى ستستمر للأبد.
الحل (الشكل الشجري الطبيعي - Tree Normal Form): أدرك الفريق أن العديد من الروبوتات هي مجرد "توائم" لبعضها البعض (تقوم بنفس الشيء، فقط بأسماء مختلفة). قاموا ببناء شجرة عائلة لتجميع هؤلاء التوائم معاً. هذا قلص المكتبة من 16 تريليون كتاب إلى 181 مليون كتاب يمكن إدارتها. لا يزال عدداً كبيراً، لكنه قابل للتنفيذ باستخدام الحواسيب.

بعد ذلك، بنوا آلة تصفية (خط إنتاج من "المقررين"). فكر في هذا كأنه سلسلة من نقاط التفتيش الأمنية:

كاشف الحلقات (The Loop Detector): "مهلاً، هذا الروبوت يمشي في دوائر! لن يتوقف أبداً. مستبعد." (هذا اصطاد الغالبية العظمى من الروبوتات).
مطابق الأنماط (The Pattern Matcher): "هذا الروبوت يكتب نمطاً متكرراً لن ينتهي أبداً. مستبعد."
خبير الرياضيات (The Math Prover): "هذا الروبوت يقوم بشيء معقد، لكن يمكننا إثبات رياضياً أنه لن يتوقف أبداً."

تم الإمساك بمعظم الروبوتات بواسطة أول نقطتي تفتيش. لكن 13 روبوتاً عنيداً (تسمى الآلات الشاذة/Sporadic Machines) كانت صعبة للغاية. لم تكن تدور في حلقات، ولم تتبع أنماطاً بسيطة. كانت مثل حيوانات برية يجب دراستها بشكل فردي.

أحد هذه الروبوتات، المسمى "Skelet #17"، كان هو "الوحش النهائي" (Final Boss). كان معقداً للغاية لدرجة أنه استلزم ورقة بحثية مخصصة لشرح كيفية عمله. لقد كان الأخير الذي تم ترويضه.

"الكريبتيدات" (الوحوش في الغابة)

تتحدث الورقة أيضاً عن الكريبتيدات (Cryptids). في عالم "بيغ فوت" أو "وحش لوخ نيس"، هذه هي المخلوقات التي يعتقد الناس بوجودها لكن لا يمكنهم إثبات ذلك.
في عالم "البيفر المشغول"، الكريبتيد هو روبوت نعتقد أنه يستمر للأبد، لكننا لا نستطيع إثبات ذلك بعد.

وجد الفريق أنه بالنسبة لـ روبوتات الـ 6 حالات، هناك العديد من الكريبتيدات.
أحد هذه الكريبتيدات مرتبط بمعضلة رياضية شهيرة غير محلولة (حدسية كولاتز/Collatz Conjecture). إثبات ما إذا كان هذا الروبوت سيتوقف أم لا هو أمر بصعوبة حل تلك المعضلة الرياضية.
يمزح المؤلفون بأن "أصغر مشكلة مفتوحة في الرياضيات" قد تكون مخبأة داخل روبوت من 6 حالات.

لماذا يجب أن تهتم؟

إنه جهد جماعي: لم يتم هذا العمل بواسطة عبقري واحد يرتدي معطف المختبر. بل تم بواسطة مئات الأشخاص (طلاب، مهندسين، هواة) يتحدثون عبر "ديسكورد"، ويشاركون الأكواد، ويساعدون بعضهم البعض. إنه يشبه مشروع برمجيات مفتوحة المصدر ضخم، ولكن للرياضيات.
إنه اختبار للذكاء الاصطنا_ي: يستخدم المؤلفون هذا الإثبات الآن لاختبار الذكاء الاصطناعي. هل يمكن للذكاء الاصطناعي فهم المنطق وراء هذه الروبوتات؟ حتى الآن، يؤدي الذكاء الاصطناعي بشكل جيد، لكنه تحدٍ صعب.
حدود المعرفة: توضح لنا هذه الورقة حافة ما يمكننا معرفته. يمكننا إثبات الإجابة لـ 5 حالات، ولكن بالنسبة لـ 6 حالات، تصبح المشكلات صعبة للغاية لدرجة أنها قد تكون مستحيلة الحل بقواعد الرياضيات الحالية لدينا.

الخلاصة

نجح الفريق في مطاردة بطل سباق "البيفر المشغول" ذي الـ 5 حالات. لقد أثبتوا أنه يستمر لـ 47,176,870 خطوة ثم يتوقف. لقد فعلوا ذلك من خلال بناء حصن رقمي من المنطق لا يمكن لأحد الجدال فيه.

إنه انتصار للفضول البشري، وللتعاون، ولقوة الحواسيب في مساعدتنا على فهم حدود الكون. وبينما حلوا لغز الـ 5 حالات، فقد وجدوا أيضاً غابة جديدة تماماً من "الكريبتيدات" في عالم الـ 6 حالات، تنتظر الجيل القادم من المستكشفين لحلها.

إليك ملخص تقني مفصل لورقة البحث "تحديد قيمة Busy Beaver الخامسة" (Determination of the fifth Busy Beaver value) من قبل تعاون bbchallenge.

1. بيان المشكلة

تتناول الورقة تحديد دالة Busy Beaver $S(n)$ ، والتي تُعرف بأنها أقصى عدد من الخطوات التي يمكن لآلة تورينج (Turing machine) مكونة من $n$ من الحالات ورمزين يمكنها تنفيذها قبل التوقف، بدءاً من شريط يحتوي على جميع الأصفار.

السياق: دالة $S(n)$ هي دالة غير قابلة للحوسبة. قبل هذا العمل، تم إثبات قيم $S(1)$ حتى $S(4)$ فقط بشكل صارم ( $S(4)=107$ ).
التحدي: يتطلب تحديد $S(5)$ تحليل سلوك التوقف لمساحة بحث هائلة. وبينما تعمل الآلة الفائزة (التي اكتُشفت في عام 1989) لمدة 47,176,870 خطوة، فإن الصعوبة الرئيسية تكمن في إثبات أن لا توجد آلة أخرى مكونة من 5 حالات تعمل لفترة أطول أو تتوقف لاحقاً. يتضمن ذلك إثبات حالة عدم التوقف لملايين الآلات، والتي يُظهر بعضها سلوكيات معقدة وفوضوية تحاكي فرضيات رياضية صعبة (مثل فرضية غولدباخ أو فرضية ريمان).
الهدف: إثبات أن $S(5) = 47,176,870$ و $S(2, 4) = 3,932,964$ (لآلات مكونة من حالتين و4 رموز) باستخدام برهان تم التحقق منه آلياً.

2. المنهجية

استخدم المؤلفون جهداً تعاونياً ضخماً مدمجاً مع التحقق الرسمي باستخدام مساعد الإثبات Coq. وتتكون المنهجية من ثلاث ركائز أساسية:

أ. تقليص مساحة البحث: الصيغة الشجرية الطبيعية (Tree Normal Form - TNF)

لجعل المشكلة قابلة للمعالجة حاسوبياً، استخدم المؤلفون تعداد الصيغة الشجرية الطبيعية (TNF).

التقليص: بدلاً من تحليل العدد الإجمالي النحوي لـ $\approx 1.67 \times 10^{13}$ (16.7 تريليون) من آلات الـ 5 حالات الممكنة، يقوم TNF بتقليص مساحة البحث إلى 181,385,789 آلة فريدة.
التقنية: يقوم TNF ببناء الآلات بشكل متكرر عبر تعريف الانتقالات فقط عند الضرورة، مما يؤدي إلى استبعاد الانتقالات غير القابلة للوصول وإلغاء الآلات التي ليست سوى تبديلات للحالات أو الرموز.
التنفيذ: تم تنفيذ عملية تعداد وتتبع TNF بالكامل مباشرة داخل Coq، وهو ما يعد خروجاً كبيراً عن الطرق السابقة التي اعتمدت على تعداد غير مُتحقق منه خارجياً.

ب. خط أنابيب "المقرر" (The Decider Pipeline)

جوهر البرهان هو خط أنابيب من الخوارزميات ("المقررات" أو deciders) التي تحاول تحديد ما إذا كانت الآلة ستتوقف أم ستدخل في حلقة مفرغة. وبما أن مشكلة التوقف غير قابلة للتقرير، فإن هذه الأدوات هي "مقررات جزئية"؛ فإذا فشل أحدها، تُمرر الآلة إلى التالي.

الحلقات (الخوارزمية 1): تكتشف الدورات القياسية (Cyclers) والدورات ذات الانتقال المكاني (Translated Cyclers) من خلال تحليل سجلات (state-symbol-head position) بدلاً من تكوينات الشريط الكاملة. وقد حلت هذه الطريقة 95.48% من الآلات غير المتوقفة.
مجموعة المواقع المغلقة لـ n-gram (الاسم: NGramCPS): هي تجريد لتقنية "مجموعة المواقع المغلقة". وهي تتبع التكوينات المحلية (n-grams من رموز الشريط) لإثبات أن الآلة تدخل في مجموعة مغلقة من الحالات لا يمكنها الهروب منها إلى انتقال التوقف. وقد حلت هذه الطريقة 99.89% من الآلات المتبقية غير المتوقفة.
- التعزيز: قام المؤلفون بتعزيزها باستخدام "التاريخ ثابت الطول" و"تاريخ الاستخدام الأخير (LRU)" للتعامل مع الآلات ذات الاعتمادات المعقدة على الشريط.
قائمة الكلمات المتكررة (RepWL): تستخدم التعبيرات المنتظمة لتمثيل تكوينات الشريط. إذا تكرر كتلة من الرموز أكثر من حد معين $T$ ، فإنه يتم التعامل معها كتكرار لانهائي. وتتعامل هذه الطريقة مع الآلات ذات النمو الدوري أو الفركتلي (fractal-like) في الشريط.
اختزال الآلات ذات المجموعات المنتهية (FAR) والـ (WFAR):
- FAR: تقنية (co-CTL) (لغة الشريط المغلقة) باستخدام الآلات المحدودة غير الحتمية (NFA) لإثبات أن مجموعة تكوينات التوقف منفصلة عن التكوين الأولي.
- WFAR: امتداد باستخدام الآلات المحدودة الموزونة للتعامل مع اللغات غير المنتظمة، مما يسمح بإثبات عدم التوقف للآلات ذات الثوابت الأكثر تعقيداً.
الآلات الشاذة (Sporadic Machines): بالنسبة للـ 13 آلة التي قاومت جميع المقررات الآلية، قام الفريق ببناء براهين فردية مصممة يدوياً في Coq لإثبات عدم التوقف. تُظهر هذه الآلات سلوكيات فريدة (مثل عدادات فيبوناتشي، وتشفير كود غراي (Gray code) المعقد، وحلقات ما قبل دورية ضخمة).

ج. التحقق الرسمي (Coq-BB5)

البرهان: العملية بأكملها مغلفة في Coq-BB5، وهو نص برمجي رسمي للإثبات.
الانعكاس (Reflection): يستخدم البرهان "البرهان بالانعكاس"، حيث يقوم Coq بتشغيل الخوارزميات المتحقق منها (تعداد TNF والمقررات) ويستخدم مخرجاتها لبناء النظرية النهائية.
الثقة: البديهية الخارجية الوحيدة المستخدمة هي functional_extensionality_dep وهي قياسية ومتسقة. يستغرق البرهان حوالي 45 دقيقة للعمل على 13 نواة.

3. المساهمات الرئيسية

أول تحقق رسمي لقيمة Busy Beaver: هذه هي المرة الأولى التي يتم فيها تحديد قيمة Busy Beaver ببرهان تم التحقق منه آلياً، مما يلغي الخطأ البشري في التحقق من ملايين الحالات.
بحث تعاوني ضخم: استخدم المشروع منصة bbchallenge.org، حيث قام مئات المساهمين (معظمهم من غير الأكاديميين) بتطوير المقررات، وتحليل "الآلات الصعبة" (holdouts)، ومشاركة الأكواد بلغات مختلفة (C++، Python، Rust، Haskell، إلخ).
ابتكارات خوارزمية:
- تطوير الخوارزمية 1 لكشف الحلقات باستخدام تحليل السجل (transcript analysis).
- تحسين NGramCPS مع تعزيزات الشريط (LRU/التاريخ الثابت).
- تقديم WFAR للتعامل مع الآلات غير المنتظمة غير المتوقفة.
التعداد المباشر في Coq: النجاح في تنفيذ وتشغيل تعداد TNF لـ 181 مليون آلة مباشرة داخل مساعد الإثبات Coq، وهو إنجاز كان يُعتقد سابقاً أنه مكثف حاسوبياً للغاية.

4. النتائج

تؤكد الورقة القيم التالية:

$S(5) = 47,176,870$ : تم إثبات ذلك من خلال إظهار أن الآلة البطلة لعام 1989 تتوقف عند عدد الخطوات هذا، وأن جميع الآلات الـ 181,385,888 الأخرى إما تتوقف في وقت أبكر أو لا تتوقف أبداً.
$\Sigma(5) = 4,098$ : أقصى عدد من الواحدات (1s) على الشريط لآلة مكونة من 5 حالات تتوقف.
$S(2, 4) = 3,932,964$ : القيمة لآلات مكونة من حالتين و4 رموز.
$S(4) = 107$ : تمت إعادة التحقق منها ببراهين رسمية، مما أكد النتائج السابقة.

مخرجات البيانات:
استخرج المؤلفون قائمة بجميع الـ 181,385,879 آلة (من 5 حالات) المعددة، وحالة التوقف الخاصة بكل منها، والمقرر المحدد الذي حلها. هذه المجموعة من البيانات متاحة للجمهور وتسمح بحساب أي مقياس قابل للرصد على آلات الـ 5 حالات.

الآلات الشاذة (Sporadic Machines):
كانت الـ 13 آلة الشاذة (مثل "Skelet #1"، "Skelet #17") هي الأصعب في الحل.

Skelet #1: دورة مترجمة (Translated Cycler) مع فترة ما قبل دورية تبلغ $\approx 5.41 \times 10^{51}$ خطوة.
Skelet #10: عداد فيبوناتشي مزدوج.
Skelet #17: آلة تنفذ تحويلاً معقداً لكود غراي (Gray code) على قائمة من الأعداد الصحيحة.

5. الأهمية

الحدود الرياضية: يوضح هذا العمل أن "أصغر مشكلة مفتوحة" في الرياضيات (في سياق Busy Beaver) لا تكمن في آلات الـ 5 حالات، بل على الأرجح في آلات الـ 6 حالات (تحديداً "الكريبتيدز" مثل Antihydra، المرتبطة بفرضية كولاتز والتي من المرجح أنها غير قابلة للإثبات في نظرية مجموعات ZF القياسية).
العلوم التعاونية: يبرهن على فعالية "الرياضيات مفتوحة المصدر"، حيث يمكن للتعاون الموزع وغير الأكاديمي حل مشكلات كانت متعثرة لعقود.
معيار للذكاء الاصطناعي: تعمل المشكلات المفتوحة الناتجة (الكريبتيدز) والبراهين الرسمية كمعايير لأدوات الاستدلال في الذاء الاصطناعي. أظهرت الاختبارات المبكرة أن أنظمة الذكاء الاصطناعي تحل 58% من أول 100 لِمّة (lemma) من برهان $S(4)$ .
الأساليب الرسمية: يضع معياراً جديداً لنطاق التحقق الرسمي في علوم الحاسوب النظرية، مما يثبت أن عمليات البحث الحاسوبي الضخمة يمكن دمجها بالكامل في إطار منطقي موثوق.

باختصار، تحل الورقة مشكلة عمرها 40 عاماً في نظرية القابلية للحساب من خلال الجمع بين الابتكار الخوارزمي، والحوسبة الموزعة الضخمة، والتحقق الرسمي الصارم، مما يغلق فصلاً من فصول الـ Busy Beavers لـ 5 حالات.