💻 computer science

Formal Verification of Minimax Algorithms

تقدم هذه الورقة تحققاً رسمياً لخوارزميات بحث "مينيمكس" (minimax) مع تقليم "ألفا-بيتا" (alpha-beta) وجداول النقل (transposition tables) باستخدام نظام "دافني" (Dafny)، حيث تقدم معيار صحة قائماً على الشاهد (witness-based) ينجح في إثبات نوع عملي واحد بينما يكشف عن انتهاك للصحة في نوع آخر.

المؤلفون الأصليون: Wieger Wesselink, Kees Huizing, Huub van de Wetering

نُشر 2026-04-23

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

CC BY 4.0

المؤلفون الأصليون: Wieger Wesselink, Kees Huizing, Huub van de Wetering

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

تخيل أنك تلعب لعبة لوحية معقدة مثل الشطرنج أو الداما ضد كمبيوتر فائق الذكاء. لاتخاذ قراره بشأن حركته التالية، لا يقوم الكمبيوتر بمجرد التخمين؛ بل يبني "شجرة" ضخمة من الاحتمالات في عقله. هو يسأل نفسه: "إذا ذهبت إلى هنا، ستذهب أنت إلى هناك، ثم سأذهب أنا إلى هناك..." وهكذا، محاولاً توقع النتيجة الأفضل. هذا ما يسمى بـ خوارزمية المينيمكس (Minimax algorithm).

ومع ذلك، فإن بناء هذه الشجرة بالكامل للعبة مثل الشطرنج أمر مستحيل لأنها ضخمة جداً. لذا، تستخدم الحواسيب حِيلاً لتسريع العملية:

تقليم ألفا-بيتا (Alpha-Beta Pruning): مثل المحقق الذي يتجاهل الأزقة المسدودة، يتوقف الكمبيوتر عن البحث في المسارات التي تبدو سيئة بوضوح.
جداول الانتقال (Transposition Tables): هذا نظام "الملاحظات اللاصقة". إذا كان الكمبيوتر قد حسب وضعية معينة للوحة من قبل، فإنه يكتفي بالبحث عن الإجابة في الملاحظة اللاصقة بدلاً من إعادة الحساب.

المشكلة:
هذه الحيل ذكية للغاية، لكنها فوضوية أيضاً. نظرًا لأن الكمبيوتر يتخطى بعض الخطوات ويعيد استخدام ملاحظات قديمة، فمن الصعب رياضياً إثبات أن الإجابة النهائية صحيحة بالفعل. أحياناً، قد يتخطى الكمبيوتر مساراً كان من شأنه أن يؤدي إلى الفوز، فقط لأن ملاحظة قديمة أخبرته بالتوقف عن البحث.

الحل (مهمة الورقة البحثية):
أراد مؤلفو هذه الورقة استخدام "آلة إثبات رياضية" (أداة تسمى Dafny) للتحقق مما إذا كانت خوارمايات لعب الألعاب هذه تقول الحقيقة بالفعل. لم يكتفوا بمجرد إجراء اختبارات (والتي قد تفوت الأخطاء النادرة)؛ بل حاولوا إثبات أن الكود مثالي.

الفكرة الكبرى: "الشاهد" (The Witness)
الجزء الأصعب كان التعامل مع "الملاحظات اللاصقة" (جداول الانتقال). عندما يعيد الكمبيوتر استخدام إجابة قديمة، فالأمر يشبه النظر إلى خريطة لمدينة زرتها العام الماضي. ولكن ماذا لو تغيرت المدينة؟ أو ماذا لو نظرت فقط إلى جزء من المدينة في المرة الماضية؟

اخترع المؤلفون طريقة جديدة للتحقق من الصحة تسمى "الشاهد" (Witness).

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

التجربة: منافسان
أخذ المؤلفون نسختين شائعتين من هذه الخوارزمية وأخضعاها لاختبار "الشاهد".

1. نسخة ويكيبيديا (NegamaxTTW)

كيف تعمل: هي نسخة حذرة نوعاً ما. عندما ترى ملاحظة لاصقة، تتحقق: "هل تضمن لي هذه الملاحظة التوقف عن البحث الآن؟". إذا كانت الملاحظة غامضة أو من سياق مختلف، فإنها تتجاهلها وتقوم بالحساب الكامل.
النتيجة: نجاح. نجح المؤلفون في إثبات أن هذه النسخة تنتج دائماً "شاهداً" صالحاً باستخدام آلة Dafy. إنها آمنة، موثوقة، وسليمة رياضياً.

2. نسخة مارسلاند (NegamaxTTM)

كيف تعمل: هذه النسخة أكثر هجومية. عندما ترى ملاحظة لاصقة تقول "القيمة هي 3 على الأقل"، فإنها تقلص نافذة البحث فوراً، معتقدة: "رائع، لست بحاجة للنظر في أي شيء أقل من 3!".
النتيجة: فشل. وجد المؤلفون سيناريو محدد (مثال مضاد) حيث أدت هذه الهجومية إلى نتائج عكسية.
- الفخ: رأى الكمبيوتر ملاحظة تقول "القيمة هي 3 على الأقل". استخدم هذا للتوقف عن البحث في فرع يحتوي في الواقع على قيمة قدرها 1 (وهي قيمة أفضل للخصم). ولأنه توقف عن البحث، فقد فاتته الحركة الأفضل وأعطى إجابة خاطئة.
- الإثبات: لم يستطع الكمبيوتر إنتاج "شاهد" لإجابته. كان الأمر أشبه بمحقق يدعي حل قضية ولكنه يرفض إظهار الأدلة لأنه توقف عن البحث مبكراً جداً.

لماذا يهم هذا؟
هذه الورقة البحثية تشبه مفتش السلامة لـ "الصندوق الأسود" للذكاء الاصطناعي الخاص بالألعاب.

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

باختصار: بنى المؤلفون مجهراً رياضياً لفحص كود لعب الألعاب. لقد أثبتوا أن إحدى الطرق الشائعة آمنة وسليمة، لكنهم ضبطوا طريقة أخرى شائعة وهي ترتكب خطأً دقيقاً وخطيراً بسبب الثقة في ملاحظاتها بسرعة كبيرة. هذا يضمن أن الذكاء الاصطناي الذي نلعب ضده يلتزم بقواعد المنطق، وليس مجرد التخمين.

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

تُعد خوارزميات "مينماكس" (Minimax)، ولا سيما تلك المعززة بـ تقليم ألفا-بيتا (alpha-beta pruning) وجداول الانتقال (transposition tables - TT)، هي العمود الفقري لمحركات ألعاب الألعاب الكلاسيكية (مثل الشطرنج والداما). ورغم انتشارها الواسع، إلا أن هذه الخوارقات يصعب التنبؤ بسلوكها بدقة بسبب:

التعقيد والتحسين: فهي تعتمد على استدلالات معقدة وتقليم عدواني لتحسين الكفاءة.
البحث المحدود بالعمق: على عكس البحث النظري غير المحدود بالعمق، تستخدم المحركات العملية حدوداً للعمق. وهذا يخلق أشجاراً "مبتورة" حيث يتم إعادة استخدام النتائج المخزنة من عمليات بحث أعمق في أجزاء مختلفة من الشجرة.
الغموض الدلالي: إن التفاعل بين القيم المخزنة (المخزنة بأعماق مختلفة وتحت نوافذ بحث مختلفة) وسياق البحث الحالي يكسر دلالات عبور الأشجار البسيطة المستخدمة لتبرير صحة خوارزمية "مينماكس" القياسية.
محدودية الاختبار: من الصعب اكتشاف الأخطاء غير الواضحة الناتجة عن هذه التفاعلات من خلال الاختبار وحده، لأنها غالباً ما تعتمد على تسلسلات محددة من حالات إصابة الجدول (table hits) وشروط التقليم.

يعالج البحث الافتقار إلى أساس رسمي صارم للتحقق من صحة خوارزميات "مينماكس" المعتمدة على الجداول الانتقالية والبحث المحدود بالعمق.

2. المنهجية

استخدم المؤلفون نظام التحقق Dafny، وهو لغة برمجة ومتحقق يعتمد على منطق "فلويد-هوار" (Floyd-Hoare logic)، للتحقق رسمياً من التنفيذات الأمرية لخوارزميات "مينماكس" و"نيجاماكس" (negamax).

الابتكارات المنهجية الرئيسية:

معيار الصحة القائم على الشاهد (Witness-Based Correctness Criterion):
التحديد الجوهري هو تعريف معنى "الصحة" عندما تعيد عملية البحث استخدام نتائج مخزنة من أعماق مختلفة. قدم المؤلفون معيار صحة قائماً على الشاهد:
- المفهوم: تكون القيمة المعادة صحيحة إذا وجد "شاهد" (witness tree) — وهو توسيع صريح لشجرة اللعبة المبتورة التي تدمج مسار البحث الحالي مع الأشجار الفرعية الضمنية لمدخلات جدول الانتقال المعاد استخدامها.
- التعريف الرسمي: تكون النتيجة صالحة إذا وجد شاهد $u'$ $u^{'}$ بحيث:
  1. $u'$ هي شجرة فرعية من الشجرة الأصلية $u$ .
  2. $u'$ تحتوي على التقطيع الكامل لـ $u$ عند العمق $d$ .
  3. $u'$ تحترم قاعدة تضمين الأبناء "الكل أو لا شيء" (لا توجد مجموعات فرعية عشوائية من الأبناء).
  4. قيمة الخوارزمية المعادة تطابق نتيجة "نيجاماكس ألفا-بيتا" المحسوبة على الشاهد $u'$ .
نمذجة جداول الانتقال (Transposition Tables):
نمذج المؤلفون جدول الانتقال (TT) كخريطة جزئية من العقد إلى مدخلات تحتوي على قيمة، وعمق، وعلامة (دقيقة Exact، أو حد أدنى Lower Bound، أو حد أعلى Upper Bound). وقد اعتمدوا نموذجاً متسامحاً (permissive model) حيث يمكن لمحتويات الجدول أن تتغير بشكل عشوائي (لمحاكاة تصادمات الهاش وتجاوز البيانات) طالما أن كل مدخل في الجدول مبرر بواسطة شاهد صالح ما.
التنفيذ:
قاموا بترجمة الكود الزائف (pseudocode) لخوارزميات "مينماكس"، و"نيجاماكس"، ونوعين محددين من المتغيرات المعتمدة على جداول الانتقال إلى لغة Dafny. تضمنت عملية التحقق تعريف ثوابت الحلقات (loop invariants)، والشروط المسبقة واللاحقة، ومعمات (lemmas) محددة للتعامل مع المكممات (quantifiers) المعقدة المتأصلة في هياكل أشجار الألعاب.

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

التعريف الرسمي للصحة القائمة على الشاهد: يقدم البحث معيار صحة جديداً ومرناً يأخذ في الاعتبار التفاعل المعقد بين البحث المحدود بالعمق، وتقليم ألفا-بيتا، وإعادة استخدام جداول الانتقال. هذا ينتقل بما هو أبعد من مجرد تتبع التنفيذ إلى الخصائص الهيكلية لأشجار الألعاب الموسعة.
التحقق الآلي من NegamaxTTW: نجح المؤلفون في تقديم إثبات كامل وصحيح لـ NegamaxTTW، وهو متغير شائع في المصادر المجتمعية (مثل ويكيبيديا). هذا هو أول إثبات رسمي لصحة بحث "نيجاماكس" المحدود بالعمق مع تقليم ألفا-بيتا وجداول الانتقال.
اكتشاف مثال مضاد لـ NegamaxTTM: حاول المؤلفون التحقق من Negase-maxTTM (متغير يعتمد على أعمال مارسلاند). فشل التحقق، مما أدى إلى بناء مثال مضاد ملموس. يوضح هذا المثال المضاد أن NegamosTTM يمكن أن يعيد قيماً تنتهك معيار الصحة القائم على الشاهد.
التحليل المقارن: يقدم البحث مقارنة تقنية مفصلة تشرح لماذا تعمل إحدى الخوارزميات وتفشل الأخرى، مع تسليط الضوء على الاختلافات الدقيقة في استراتيجيات البحث في الجداول وإدارة النوافذ.

4. النتائج

النجاح: NegamaxTTW

التحقق: نجح متحقق Dafny في إثبات صحة NegamaxTTW في حوالي 4 ثوانٍ.
الآلية: تستخدم هذه الخوارزمية استراتيجية بحث في الجدول محافظة. فهي لا تعيد قيمة مخزنة إلا إذا كانت تضمن فوراً حدوث تقليم (أي أن القيمة المخزنة تقع تماماً خارج نافذة ألفا-بيتا الحالية). إذا لم تضمن القيمة المخزنة حدوث تقليم، فإن الخوارزمية تتجاهلها وتجري بحثاً كاملاً. تضمن هذه الاستراتيجية المحافظة وجود شجرة شاهد صالحة دائماً.

الفشل: NegamaxTTM

المثال المضاد: حدد المؤلفون سيناريو تعيد فيه NegamaxTTM قيمة غير صحيحة.
- السيناريو: تم البحث في عقدة $v$ عند العمق 4 بنافذة ضيقة $(0, 2)$ ، مما أعاد حداً أدنى قدره 3. لاحقاً، تم البحث في $v$ عند العمق 2 بنافذة أوسع $(0, 5)$ .
- الخلل: تعيد NegamaxTTM الحد الأدنى (3) من البحث السابق لتضييق النافذة الحالية إلى $(3, 5)$ . هذا التضييق المبكر يتسبب في تقليم فرع كان من الممكن أن يؤدي إلى قيمة أفضل (1)، مما نتج عنه قيمة معادة قدرها 2.
- الانتهاك: لا يوجد شجر شاهد صالح يبرر القيمة المعادة وهي 2. لقد قامت الخوارزمية فعلياً بـ "إخفاء" حركة أفضل عبر إعادة استخدام حد تم حسابه تحت قيود مختلفة.
السبب الجذري: يكمن الانحراف في مرحلة البحث في الجدول (Table Lookup). تستخدم NegomaxtTM الحدود المخزنة لتقليص نافذة البحث، وهو أمر غير آمن عندما تم حساب الحد تحت نافذة مختلفة (أضيق).

5. الأهمية والأثر

أساس صارم لذكاء الألعاب: يوفر هذا العمل أول أساس دلالي رسمي للاستدلال على صحة البحث المحدود بالعمق مع جداًول الانتقال، وهو مكون حيوي لمحركات الألعاب الحديثة.
التحقق من الممارسات الشائعة: من خلال التحقق من NegamaxTTW، يؤكد البحث أن التنفيذ "على طراز ويكيبيديا" سليم رياضياً بموجب المعيار المقترح.
كشف الأخطاء الدقيقة: يوضح المثال المضاد لـ NegamaxTTM أن حتى الخوارزميات المعروفة في الأدبيات يمكن أن تحتوي على عيوب منطقية دقيقة تكون غير مرئية للاختبار ولكنها قاتلة للصحة الرسمية. إنه يسلط الضوء على خطورة إعادة استخدام الحدود عبر نوافذ بحث مختلفة دون شروط صارمة.
عرض القدرات الأدواتية: يستعرض البحث قدرة Dafny على التعامل مع الخوارزميات التكرارية والحالة المعقدة ذات الثوابت غير البديهية، مما يجعله نموذجاً للتحقق من خوارزميات البحث في الذكاء الاصطناعي الأخرى (مثل SSS* و MTD(f)).
المصدر المفتوح: جميع المواد، بما في ذلك براهين Dafny وتطبيقات Python القابلة للتنفيذ، متاحة علناً لتعزيز قابلية التكرار ومزيد من البحث.

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