1215 ورقة بحثية
تقدم هذه الورقة البحثية ، وهي امتداد لمنطق الزمن المتبادل (Alternating-Time Temporal Logic) يجمع بين الاستدلال الاستراتيجي وقيود متوسط العائد طويل الأمد على هياكل الألعاب المتزامنة الموزونة، حيث تثبت أن فحص النموذج (model checking) هو مسألة كاملة من فئة في الحالات أحادية الأبعاد ومتعددة الأبعاد، مع توصيف الهيكل الصارم لمتطلبات الذاكرة والقدرة التعبيرية للمنطق من أجل التوليف المضمون للأداء والتحقق التعاوني العقلاني.
تقدم هذه الورقة صياغة رسمية باستخدام Isabelle/HOL لبروتوكول إثبات شفاف من طراز STARK، يتميز بنموذج قابل للتنفيذ للمُثبت والمُتحقق، وموناد حالة احتمالية مع حساب الشرط الأضعف، ونظريات مُحققة رسميًا حول كمال الأمان والنزاهة (honest completeness) وصحة الإثبات (soundness) مع حدود احتمالية صريحة.
تقدم هذه الورقة Octopus، وهي أداة تترجم محللات حزم P4 إلى نماذج ذات أتمتة للتحقق بكفاءة من تكافؤها على الأجهزة الاستهلاكية عبر تقديم إما برهان التماثل أو تدفق بتات كنموذج مضاد.
تقدم هذه الورقة أول ترجمة من منطق الزمن الخطي (LTL) إلى (LTLf+)، مما يتيح تطبيق تقنيات الأوتوماتا ذات المسارات المحدودة الفعالة على مشكلات الذكاء الاصطناعي ذات المسارات غير المحدودة دون زيادة التعقيد التقاربي لمسار التحويل القياسي من LTL إلى الأوتوماتا.
تُثبت هذه الورقة أن النوع المتدرج المعتمد على التأثير المشترك (graded coeffect typing) فوق الحلقات الاستوائية (tropical semiring) ينمذج مرور الوقت بفعالية لضمان وتوصيف إنتاجية البرامج جيدة النوع، مع تمكين نظام نوع تقاطع زمني جديد مثالي من الناحية النظرية التكرارية.
تقترح هذه الورقة إطار عمل للضمان في وقت التشغيل، ثلاثي المستويات ومعتمد على التحقق، لأسراب الاستطلاع والاستخبارات والاستطلاع (ISR) المدعومة بالنماذج اللغوية الكبيرة (LLMs)، والتي تكتشف انتهاكات السياسات على مستوى المهمة — مثل انقسام الأهداف المحظورة أو تجاوز الميزانية الجماعية — من خلال تركيب الأحكام الخاصة بكل منصة عبر نسيج مراسلة مقاوم للأخطاء، مما يمنع حالات "الكل آمن" الخاطئة والصامتة الشائعة في أنظمة المراقبة المركزية.
تقترح هذه الورقة "التدرج السلسلي" (chain stratification)، وهو شرط مبتكر يعالج تحديات تطبيق النفي الافتراضي على قواعد RDF والقواعد الوجودية من خلال الجمع بين تحليل الاشتقاق متعدد الخطوات وقيود السلامة لضمان دلالات فريدة، رشيقة، ومبررة بغض النظر عن ترتيب تطبيق القواعد.
تقترح هذه الورقة نهجاً فعالاً للفرع والتقصي (Branch and Bound) للتحقق من الشبكات العصبية يستفيد من رتابة المسار والبحث الأسي لتقسيم دوال تنشيط متعددة في آن واحد، مما يؤدي إلى تخطي المشكلات الفرعية غير ذات الصلة وتحديد حدود الحكم بدقة دون عملية نشر الحدود المتسلسلة المكلفة المستخدمة في الطرق الحالية.
تقدم هذه الورقة إطار عمل للمعالجة الداخلية للتحقق من الشبكات العصبية يستخدم إجراءات الاستشراف لاستخلاص لِمات (lemmas) عبر وحدات ReLU غير المستقرة، والتي تُستخدم بعد ذلك لتقليص مساحة البحث وتحسين أداء أدوات التحقق المتطورة مثل Marabou و --CROWN من خلال إثبات عدم قابلية 34% من الحالات للتحقق.
تُثبت هذه الورقة أن جميع صيغ ضرب المصفوفات من الرتبة 23 فوق الحقل العشر التي كانت تُعتبر سابقاً "غير قابلة للإرضاء متوقعة" هي في الواقع قابلة للإرضاء، وتوفر شهادات كاملة لهذه الحالات إلى جانب مخطط جديد من الرتبة 23 يحتوي على حد مضاف خالٍ من النوع-3.