1215 ورقة بحثية
تُثبت هذه الورقة أن المواصفات التي يتم إنشاؤها بواسطة وكيل ذكاء اصطناعي واحد لعمليات الهجرة من Oracle إلى PostgreSQL غالبًا ما تفشل في الانتقال بفعالية إلى وكلاء آخرين، مما يكشف عن تدهور كبير يعتمد على الوكيل في جودة التنفيذ ويسلط الضوء على الحاجة إلى استراتيجيات صريحة مثل التلقيم المعزز بالاسترجاع لضمان التوافق عبر الوكلاء في سير عمل هندسة البرمجيات.
توسع هذه الورقة علاقة التكافؤ الثنائي بين كليرمبولت-ديبجير (Clairambault-Dybjer) بين الفئات محلياً كارتيزية مغلقة (locally Cartesian closed categories) والفئات الديمقراطية ذات العائلات (democratic categories with families) لتشمل الفئات أحادية الوحدة (univalent categories) وفئات متنوعة من التوبوسات (toposes)، مبرهنةً أن لغاتها الداخلية تقابل نظرية نوع مارتن-لوف (Martin-Löf type theory) الامتدادية مع المجموعات والمنتجات التابعة، مع صياغة جميع النتائج رسمياً في Rocq باستخدام مكتبة UniMath.
يقدم هذا البحث نموذج كتلة دلالية رسمياً ومعياراً تقييمياً محكوماً بالتنفيذ لتقييم جودة المواصفات بشكل مستقل عن قدرة النموذج، موضحاً من خلال دراسة حالة لهجرة من Oracle إلى PostgreSQL أنه بينما يعد الحتمية مفهوماً رسمياً صالحاً، إلا أنها لا تعمل بعد كمعيار جودة تجريبي قائم بذاته للنماذج اللغوية الكبيرة المعاصرة بسبب التباين الكبير في التنفيذ.
تقدم هذه الورقة معياراً بسيطاً وعاماً للدمج المعجمي لأزواج الاختزال عبر فئات متنوعة، وتستقصي متغيراً للتفسيرات المصفوفية باستخدام الترتيب المعجمي، مبرهنةً على فعاليتها من خلال التجارب والأمثلة مثل معركة هيدرا لتوزيه.
تقدم هذه الورقة "هيبوجريف" (Hippogriff)، وهي لغة ذات نظام وحدات موحد ونظرية أنواع معتمدة تدعم العودية العامة دون المساس بإنهاء التحقق من الأنواع، وتوفر دلالات فئوية لتبرير هذا التصميم عبر ربط الأنواع المعتمدة بنظريات الأنواع ذات السياق المنقسم.
تقترح هذه الورقة إطار عمل حماية احتماليًا تكيفيًا للتعلم التعزيزي الآمن يدمج تعلم النموذج عبر الإنترنت لحساب وتحديث قيود السلامة ديناميكيًا مع تقدير احتمالات الانتقال من عملية قرار ماركوف غير معروفة في البداية.
تقدم هذه الورقة دوال الاحتمال وتُوصّفها بديهياً بناءً على منطق LETK+ ذي القيم الست المحدودة (paradefinite)، مستخدمةً دلالات بنية الالتواء (twist structure semantics) للتعامل مع فجوات القيم الحقيقية، والزيادات (gluts)، والموثوقية، مع إرساء مبدأي السلامة والتمام، والتكافؤ الدلالي-النحوي لتحديث جيفري (Jeffrey's update).
تقدم هذه الورقة "مخططات العودية العليا الاحتمالية" (PHORS) كنموذج للبرامج الاحتمالية العليا من الرتب، وتثبت أن التوقف شبه المؤكد غير قابل للتقرير لمخططات PHORS من الرتبة الثانية، وتقترح إجراءً قائماً على النقطة الثابتة يكون سليماً للحساب التقريبي لاحتمالات التوقف، وهو ما تم التحقق من صحته من خلال تجارب أولية.
تُبين هذه الورقة أن مفارقة راسل يمكن ترميزها مباشرة في نظرية النوع باستخدام كون "النوع هو نوع" (type-in-type) مقترناً بأنواع سيجما (sigma types) وإما الهوية الامتدادية (extensional identity) أو الهوية الجوهرية (intensional identity) مع تفرد براهين الهوية، مما يوضح عدم اتساق مثل هذه الأنظمة.
تقدم هذه الورقة إطار عمل RDFdL، الذي يدمج الرسوم البيانية للمعرفة من نوع RDF مع المنطق الديناميكي التفاضلي لتمكين تمثيل والتحقق الرسمي من كل من المعرفة الساكنة والديناميكيات الفيزيائية المستمرة، مما يسمح بالاستعلام عن خصائص السلامة والوصول إلى الهدف للأنظمة السيبرانية الفيزيائية عبر لغة SPARQL.