1215 ورقة بحثية
تقدم هذه الورقة تقنيات خوارزمية جديدة للتحقق والتعلم التلقائي لبرامج C-RASP —وهي بنى لغوية تجسد قدرة التعبير في نماذج المحولات (transformer)— من خلال الاستفيد من الروابط مع فحص النماذج باستخدام Lustre والبحث المحلي، مما يتيح تطبيقات في تحسين برامج المحولات والتعلم المقيد.
تثبت هذه الورقة قابلية التقرير للتوسعات أحادية المتغير لحساب بريسر للقوى الثابتة الكاملة وكثيرات الحدود التكعيبية من خلال الاستفادة من النتائج المتعلقة بالمعادلات الديوفانتية فوق المنحنيات فائقة الهليلية والمنحنيات الجبرية ذات الجنس المنخفض، بينما تبين أن رفع هذه القيود يؤدي إلى عدم قابلية التقرير من خلال ترميزات لمسائل ديوفانتية مفتوحة.
تقدم هذه الورقة نظام GRASS، وهو نظام أنواع موحد يدمج آليات تقييد الموارد للمنطقيات تحت البنيوية مع التتبع الكمي للأنظمة المتدرجة، مما يتيح تحكماً مرناً وغير متجانس في استخدام المتغيرات ضمن إطار عمل واحد، ويستوعب النماذج الراسخة مثل LNL وAdjoint Logic وmGL من خلال دلالاته الفئوية.
تقدم هذه الورقة إطار عمل لتوليد حالات تحقق للشبكات العصبية ذات تسميات حقائق أرضية معروفة بشكل مبرهن للتغلب على قيود المعايير المرجعية الحالية، مما يمكّن من اكتشاف أخطاء أدوات التحقق والتحليل المنهجي لأنماط الفشل من خلال مقياس "ملف الصعوبة" الجديد.
تثبت هذه الورقة قابلية التقرير لتعيين ما إذا كانت صيغة معينة من الرتبة الثانية الأحادية (MSO) فوق ترتيبات خطية مسمومة قابلة للعد تقبل إعادة بارامترية ذات من الأبعاد، مما يثبت أن أي بنية قابلة للتفسير من هذا النوع يمكن تمثيلها بشكل مكافئ كتفسير نقطي ذي من الأبعاد.
تُظهر الورقة البحثية أن نظرية الحساب المحدود ، حتى عند تعزيزها بمبدأ بيت الحمام لجميع صيغ ، غير كافية لإثبات مبدأ التقليل للترتيبات الخطية الصارمة على الفترات المحدودة.
تقدم هذه الورقة "منطق الفرضيات" (LoH)، وهو إطار عمل عصبي رمزي مبتكر يوحد بين القواعد المصممة يدويًا والتعلم القائم على البيانات عبر توسيع المنطق القضايا بمعامل اختيار قابل للتعلم يتم تجميعه في منطق ضبابي قابل للتفاضل، مما يتيح تكاملاً مرنًا للمعرفة واستدلالًا بولينياً منفصلاً دون فقدان في الأداء.
تُثبت هذه الورقة أن نماذج المحولات ذات الدقة الثابتة هي بطبيعتها أكثر إيجازاً بشكل أسي من المنطق الزمني الخطي، والشبكات العصبية المتكررة، والأتمتة المحدودة، وهي خاصية تجعل مشكلات التحقق الأساسية مثل الفراغ والتكافؤ من فئة EXPSPACE-complete.
تقدم هذه الورقة "الهاي-سيكوينتات الديناميكية" (dynamic hypersequents)، وهي إطار نظري برهاني جديد يوسع حسابات الهاي-سيكوينت (hypersequent calculi) لتشمل منطق الإعلان العام، والذي ينجح في استيعاب ديناميكية التحديثات المعرفية ويثبت خصائص رئيسية مثل قابلية قبول القواعد الهيكلية، وقابلية عكس القواعد، وإلغاء القطع النحوي.
تثبت هذه الورقة أن "مسألة المدار" (Orbit Problem) قابلة للتقرير بحد تعقيد NP^RP عندما يكون البعد اللوغاريتمي للفضاء الجزئي المستهدف، بينما تثبت أن المسألة تصبح بصعوبة "مسألة سكولم" (Skolem Problem) التي لا تزال مفتوحة منذ فترة طويلة عندما يكون البعد الخطي للفضاء الجزئي المستهدف.