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

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

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

لم يكتفِ الباحثون بالتخمين بأن هذا سيعمل، بل أثبتوا ذلك رياضياً بأنه سليم وبنوا أداة لاختباره. وعندما اختبرت Tessa مقابل أفضل الأدوات الحالية في بعض السيناريوهات الصعبة والمزدحمة (مثل نموذج يحتوي على 17 معالجاً أو 10 طوابير انتظار)، كانت Tessa أسرع بأكثر من 100 مرة. وفي اختبار محدد يتضمن أفقاً قدره 500 خطوة، كانت أسرع بأكثر من 300 مرة. تُظهر الورقة البحثية أنه من خلال تغيير كيفية تمثيلنا للمشكلة — من خريطة متفرقة إلى كتلة بيانات كثيفة وقابلة للتوازي — يمكننا إطلاق القدرة على التحقق من أنظمة كانت في السابق أكبر من أن يتم فحصها. إنها ليست عصا سحرية تصلح لكل شيء (فهي تعمل بشكل أفضل في الأنظمة الكثفة والمزدحمة، وليس المتفرقة)، لكنها تفتح ساحة لعب جديدة تماماً لحل مشكلات كانت في السابق بعيدة المنال.

قصة Tessa: تحويل الفوضى إلى رقصة

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

لمعرفة احتمال أن ينتهي الجميع خلال فترة زمنية معينة، تحاول الأدوات التقليدية سرد كل مجموعة من الحالات. إذا كان لديك 10 أساتذة، فهذا يعني $3^{10}$ (59,049) تركيبة. وإذا كان لديك 20، فهذا يعني أكثر من 3 مليارات. تحاول الأدوات التقليدية تخزين هذه التركيبات في قائمة متفرقة ضخمة (مثل قاموس يحتوي على صفحات بيضاء في معظمها). هذا يعمل بشكل جيد للمجموعات الصغيرة، ولكن عندما تصبح المجموعة كبيرة والتفاعلات فوضوية (كثيفة)، تصبح القائمة ضخمة جداً بحيث لا تسعها الذاكرة، ويتوقف الكمبيوتر عن العمل.

رؤية Tessa: المكعب الفائق
تنظر Tessa إلى هذه المشكلة بشكل مختلف. بدلاً من القائمة، ترى حالات الأساتذة كـ تنسور كثيف — شبكة متعددة الأبعاد. إذا كان لديك 10 أساتذة، فإن Tessa لا تصنع قائمة من 59,049 عنصراً؛ بل تنشئ مكعباً ذا 10 أبعاد حيث لكل جانب 3 خانات. إنه يشبه مكعب روبيك، ولكن مع 10 طبقات بدلاً من 3.

لماذا هذا أمر رائع؟ لأن بطاقات الرسوميات الحديثة (GPUs) مصممة للتعامل مع هذه المكعبات. فهي مصممة لأداء نفس العملية الرياضية على ملايين الأرقام في وقت واحد. تقوم Tessa بترجمة قواعد الأساتذة (منطق "إذا-فإن" الخاص بسلسلة ماركوف) إلى مجموعة من التعليمات لهذا المكعب. وبدلاً من المرور عبر المتاهة خطوة بخطوة، تأمر Tessa وحدة معالجة الرسوميات بـ "ضغط" المكعب بأكمله دفعة واحدة.

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

النتائج: تسريع الزمن
اختبر الباحثون Tessa على ثلاث مشكلات شهيرة "صعبة" من الأدبيات العلمية:

1. الطوابير (Queues): تخيل 10 طوابير مختلفة من الناس ينتظرون الخدمة. كانت Tessa أسرع بأكثر من 100 مرة من أفضل أداة تالية لها.
2. مصانع الطقس (Weather Factories): نموذج حيث تتنقل المصانع بين العمل والإضراب بناءً على الطقس. مرة أخرى، كانت Tessa أسرع بأكثر من 100 مرة.
3. بروتوكول هيرمان (Herman's Protocol): مشكلة كلاسيكية حول معالجات تحاول الاتفاق على قائد. هنا، كانت Tessa أسرع بأكثر من 300 مرة من المنافسين عند النظر إلى 500 خطوة في المستقبل.

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

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

في الورقة، استخدموا هذا لحل مشكلة "حجر نرد كونث-ياو" (Knuth-Yao die roller). أرادوا إيجاد الانحياز المثالي لعملتين (قيمتان $p$ و $q$) لجعل الكمبيوتر يرمي حجر نرد عادلاً. تعاملت Tessa مع انحيازات العملات كأزرار يمكنها تدويرها. قامت بحساب كيف يؤثر تغيير الأزرار على النتيجة، ثم قامت تلقائياً بتعديلها لتقليل الخطأ. لقد وجدت القيم المثالية ($p=0.5$ و $q=0.5$) في ثوانٍ معدودة، مما يظهر أن Tessa يمكن استخدامها للتحسين (optimization)، وليس للتحقق فقط.

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