SATNet: ربط التعلم العميق والمنطق الاستدلال باستخدام حلّال الرضا القابل للمفاضلة

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