Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis

دليل المحقق لجعل الأشياء تتطابق

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

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

الاكتشاف الكبير للورقة: تعليم روبوت بناء محلل الألغاز الخاص به

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

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

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

كيف "فكر" الروبوت

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

استخدم "سنارك" طريقة تسمى الجداول الاستنتاجية (deductive tableaux). تخيل سبورة بيضاء بها عمودان: "ما نعرفه" (الادعاءات) و"ما نحتاج لإيجاده" (الأهداف).

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

خدعة "البيئة"

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

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

النتيجة النهائية: وصفة جديدة

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

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

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

لماذا هذا مهم (ولماذا ليس سحرًا بعد)

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

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