Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
تقدم الورقة البحثية Apply2Isar، وهي أداة تقوم تلقائياً بتحويل براهين نمط "apply" الإجرائية في Isabelle/HOL إلى براهين Isar إعلانية مقروءة ومتينة، وتثبت فعاليتها من خلال التقييم على مجموعة مرجعية كبيرة من أرشيف البراهين الرسمية في Isabelle.
المؤلفون الأصليون:Sage Binder, Hanna Lachnitt, Katherine Kosaian
إليك شرح لورقة بحث "Apply2Isar" باستخدام لغة بسيطة وتشبيهات إبداعية.
المشكلة: "المسودة العشوائية" مقابل "المخطوطة المنظمة"
تخيل أنك عالم رياضيات تحاول حل لغز معقد. لديك طريقتان لتدوين حلك:
أسلوب "Apply" (المسودة العشوائية): يشبه هذا دفتر ملاحظات فوضوي وسريع. أنت تصرخ بالأوامر في وجه حاسوبك: "جرب هذا! لا، جرب ذاك! حسناً، الآن افعل هذا!". هذا الأسلوب يعمل بشكل رائع أثناء محاولتك فهم الأمور لأنه سريع ومرن، ولكن بمجرد انتهائك، تكون الملاحظات كارثية. إذا حاولت أنت أو أي شخص آخر قراءتها بعد أسبوع، ستكون كابوساً. وإذا غيرت قاعدة واحدة في اللغز، فقد ينكسر تسلسل الأوامر بالكامل بطريقة تجعل الأمر غير مفهوم، ولن تدرك سبب حدوث ذلك.
أسلوب "Isar" (المخطوطة المنظمة): يشبه هذا قصة مكتوبة بجمال أو مخطوطة رسمية. إنه يُقرأ كأنه مقال منطقي: "أولاً، نحن نعلم أن س. وبسبب س، يمكننا استنتاج ص. لذلك، فإن ع هي حقيقة". إنه سهل القراءة، سهل الفهم، ومتين جداً. إذا غيرت قاعدة ما، سينكسر السياق بطريقة واضحة وسهلة الإصلاح.
المعضلة: يفضل معظم الناس كتابة الملاحظات "العشوائية" أولاً لأنها أسرع لاستكشاف الأفكار. لكن "مخطوطة Isar" هي ما يرغب الجميع في قراءته والاحتفاظ به للأبد. المشكلة هي أن تحويل المسودة العشوائية إلى مخطوطة نظيفة يتطلب جهداً هائلاً؛ إذ يتعين عليك إعادة كتابة كل خطوة يدوياً، وهو أمر ممل ومعرض للخطأ البشري.
الحل: Apply2Isar (المترجم السحري)
بنى المؤلفون أداة تسمى Apply2Isar. فكر فيها كأنها مترجم ذكي أو كاتب ظل.
كيف تعمل: تقوم بتغذية الأداة بكود "المسودة العشوائية" الخاص بك (إثبات أسلوب apply). تقوم الأداة بالمرور عبر الكود خطوة بختوة، تراقب بدقة ما يحدث لقطع اللغز، وتسجل كل حالة وسيطة.
السحر: بعد ذلك، تأخذ هذا السجل وتكتب "مخطوطة" جديدة ونظيفة (إثبات Isar مهيكل) يقوم بنفس الشيء تماماً ولكن بتنسيق قابل للقراءة.
النتيجة: تحصل على أفضل ما في العالمين. يمكنك القيام باستكشافك الفوضوي والسريع، ثم تضغط على زر للحصول على إثبات احترافي ونظيف، سهل القراءة للبشر وصعب الكسر.
لماذا هذا صعب؟ (الأجزاء المعقدة)
توضح الورقة البحثية أن هذه العملية ليست مجرد مهمة "بحث واستبدال" بسيطة. إنها تشبه محاولة ترجمة مذكرات انسيابية من الوعي إلى عقد قانوني رسمي. إليك العقبات المحددة التي توجب عليهم التغلب عليها:
مشكلة "الخلف" مقابل "الأمام":
المسودة العشوائية تعمل من الخلف إلى الأمام. تبدأ من الإجابة وتسأل: "ما الذي أحتاجه للوصول إلى هنا؟".
المخطوطة تعمل من الأمام إلى الخلف. تبدأ مما نعرفه وتبني وصولاً إلى الإجابة.
الحل: يجب على الأداة هندسة المنطق عكسياً. الأمر يشبه مشاهدة فيلم بالعكس ثم إعادة كتابة السيناريو بحيث يعمل بشكل طبيعي عند تشغيله للأمام.
فوضى "الأهداف المتعددة":
أحياناً، يحل أمر واحد في الكود العشوائي ثلاثة مشاكل مختلفة في آن واحد. في المخطوطة النظيفة، لا يمكنك ببساطة قول "تم حل كل شيء". بل يجب أن تقول صراحة: "إليك كيف حللنا المشكلة (أ)، وإليك كيف حللنا المشكلة (ب)، وإليك كيف حللنا المشكلة (ج)".
الحل: الأداة ذكية بما يكفي لتعرف أي المشاكل قد تغيرت، وتكتب فقط الخطوات الخاصة بتلك المشاكل، لتجنب القوائم المملة والمتكررة.
مشكلة "الظل":
تخيل أن لديك متغيراً باسم "x" في ملاحظاتك العشوائية. لاحقاً، قمت بإنشاء "x" جديد داخل قسم محدد. في الملاحظات العشوائية، يعرف الحاسوب أنهما مختلفان. ولكن عندما تحاول الأداة كتابة القصة النظيفة، قد ترتبك وتظن أنهما نفس الشخص، مما يسبب خلطاً.
الحل: تمتلك الأداة ميزة "إعادة التسمية" للتأكد من أن كل شخصية في القصة لها اسم فريد حتى لا تنهار الحبكة.
مشكلة "الصندوق الأسود":
أحياناً يستخدم الكود العشوائي "تعويذة سحرية" (أمراً معقداً) يقوم بالكثير من الأشياء معاً. لا تستطيع الأداة دائماً رؤية ما بداخل التعويذة لمعرفة كيف عملت بالضبط.
الحل: إذا تعثرت الأداة، فإنها تترك ملاحظة صغيرة تقول: "لقد استخدمنا تعويذة سحرية هنا"، ليبقى الإثبات صالحاً حتى لو لم يتم ترجمة هذا الجزء تحديداً بالكامل.
هل نجح الأمر؟ (النتائج)
اختبر الفريق هذه الأداة على آلاف الإثباتات الحقيقية من مكتبة ضخمة للإثباتات الرياضية (Isabelle Archive of Formal Proofs).
معدل النجاح: نجحت في تحويل 95% إلى 99% من الإثباتات العشوائية إلى إثباتات نظيفة.
النجاح الجزئي: حتى عندما لم تتمكن من تحويل 100% من الإثبات (عادة بسبب تلك "التعاويذ السحرية")، إلا أنها كانت تحول الجزء الأكبر منه، تاركةً فجوات صغيرة جداً فقط.
السرعة: قامت بكل هذا في ثوانٍ معدودة، مما وفر على البشر ساعات من إعادة الكتابة المملة.
الخلاصة
Apply2Isar هو جسر بين العالم الفوضوي والسريع لـ "اكتشاف الأفكار" وبين العالم المنظم والمتين لـ "تدوين النتائج".
إنه يسمح لعلماء الرياضيات وعلماء الحاسوب بالتوقف عن إضاعة الوقت في إعادة كتابة أعمالهم يدوياً. بدلاً من ذلك، يمكنهم التركيز على التفكير الصعب، وترك الكود العشوائي يقوم بالعمل الشاق، ثم ترك الأداة تولد لهم الإثبات الجميل والقابل للقراءة. الأمر يشبه امتلاك محرر شخصي يحول مسودتك الأولية فوراً إلى كتاب منشور.
إليك ملخص تقني مفصل لورقة البحث: "Apply2Isar: التحويل التلقائي لإثباتات نمط (Apply) في Isabelle/HOL إلى نمط (Isar) المهيكل."
1. بيان المشكلة
يدعم نظام Isabelle/HOL نمطين أساسيين للإثبات:
نمط Apply (إجرائي - Procedural): وهي نصوص برمجية تعمل من الخلف إلى الأمام من الهدف (Goal)، حيث تستدعي دوال لتعديل حالة الإثبات. وهي فعالة للاستكشاف والبحث السريع، ولكنها غالبًا ما تكون هشة، وصعبة القراءة، ويصعب صيانتها. فالتغيير الوحيد في مبرهنة (Lemma) أو قاعدة تبسيط يمكن أن يؤدي إلى كسر النص البرمجي في مراحل لاحقة دون توضيح واضح للسبب.
نمط Isar المهيكل (تصريحي - Declarative): وهي إثباتات تحدد بوضوح الأهداف الوسيطة وخطوات الاستدلال، وتتحرك من الأمام إلى الخلف. وهي عالية القابلية للقراءة، ومتينة ضد التغييرات في الأتمتة، ومفضلة لدى مجتمع Isabelle (مثل أرشيف الإثباتات الرسمية، AFP).
التحدي: بينما يعد نمط Isar متفوقًا من حيث الصيانة، يجد المستخدمون غالبًا أن نصوص (apply) أسهل في الكتابة أثناء الاستكشاف الأولي. إن تحويل نص (apply) معقد يدويًا إلى نمط Isar هو عملية مجهدة، تتطلب من المستخدم المرور عبر النص خطوة بخوة، وتسجيل الحالات الوسيطة، وإعادة بناء الإثبات يدويًا. لم تكن هناك أداة مؤتمتة لسد هذه الفجوة، مما أجبر المستخدمين على الاختيار بين النمذجة الأولية السريعة وبين قابلية الصيانة طويلة الأمد.
2. المنهجية
قدم المؤلفون أداة Apply2Isar، وهي أداة Isabelle/ML تقوم بترجمة نصوص نمط (apply) تلقائيًا إلى إثباتات Isar مهيكلة. وتتضمن المنهجية الجوهرية ما يلي:
تحليل AST وإعادة التشغيل: تقوم الأداة بتجزئة وتحليل نص (apply) المدخل إلى شجرة بناء جمل مجردة (AST) مخصصة. ثم تقوم بـ "إعادة تشغيل" النص عبر استدعاء دوال Isabelle/ML المقابلة لمحاكاة تنفيذ كل أمر.
تتبع الحالة: أثناء إعادة التشغيل، تقوم Apply2Isar بتسجيل حالات الإثبات الوسيطة (تحديدًا قائمة الأهداف المعلقة) بعد تطبيق كل طريقة (Method).
البناء العكسي: بما أن نصوص (apply) تستدل من الخلف إلى الأمام (الهدف ← الأهداف الفرعية) بينما يستدل Isar من الأمام إلى الخلف (الحقائق ← الاستنتاج)، فإن الأداة تبني إثبات Isar بترتيب عكسي. فهي تطبع الأهداف الوسيطة والطرق المستخدمة لتفريغها، مما يعكس تدفق النص الأصلي فعليًا.
إدارة الحقائق: لربط الخطوات، تستخدم الأداة طريقة fact. يتم تسمية الأهداف الوسيطة (مثل h_1_1) للسماح للخطوات اللاحقة بالإشارة إليها صراحةً.
استراتيجيات التنفيذ الرئيسية للاختلافات الهيكلية:
الأهداف المتعددة: لتجنب الإطالة عند قيام طريقة ما (مثل auto) بالتأثير على أهداف متعددة في آن واحد، تنفذ الأداة خيار smart_goals. فبدلاً من سرد جميع الأهداف عند كل خطوة، تقوم الأدوية فقط بطباعة الأهداف التي تغيرت، مع تأجيل دمج الأهداف المتبقية إلى بيان show نهائي.
الأهداف الفرعية وترتيب الحقائق: تخلق أوامر مثل subgoal (التي تركز على هدف معين) و supply (التي تسمي الحقائق) تبعيات في الترتيب. وبما أن Isar يتطلب تعريف الحقائق قبل استخدامها، تقوم Apply2Isar برفع كتل subgoal وأوامر note إلى بداية كتلة الإثبات لضمان الصلاحية المنطقية، حتى لو أدى ذلك إلى تعطيل التدفق السردي الأصلي.
التعامل مع unfolding و using: تدير الأداة التفاعل بين هذه الأوامر و apply عن طريق تجميع تأثيراتها. كما توفر خيار smart_unfolds لدمج هذه التأثيرات مع تطبيق الطريقة التالي لتقليل التكرار.
تظليل المتغيرات (Variable Shadowing): تعالج الأداة مشكلة تظليل المتغيرات في أوامر subgoal (حيث قد يشترك متغير محلي جديد في الاسم مع متغير موجود). وتوفر خيار subgoal_fix_fresh لإعادة تسمية المتغيرات لمنع التعارضات، رغم أن هذا يتطلب معالجة دقيقة للإشارات الصريحة.
المتغيرات المخطط لها (Schematic Variables): إذا كان الإثبات يحتوي على أهداف مخطط لها (مجاهيل سيتم تخصيصها لاحقًا)، فلا يمكن للأداة ترجمة ذلك الجزء بالكامل. لذا، تقوم بجمع الأوامر حتى يتم حل الأهداف المخطط لها، ثم تغلف القسم غير المكتمل في بيان have واحد مع apply-script مدمج، مع وضع علامة على النتيجة كـ "ترجمة جزئية".
3. المساهمات الرئيسية
أداة ترجمة مؤتمتة: أول أداة قادرة على تحويل أي نصوص نمط (apply) إلى إثباتات Isar مهيكلة داخل بيئة Isabelle/HOL.
المتانة عبر إعادة التشغيل: من خلال إعادة تشغيل النص والتقاط حالات الإثبات الفعلية، تضمن Apply2Isar أن يكون Isar الناتج صالحًا منطقيًا ومخلصًا لمسار التنفيذ الأصلي، بدلاً من الاعتماد على مطابقة الأنماط الاستدلالية.
التعامل مع الحالات المعقدة: تنجح الأداة في إدارة التفاعلات المعقدة بين الأوامر (مثل back و subgoal و unfolding و using) وتوفر خيارات تهيئة (مثل named_facts و smart_goals و print_types) للموازنة بين القابلية للقراءة والدقة تجاه النص الأصلي.
دعم الترجمة الجزئية: تتعامل الأداة بسلاسة مع الإثباتات التي لا يمكن تحويلها بالكامل (بسبب المتغيرات المخطط لها أو الأوامر غير المدعومة) عن طريق عزل الأجزاء الإشكالية، مما يسمح بتحويل بقية الإثبات.
4. نتائج التقييم
قيم المؤلفون أداة Apply2Isar على مجموعة اختبار مكونة من 4,461 إثباتًا بنمط (apply) مستمدة من خمس مدخلات رئيسية لـ AFP (وهي: Group-Ring-Module، وAutoCorres2، وFlyspeck-Tame، وValuation، وBNF_Operations).
معدل النجاح: نجحت الأداة في إنتاج ترجمات كلية أو جزئية في 95%–99% من حالات الاختبار عبر المدخلات المختلفة.
أنماط الفشل:
فشل الطباعة (~1-2%): نتجت حالات الفشل عن عدم الاتساق في آلية طباعة المصطلحات في Isabelle (إعادة تحليل هدف مطبوع أدى إلى خطأ في الصيغة أو مصطلح مختلف). وهذا قصور في Isabelle نفسها وليس في الأداة.
انتهاء الوقت (Timeouts): نتجت عن البطء الشديد في إعادة تحليل الأهداف المعقدة عندما كانت التوصيفات النوعية (type annotations) مطلوبة.
متنوعة: حالات فشل نادرة تتعلق بالسلوكيات الطرفية للطرق غير الشائعة.
الأداء: الأداة ذات أداء جيد عمومًا، مع ضبط مهلة زمنية قدرها 30 ثانية لكل إثبات. وقد نجحت في التعامل مع أطول نص برمجي في مجموعة الاختبار، والذي احتوى على أكثر من 350 أمرًا.
5. الأهمية
سد الفجوة: تسمح Apply2Isar للمستخدمين بالاستمتاء بقدرات الاستكشاف السريع لنصوص (apply) مع الاحتفاظ بالصيانة طويلة الأمد وسهولة القراءة لنمط Isar المهيكل.
قابلية الصيانة: تقلل بشكل كبير من الجهد اليدوي المطلوب لإعادة هيكلة الأكواد القديمة أو الإثباتات التجريبية إلى التنسيق القياسي المفضل من قبل مجتمع Isabelle و AFP.
الحتمية مقابل النماذج اللغوية الكبيرة (LLMs): على عكس النهج الحديثة المعتمدة على النماذج اللغوية الكبيرة (مثل Isabelle Assistant)، فإن Apply2Isar حتمية تمامًا. فهي لا تعتمد على التوليد الاحتمالي، مما يضمن أن المخرج هو تحويل أمين وقابل للتكرار للنص المدخل.
التنفيذ المحلي: تعمل الأداة محليًا على الأجهزة القياسية، مما يجنب المستخدم الحاجة إلى اشتراكات سحابية أو تبعيات لواجهات برمجة تطبيقات خارجية.
في الختام، تعد Apply2Isar أداة عملية وعالية الفائدة تعزز منظومة Isabelle/HOL من خلال أتمتة الانتقال من الإثباتات الإجرائية إلى الإثباتات التصريحية، مما يحسن متانة وسهولة الوصول إلى تطويرات التحقق الرسمي.