🤖 machine learning

SMT-Based Active Learning of Weighted Automata

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

المؤلفون الأصليون: Tiago Ferreira, Kevin Batz, Alexandra Silva

نُشر 2026-05-11

📖 5 دقيقة قراءة🧠 قراءة متعمّقة

CC BY 4.0

المؤلفون الأصليون: Tiago Ferreira, Kevin Batz, Alexandra Silva

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

تخيل أنك تحاول تعليم روبوت كيفية التنقل في متاهة، لكنك لا تعرف مخطط المتاهة. يمكنك طرح نوعين من الأسئلة على الروبوت:

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

هذه هي الفكرة الجوهرية لـ التعلم النشط (Active Learning): خوارزمية تتعلم نموذجًا من خلال طرح أسئلة ذكية على "المعلم" (النظام الحقيقي).

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

تقدم هذه الورقة البحثية طريقة جديدة وقوية لتعليم الحواسيب تعلم هذه الأوتوماتا الموزونة (Weighted Automata) (متاهات مرتبطة بأرقام في مساراتها).

الطريقة القديمة: طريقة "الجدول"

في السابق، استخدم الباحثون طريقة تعتمد على جدال ضخمة (تسمى مصفوفات هانكل - Hankel matrices). تخيل محاولة حل لغز عن طريق ملء جدول بيانات ضخم حيث تعتمد كل خلية فيه على قواعد جبرية معقدة.

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

الطريقة الجديدة: طريقة "SMT"

يقترح المؤلفون نهجًا مختلفًا: حل القيود (Constraint Solving). بدلًا من ملء جدول بيانات، يقومون بتحويل مشكلة التعلم إلى لغز منطقي ضخم.

التشبيه: المحقق ومحلل الـ SMT
تخيل أنك محقق تحاول إعادة بناء مسرح جريمة (المتاهة) بناءً على شهادات الشهود (إجابات المعلم).

الفرضية: تخمن مشتبهًا به وجدولًا زمنيًا (خريطة صغيرة بها عدد قบ้าง حالات).
القيود: تكتب قائمة من القواعد: "إذا كان المشتبه به في البنك، فيجب أن يكون قد غادر بحلول الساعة 5 مساءً"، أو "يجب أن يكون إجمالي المال المسروق يساوي 100 دولار".
محلل الـ SMT: هذا برنامج حاسوبي فائق الذكاء (مثل محرك منطقي) يتحقق مما إذا كانت قواعدك منطقية. إنه يسأل: "هل هناك أي طريقة لترتيب تحركات المشتبه به بحيث تكون كل هذه القواعد صحيحة؟"
- إذا كانت الإجابة نعم: يعطيك المحلل خريطة صالحة.
- إذا كانت الإجابة لا: يخبرك أن خريطتك مستحيلة.

تعمل خوارزمية الورقة البحثية كالتالي:

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

لماذا هذه الطريقة أفضل؟

تدعي الورقة وجود ثلاث مزايا رئيسية، مشروحة ببساطة:

1. تجد دائمًا أصغر خريطة (الحد الأدنى - Minimality)
الطرق القديمة كانت تعطيك أحيانًا خريطة بـ 10 غرف بينما كانت خريطة من 3 غرف ستفي بالغرض. طريقة SMT الجديدة مصممة لإيجاد أصغر خريطة ممكنة تتوافق مع القواعد. الأمر يشبه العثور على المسار الأكثر كفاءة بدلًا من مجرد العثور على أي مسار.

2. تعمل مع رياضيات "غريبة"
عانت الطرق القديمة مع الأنظمة العددية المعقدة (مثل رياضيات "تروبيكال" - Tropical math، حيث تجمع الأرقام ولكن تأخذ الحد الأدنى، أو رياضيات "عنق الزجاجة" - Bottleneck math). الطريقة الجديدة يمكنها التعامل مع هذه الأنظمة الرياضية "الغريبة" عن طريق تحويلها إلى ألغاز منطقية يفهمها محلل الحاسوب. الأمر يشبه امتلاك مترجم عالمي يمكنه تحويل الرياضيات المعقدة إلى أسئلة بسيطة من نوع "صواب/خطأ".

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

المقارنة مع الأساس "الساذج" (Naive Baseline): قارنوا طريقتهم بنسخة "غبية" تقوم بالتخمين العشوائي فقط، وكانت طريقتهم متفوقة بمراحل.
المقارنة مع المنافس "الأحدث" (State-of-the-Art): قارنوا طريقتهم بأفضل طريقة موجودة حاليًا، ونتج عن طريقتهم خرائط أصغر بكثير (أحيانًا بـ 10 أضعاف!) ومع ذلك انتهت في وقت معقول.

"المكون السحري": محللات الـ SMT

السر يكمل في حل الـ SMT (الرضا ضمن النظريات - Satisfiability Modulo Theories). اعتبر محلل الـ SMT بمثابة مدقق منطقي فائق القدرة. فهو لا يكتفي بالتحقق مما إذا كانت الجملة صحيحة، بل يتحقق مما إذا كانت مجموعة معقدة من القواعد الرياضية يمكن أن تكون صحيحة في آن واحد.

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

الملخص

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

النتيجة: تجد أبسط نموذج ممكن.
النتيجة: تعمل على مجموعة أوسع من الأنظمة الرياضية مقارنة بما سبق.
النتيجة: هي أسرع وتطرح أسئلة أقل من الطرق السابقة.

لقد اختبر المؤلفون هذا على آلاف الأمثلة ووجدوا أنه أداة عملية وقوية لتعلم هذه الأنظمة المعقدة، مما يقدم بديلًا قويًا للطرق المستخدمة في العقد الماضي.

ملخص تقني: التعلم النشط للأوتوماتا الموزونة القائم على SMT

بيان المشكلة

أصبح تعلم الأوتوماتا النشط، الذي رادته خوارزمية $L^\star$ لـ Angluin، تقنية قياسية لاستنتاج نماذج للمكونات غير المعروفة في التحقق الرسمي. وبينما تُعد طرق $L^\star$ مستقرة ومستقرة للأوتوماتا البوليانية (الحتمية وغير الحتمية)، فإن توسيع نطاقها ليشمل الأوتوماتا ذات الأوزان المحدودة (WFAs) أثبت أنه أكثر صعوبة بشكل ملحوظ. تقوم الـ WFAs بتعميم الأوتوماتا البوليانية عبر تعيين أوزان من نصف حقل (semiring) للتحولات، مما يسمح بنمذجة الخصائص الكمية مثل التكلفة، أو الاحتمالية، أو استهلاك الموارد.

تعتمد النهج الحالية لتعلم الـ WFAs على تعميمات لمصفوفة هانكل (Hankel matrix) أو جدول الملاحظات (مثل $WL^\star$ ). تتطلب هذه الطرق التفكير في البنية الجبرية لنصف الحقل الأساسي. وبناءً على ذلك، فإن إثبات الإنهاء والحد الأدنى (minimality) أمر دقيق وغالباً ما يقتصر على فئات جبرية محددة (مثل الحقول أو النطاقات المثالية الرئيسية). بالنسبة للعديد من أنصاف الحقول ذات الصلة العملية، مثل نصف الحقل الاستوائي (Tropical semiring) أو نصف حقل العنق (Bottleneck semiring)، فإن ضمانات الإنهاء إما غير معروفة أو لا تضمن إنتاج أوتوماتا ذات حد أدنى. علاوة على على ذلك، غالباً ما تنتج الخوارزميات الحالية نماذج غير دنيا أو تفشل في التوسع بفعالية عبر أنصاف الحقول اللانهائية.

المنهجية

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

النهج الجوهري

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

تتبع عملية التعلم حلقة تعلم نشط قياسية (الخوارزمية 1):

توليد الفرضية: تحاول الخوارزمية إيجاد WFA بـ $n$ من الحالات يكون متسقاً مع مجموعة الملاحظات الحالية $O$ . يتم تفويض هذه المهمة إلى إجراء فرعي يسمى getAutomaton.
استعلام التكافؤ: إذا تم العثين على فرضية $H$ متسقة، يتم استعلام المعلم للتحقق مما إذا كانت $H$ تتعرف على اللغة المستهدفة $L$ .
التعامل مع المثال المضاد: إذا قدم المعلم مثالاً مضاداً $w$ (حيث $H(w) \neq L(w)$ )، يتم إضافة $w$ إلى $O$ ، وتتكرر الحلقة مع تقوية القيود.

الإجراء الفرعي `getAutomaton`

يقدم البحث تنفيذين لـ getAutomaton:

الأساس الساذج (Naive Baseline): يقوم بتشفير دلالات الـ WFA مباشرة. يعامل الأوزان الأولية، ومصفوفات الانتقال، والأوزان النهائية كمتغيرات مجهولة ويحل المعادلة $out(w) = \text{semantics}(w)$ لجميع $w \in O$ .
المُحسَّن (SWAL): يستخدم منظوراً كوجبرياً (coalgebraic perspective) ومفهوم لغات الحالات. بدلاً من حل اللغة العالمية مباشرة، يُدخل متغيرات وسيطة تمثل اللغة المقبولة من كل حالة. ينتج عن ذلك نظام من المعادلات حيث:
- تضمن قيود الاستقرار (Stabilization constraints) أن لغات الحالات متسقة مع أوزان الانتقال.
- تضمن قيود الامتداد (Spanning constraints) أن الأوزان الأولية تجمع لغات الحالات بشكل صحيح لتطابق المخرجات المستهدفة.
- رؤية جوهرية: بينما يقدم هذا التشفير المزيد من المتغيرات والمعادلات، إلا أنه يكشف عن بنيات فرعية مشتركة (اللاحقات) بين الملاحظات. وهذا يسمح لحلول SMT بإعادة استخدام النتائج الوسيطة، مما يحسن القابلية للتوسع بشكل كبير مقارنة بالنهج الساذج.

القابلية للتقرير وأنصاف الحقول

الخوارزمية معلمية (parametric) في نصف الحقل. حدد المؤلفون أن أنصاف الحقول القابلة للتقرير (حيث تكون قابلية إرضاء أنظمة المعادلات المنتهية قابلة للتقرير) يمكن تنفيذ الإجراء الفرعي getAutomaton فيها بشكل سليم وكامل.

أنصاف الحقول المنتهية: قابلة للتقرير بشكل بديهي عبر البحث الشامل أو SMT.
أنصاف الحقول اللانهائية: يقدم البحث تشفيرات لـ نصف الحقل الاستوائي ( $\min, +$ )، وأنصاف الحقول الاستوائية المحدودة، ونصف حقل العنق ( $\max, \min$ ) في نظريات قابلة للتقرير مثل الحساب الصحيح الخطي الخالي من المكمم (QF-LIA) والمتجهات الثنائية الخالية من المكمم (QF-BV).

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

خوارزمية جديدة: خوارزمية تعلم نشط جديدة قائمة على SMT للأوتوماتا ذات الأوزان المحدودة غير الحتمية، وهي معلمية في نصف الحقل.
ضمان الحد الأدنى: على عكس طرق $L^\star$ التي تفتقر غالباً لضمانات الحد الأدنى خارج الهياكل الجبرية المحددة، فإن هذه الخوارمة تضمن إنتاج WFAs دنيا عند الانتهاء، بغض النظر عن نصف الحقل.
شروط الإنهاء: يثبت المؤلفون الصحة الجزئية ويوفرون شروطاً كافية للإنهاء. تحديداً، يثبتون أن الخوارزمية تنتهي لـ جميع أنصاف الحقول المنتهية. بالنسبة لأنصاف الحقول اللانهائية، ورغم أن الإنهاء ليس مضموناً نظرياً بنفس حجج الكاردينالية، إلا أن التنفيذ يظهر نجاحاً عملياً.
التركيب القائم على القيود: يقدم البحث أول خوارزمية توليد قائمة على القيود لـ WFAs، مما يتيح التركيب القائم على SMT. كما يحدد أنصاف حقل محددة تكون فيها أنظمة القيود الناتجة قابلة للتقرير.
التقييم التجريبي: تقييم شامل يقارن الطريقة المقترحة (SWAL) بالأساس الساذج وخوارزمية $WL^\star$ المتطورة.

النتائج التجريبية

قام المؤلفون بتنفيذ الخوارزمية (SWAL) بلغة OCaml باستخدام محلل Z3 وقاموا بتقييمها على أكثر من 5,000 اختبار مرجعي تم إنشاؤه عشوائياً عبر أنصاف الحقول البوليانية، والاستوائية، والاستوائية المحدودة، والعنق.

مقابل الأساس الساذج: يتفوق SWAL بشكل كبير على التشفير الساذج في كل من وقت التشغيل والقابلية للتوسع. بينما يواجه النهج الساذج صعوبة في تعلم الأوتوماتا التي تحتوي على أكثر من 2-6 حالات (اعتماداً على نصف الحقل)، ينجح SWAL في تعلم الأوتوماتا الدنيا التي تصل إلى 8 حالات. التشفير المُحسَّن (لغات الحالات) يقلل من حالات انتهاء الوقت (timeouts) أو أخطاء نفاذ الذاكرة (OOM) بعدة مراتب.
مقابل $WL^\star$ : عند مقارنتها بـ $WL^\star$ $W L^{⋆}$ (وهي خوارزمية متطورة للنطاقات المثالية الرئيسية):
- الحد الأدنى: تنتج SWAL باستمرار أوتوماتا دنيا (minimal)، بينما تنتج $WL^\star$ غالباً أوتوماتا أكبر بما يصل إلى 10 أضعاف.
- الكفاءة: تتطلب SWAL عدد استعلامات مخرجات أقل (تفاعلات مع المعلم) من $WL^\star$ .
- وقت التشغيل: تعد SWAL منافسة في وقت التشغيل، وغالباً ما تنتهي بشكل أسرع ومع عدد أقل من فشلات الموارد (TO/OOM) مقارنة بـ $WL^\star$ .
التزايد (Incrementality): أدى تمكين حل SMT التزايدي إلى تقليل وقت التعلم واستهلاك الموارد بشكل كبير، مما يؤكد ملاءمة النهج القائم على القيود للتعلم التزايدي.

الأهمية والادعاءات

تضع الورقة التعلم القائم على القيود كبديل عملي وقوي للطرق التقليدية القائمة على Hankel/ $L^\star$ للأوتوماتا ذات الأوزان، خاصة في سياقات التحقق.

المتانة: يتعامل النهج مع نطاق أوسع من أنصاف الحقول (بما في ذلك اللانهائية مثل Tropical) حيث يصعب أو يستحيل إثبات الإنهاء الجبري لطرق $L^\star$ .
الحد الأدنى: يعد ضمان الحد الأدنى ميزة حاسمة، حيث أن النماذج الدنيا ضرورية للتحقق والتبسيط الفعال.
القابلية للتوسع: تظهر النتائج التجريبية أن التركيب القائم على SMT يمكن أن يتوسع لتعلم أوتوماتا ذات أوزان معقدة ودنيا، والتي تعد حالياً بعيدة المنال بالنسبة للخوارزميات الموجودة.

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