1215 ورقة بحثية
توسع هذه الورقة نطاق "حساب الآلة الوظيفي" (Functional Machine Calculus) من تدفق التحكم المتسلسل إلى تدفق التحكم المتفرع والمتكرر، مما يتيح التضمين الأمين للغة أمرية كاملة مع الحفاظ على الخصائص الجوهرية مثل الاختزال المتوافق، والنمذجة القوية، ودلالات تشغيلية موحدة قائمة على آلة "كريفين" متعددة المكدسات.
تجسد هذه الورقة إطار عمل دلالات الأثر الكو-الجبري لألعاب التحكم مقابل البيئة المكونة من لاعبين، مع بيئات غير حتمية أو احتمالية، مظهرةً أن عناصر الأثر تقابل مجموعات من اللعب التي يمكن للمتحكم فرضها عبر استراتيجيات محددة، وكل ذلك مُعايَر بواسطة قانون توزيع ضعيف.
تقدم هذه الورقة مفهوم النظريات التكافؤية الكمية المتراصة، حيث تثبت أن نظرية جبرات الباريسنترك الاستيفائية متراصة وتستخدم هذه النتيجة لاشتقاق نظريات متراصة أخرى تضع بديهيات للمسافات على توزيعات الاحتمالات ذات الدعم المحدود.
تقدم هذه الورقة نهجاً قائماً على التلقين يستفيد من النماذج اللغوية الكبيرة لتوجيه التفكيك الهرمي لالتزامات إثبات TLA+ إلى ادعاءات فرعية أبسط من أجل التحقق الرمزي، مما يتغلب على التحديات الهيكلية ويتفوق على الطرق المرجعية في معيار جديد يتكون من 119 نظرية.
تقدم هذه الورقة تدريب البديل متعدد الحدود (PST)، وهو أسلوب قابل للتوسع يتيح التدريب التفاضلي الفعال لشبكات البوابات المنطقية الثلاثية، وذلك من خلال تمثيل العصبونات كمتعددات حدود قابلة للتعلم، مما يتغلب على فضاء البحث المستعصي للنهج الحالية ويُظهر قدرة فائقة على التعامل مع عدم اليقين وسرعة تدريب مقارنة بنظيراتها الثنائية.
تقدم هذه الورقة صياغة رسمية بلغة Lean 4 ضمن مكتبة Mathlib تعمل على إزالة التحيز عن الفئات المونويدية المتناظمة عبر تمديد بياناتها إلى شبه دالة (pseudofunctor) ذات قيم في فئة Cat فوق الروابط (spans) للمجموعات المنتهية، مستفيدة من مبرهنة التماسك لماكلان (Mac Lane's coherence theorem) وتشفير ثنائي الفئة كليسلي (Kleisli bicategory encoding) للتعامل مع نواتج الضرب التنسوري ذات الرتب العليا وتماسكها.
تقدم هذه الورقة البحثية PPO-LTL، وهو إطار عمل للتعلم التعزيزي الآمن يدمج قيود المنطق الزمني الخطي (LTL) في خوارزمية التحسين التقاربي السياساتي (PPO) عن طريق ترجمة انتهاكات المنطق الزمني الخطي إلى إشارات جزاء عبر أوتوماتا بوشي المحدودة الحتمية ومخطط لاغرانج، مما يظهر تفوقاً في السلامة والأداء في بيئات الروبوتات.
توضح هذه الورقة الطبيعة المترية للعلاقات المنطقية التفاضلية من خلال تقديم فضاءات شبه-شبه-مترية لنمذجة مسافات البرامج، وإرساء تمهيدية أساسية للاستدلال التركيبي، وإثبات أنه بينما تدعم هذه الفضاءات علاقة منطقية تفاضلية أقصى ما يمكن، إلا أنها تفتقر إلى نظير هو الأشد خشونة، على خلاف التكافؤات السياقية التقليدية.
تقدم هذه الورقة Canonical-min، وهو محلل موجز وسليم لمسائل عدم القابلية للتقرير في الاستيطان والتوحيد في نظرية النوع التابع، إلى جانب إطار عمل موني (monadic) جديد لتحويل مدققي الأنواع إلى محللات فعالة، ومعيار DTTBench للتقييم.
تقدم هذه الورقة إطاراً جبرياً شاملاً لتعميم المصطلحات حتى النظريات التكافؤية من خلال الاستفادة من الجبر الإسقاطي والدقيق لتوصيف ترتيب التعميم الجزئي ونوع المسائل، مما يؤدي في النهاية إلى تحديد فئة من الأنواع حيث تختزل هذه الخصائص إلى شبكة التطابق للجبر الحر ذي المولد الواحد، وإثبات أنواع التعميم الوحدوية في مختلف البنى الجبرية والمنطقية.