1215 ورقة بحثية
تقدم هذه الورقة "ReasonOps"، وهو نموذج تشغيلي موحد مستوحى من "DevOps" و"MLOps"، يدمج التفسير الدلالي، والتحقق الرسمي، وضمان وقت التشغيل في دورة حياة مستمرة لمعالجة التناقضات المنطقية وفجوات الموثوقية في استدلال النماذج اللغوية الكبيرة للتطبيقات ذات الأهمية الحرجة للسلامة.
تؤيد هذه الموقفية التعددية المنطقية ضمن إطار منطقي كلي موحد مثل LogiKEy، محاجةً بأن دعم منطقات موضوعية متعددة في مساعدات الإثبات —بدلاً من فرض منطق تأسيسي واحد— من شأنه أن يُمكّن بشكل أفضل من الأبحاث البينية وتطوير النظريات واسعة النطاق.
تُثبت هذه الورقة أن تقريب الحلول من خوارزميات استرخاء PCSP القياسية (BLP وAIP وBLP+AIP) لإيجاد شهادات البحث هو بصعوبة أي مسألة من مسائل TFNP، وتُثبت أن تحديد ما إذا كانت قوالب PCSP المنتهية تستوفي هذه الخوارزميات أو شروطاً جبرية معينة من حيث القابلية للتتبع هو أمر غير قابل للتقرير.
تقدم هذه الورقة FLINGO، وهي لغة وأداة تعزز برمجة مجموعات الإجابات المقيدة (CASP) من خلال دمج ميزات أساسية لبرمجة مجموعات الإجابات (ASP) — مثل القيم الافتراضية، والسمات غير المعرفة، والتعيينات غير الحتمية، والتجميعات — ضمن القيود الصحيحة الخطية، جنباً إلى جنب مع آلية ترجمة إلى أدوات حل CASP القياسية.
تعالج هذه الورقة البحثية الغموض البعدي في القيود المكانية لبروتوكول ODRL من خلال تقديم طريقة لتفكيك المحاور تحول المعاملات متعددة المحاور إلى فترات قياسية محددة لكل محور، مما يتيح كشفاً سليماً وكاملاً للتعارض عبر مقارنة الصناديق، ويتم التحقق من صحتها عبر ملف تعريف جديد وتحقق شكلي واسع النطاق.
تتقصى هذه الورقة ديناميكيات النمو في اكتشاف المعادلات عبر مجالات تجريبية وواقعية، حيث وجدت أنه بينما يتبع النمو قصير المدى قانون القوة، فإن المسارات طويلة المدى تظهر أنماط تشبع تعتمد على الركيزة يمكن نمذجتها بشكل أفضل بواسطة دالة قانون قوة مشبعة، مع تباين الديناميكيات المحددة بشكل كبير بين البيئات الحسابية المختلفة.
تقدم هذه الورقة خوارزمية مبتكرة تستفيد من تقنيات التحقق من الشبكات العصبية لحساب حدود دقيقة ومثبتة وقابلة للضبط بشكل تعسفي لقيم شابلي (Shapley) الدقيقة، مما يتيح حساب قيم SHAP بدقة وقابلية للتوسع للشبكات العصبية ذات مساحات البحث الأكبر بكثير من الطرق الدقيقة الحالية.
تتناول هذه الورقة أوجه القصور في أدوات التخليق الحالية فيما يتعلق بالمواصفات الحسابية الحقيقية غير الخطية غير القابلة للتحقيق، وذلك عبر اقتراح إطار عمل يعمل على تخليق برامج ذات مدخلات ومخرجات نسبية إما لاستيفاء المواصفة أو للإبلاغ بشكل صحيح عن عدم وجودها، ويتميز بخوارزمية كاملة لحالات المخرج الواحد ونهج سليم وغير كامل للمواصفات العامة تم تنفيذه في أداة NQSynth.
تقدم هذه الورقة شبكة البوابات المنطقية الثلاثية المتكررة والقابلة للتفاضل (R-DTLGN)، وهي بنية مبتكرة تتعلم التنبؤ بأحكام المنطق الزمني الإشاري مع توفير ضمانات رسمية للديناميكيات المستقرة والامتناع المبدئي تحت ظروف تدهور المستشعرات من خلال العمل عبر منطق كليين ثلاثي القيم واستخلاص حجم الشبكة مباشرة من بنية الصيغة الزمنية.
تقدم هذه الورقة حسابات عرض التفنيد لمنطق LE الأساسي، وتثبت سلامتها واكتمالها من خلال تحليل البرهان، وتستنتج منها حسابات جداول استدلالية متوقفة.