1215 ورقة بحثية
يُثبت هذا البحث وجود اختزال ذي حالة محدودة لمنطق فيتينج الموجه ذي القيم هيتينغ (Fitting's finite Heyting-valued modal logic) باستخدام تمثيل ثنائي الطوبولوجيا علائقي، مُثبتاً أن الحصص الملاحظة تحفظ قيم الحقيقة الدقيقة وتُمكّن من بناء شهادات شجرية محدودة لكل من الصيغ الصالحة وغير الصالحة.
تقدم هذه الورقة إطار عمل مدركاً للضجيج للبرمجة الكمومية يؤسس دلالات تعتمد على الأجهزة، ويطور منطق "هوار" (Hoare logic) مقابلاً للتحقق المحدود، ويمكّن من التخليق التلقائي لروتينات فرعية كمومية خالية من الحلقات ومثلى من حيث الضجيج عبر الاستفيد من نماذج الخطأ الواقعية من موردين مثل IBM.
توسع هذه الورقة حساب لامدا الخطي الكمي (quantalic linear lambda-calculus) بإضافة الفصل الجمعي (additive disjunction) لتمكين الاستدلال الكمي حول عبارات الحالة (case statements)، مع إثبات سلامته واكتماله التقريبي تحت شروط الاستمرارية، بينما تستعرض قابليته للتطبيق عبر نماذج المنطق الفئوي، والحوسبة الاحتمالية، وحوسبة الكم، لا سيما باستخدام فضاءات باناخ (Banach spaces) لتحليل المسارات العشوائية.
تقدم هذه الورقة HOPSCOTCH، وهو إطار عمل لـ Lean 4 يعمل على مكننة البراهين التشفيرية القائمة على الألعاب والمتسقة حاسوبياً باستخدام منهجية التضمين الضحل وتجريد الحالة للتحقق رسمياً من الخصائص الأمنية المعقدة مثل بناء GGM وأمن IND-CCA.
تقدم هذه الورقة أداة Uppaal Coshy، وهي أداة تلقائية تعمل على تخليق دروع سلامة مدمجة للأنظمة الهجينة من خلال تقريب تقسيمات فضاء الحالة المعقدة عبر عمليات المحاكاة وتوظيف خوارزمية Caap لتمثيل الاستراتيجيات الناتجة بكفاءة كأشجار قرار.
تثبت هذه الورقة أن علاقة التكافؤ الخاصة بـ pp-bi-interpretability، التي تشكل ركيزة النهج الجبري لتخمين بوديرسكي-بينسركر حول تعقيد مسألة التوافق (CSP)، هي علاقة قابلة للتقرير في ظل ظروف طفيفة وتُظهر أدنى تعقيد ممكن في نظرية المجموعات الوصفية (النعومة) للبنى -categorical المتعدية التي تفتقر إلى الجبرية، بينما تقدم أيضاً برهاناً بنائياً لقابلية الحوسبة للنوى كاملة النموذج (model-complete cores) في البنى ذات التوسعات رامزي محدودة الحدود.
تقترح هذه الورقة إطار عمل للدمج العصبي الرمزي خالٍ من المعرفة بالمجال، يستفيد من مجمعات ناقلات التسمية والاستنباط القائم على الاتساق لدمج كواشف "ViT" سابقة التدريب بشكل قوي، محققاً أداءً فائقاً على نماذج التصويت بالأغلبية المرجعية في ظل كل من التحولات التوزيعية والهجمات العدائية المنسقة.
إيغينيوس (Eigneius) هو نظام إدارة قواعد بيانات معرفية مفتوح المصدر ومعتمد على الأنواع، يوحد بين نظرية النوع التابع، وحدود التكامل المؤسسي، والتخزين غير القابل للتغيير لفرض الحالة الإبستيمية كمتغير بنيوي ثابت، وبذلك يستبدل نصوص أبحاث الذكاء الاصطناعي الهشة والزائلة برسم بياني للأدلة قابل للمسح الآلي وجاهز للتدقيق، وقادر على التحقق من الاستنتاجات العلمية وكشف التناقضات.
تقدم هذه الورقة صياغة بديهية منقحة للخطية التزايدية في الحساب الصحيح غير الخطي، والتي تحسن بشكل كبير من التقارب في قيود كثيرات الحدود عالية الدرجة، مما يظهر أداءً تنافسيًا ضد أحدث الحلول، لا سيما في الاختبارات المرجعية التي تهيمن عليها مثل هذه القيود.
تقدم هذه الورقة "موناد احتمالي مدرك للتكلفة" (cost-aware probability monad) لـ Liquid Haskell، يدمج البرامج الاحتمالية القابلة للتنفيذ مع التحقق القائم على أنواع التجويد (refinement-type-based verification) والأتمتة باستخدام (SMT)، لتمكين الاستدلال التركيبي والإثبات الآلي للتكاليف المتوقعة في الخوارزميات وهياكل البيانات الاحتمالية.