1215 ورقة بحثية
تقدم الورقة البحثية MathConstraint، وهو معيار تكيفي يقوم بتوليد مسائل الاستدلال التوليفي الصعبة والتحقق منها بصرامة بشكل تلقائي لتقييم النماذج اللغوية الكبيرة، مما يظهر أن الوصول إلى الأدوات يعزز الأداء بشكل كبير مع الكشف عن حساسية النماذج العالية تجاه تقليص ميزانيات استدعاء الأدوات.
تقدم الورقة البحثية "محول الاستنتاج الشبكي" (LDT)، وهو نموذج متكرر يحقق دقة تقارب الكمال في الألغاز المنطقية المعقدة مثل السودوكو والمتاهات من خلال تقريب الاستنتاج السليم عبر الإسقاطات الشبكية والتفسير المجرد، متفوقاً بشكل كبير على النماذج اللغوية الكبيرة الرائدة مع الحفاظ على السلامة التجريبية.
تقترح هذه الورقة إطاراً رياضياً باستخدام نظرية المجموعات الموضعية (sheaf theory) لضمان اتساق الرؤى المتعددة في بنيات النظم السيبرانية الفيزيائية، مُثبتةً من خلال براهين تم التحقق منها آلياً باستخدام لغة Lean 4 أن الاتساق التصميمي العالمي يمكن ضمانه عبر التحقق من توافق الواجهات ثنائية الاتجاه.
تقدم هذه الورقة تمثيلاً لتركيب (syntax) عاماً، ومحدد النطاق، وغير مسمى محلياً لـ Agda، مُعايراً بتواقيع ربط على طراز بلوتكين (Plotkin-style)، مع إثبات كفايته مقابل التركيب المسمى الساذج (naive nameful syntax) بموجب التحويل ألفا (alpha-conversion)، وتوضيح فائدته من خلال الأمثلة.
تثبت هذه الورقة قابلية التقرير لمنطق المتغيرين على الكلمات البيانات الممتدة بمسندات منتظمة محروسة من خلال تقديم أوتوماتا المجموعات وإثبات أن المنطق يكون قابلاً للتقرير تحديداً عندما يكون المونويد الأساسي متماثلاً مع مثاليات ثنائية الجانب مرتبة خطياً، وهي نتيجة تم تحقيقها عن طريق اختزال المشكلة إلى فراغ أوتوماتا متعددة العدادات مرتبة.
تقدم هذه الورقة TreeWidzard، وهو محرك موحد يسهل تطوير ودمج خوارزميات البرمجة الديناميكية القائمة على عرض الشجرة (treewidth) لتقرير خصائص الرسوم البيانية المعقدة ودعم إثبات النظريات الآلي.
تقدم هذه الورقة أداة لاستنتاج المواصفات لـ Move Prover تعمل على دمج تحليل الشرط الأضعف السليم مع واجهة سطر أوامر برمجية وكيلية (agentic coding CLI) لتوليد وتحسين مواصفات التحقق تلقائياً، مما يقلل بفعالية من العمل الروتيني اليدوي مع التعامل مع الخصائص المعقدة مثل ثوابت الحلقات والثوابت الهيكلية.
تتقصى هذه الورقة التوقعات العامة بوصفها دالات متجانسة إيجابياً، مبرهنةً أنه يمكن تمثيلها كقيم صغرى لتوقعات تحت خطية وقيم عظمى لتوقعات فوق خطية، مما يؤسس تقارباً (homeomorphisms) بين فضاءات التوقعات وفضاءات فوقية محددة عبر بناء فضاء القوى المزدوج.
تستقصي هذه الورقة قدرات العدّ متعدد الحدود لشبكات الأعصاب الممررة للرسائل (MPNNs)، حيث تُثبت قدرتها على التحقق من قيود متعددة الحدود عالمية ومحلية محددة في الرسوم البيانية ذات العقد المسمّاة باستخدام تجميع المتوسط، لا سيالما في ظل ظروف مثل الرسوم البيانية المنتظمة، أو الأنماط غير المتداخلة، أو الهياكل الشبيهة بالأشجار.
تثبت هذه الورقة أن المنطق من الدرجة الأولى مع العد بمقياس (FOMOD) قابل للاختبار في وقت ثابت على الرسوم البيانية المحدودة (الدرجة وحجم المكونات المحدودة)، وذلك عبر تكييف الصيغة الطبيعية لـ "هانف" وتقديم شرط "قابلية الرقع" (patchability) جديد ذي طبيعة نظرية عددية، مما يحل مسألة مفتوحة تتعلق بقابلية الاختبار في وقت ثابت لمنطق الدرجة الثانية الأحادي مع العد على هذه الفئات.