1215 ورقة بحثية
تقدم هذه الورقة البحثية DateSAT، وهو أول إطار عمل للتعبير الصوري وحل قيود القابلية للإشباع المتعلقة بالتواريخ والفترات التقويمية عن طريق اختزالها إلى صيغ SMT قائمة على الأعداد الصحيحة، وتتحقق من فعاليته من خلال تقييم تجريبي على مجموعة بيانات منسقة تضم 450 قيداً.
تقدم هذه الورقة البحثية "BBT-spectral"، وهي طريقة تكميم تركز على الجانب الهندسي تطبق دورات "والش-هادامارد" التكيفية مع التأثير وإعادة قياس قائمة على الطاقة على مصفوفات الأوزان، مما يقلل بشكل كبير من الحيرة (perplexity) في تكميم النماذج اللغوية الكبيرة ذات البتات المنخفضة للغاية (W2A16) عبر مختلف بنيات النماذج مع ضمان التوافق مع الأجهزة من أجهزة إنتل.
تقترح هذه الورقة إطار عمل لإعادة الهندسة من نوع (Code2Text2Code) قائم على المواصفات، يعمل على الحد من الانحراف الدلالي وعدم الاتساق السلوكي في تطور البرمجيات بوساطة النماذج اللغوية الكبيرة، وذلك عبر تحويل الكود المصدري إلى مواصفات نصية محايدة للتحقق التكراري قبل إعادة توليد الكود المستهدف.
تقدم هذه الورقة تقنية "الالتقاط اللحظي لحالة البرهان" (proof-state snapshotting) لـ Lean 4، وهي تقنية تعمل على التقاط وإعادة استخدام حالات البرهان المفصلة عبر فروع البحث المتوازية للقضاء على عمليات تحميل الاستيرادات وتفصيل متن المبرهنة المكررة، مما يحقق تسريعاً في وقت التنفيذ الفعلي يتراوح بين 5.6 و50 ضعفاً لعمليات الإثبات الآلي للمبرهنات.
تُثبت هذه الورقة نظرية إعادة تمثيل تُظهر أن استعلامات الرتبة الثانية المونادية والرتبة الأولى على السلاسل المتناهية ذات أحجام المخرجات المحدودة حدودياً يمكن تحديدها باستخدام منطق الرتبة الثانية المونادي (MSO) عبر عدد ثابت من المواضع وبيانات متناهية، مما يؤكد أن تقليل الأبعاد يتحقق في تفسيرات السلسلة-إلى-السلسلة من الرتبة الأولى.
تقدم هذه الورقة نظرية أنواع جديدة قائمة على نظرية الأنواع ذات المعلمات الداخلية الصفرية (Nullary Internally Parametric Type Theory) ومبدأ استقراء أسماء محدد، ينجح في توحيد قواعد النوع الصافية للتجريدات الاسمية الكلية مع قدرات مطابقة الأنماط القوية للتجريدات الوجودية، مما يؤسس إطاراً اسمياً منضبطاً لتمثيل البنية النحوية ذات الروابط.
تقدم هذه الورقة إطار عمل غير مرتبط بنظرية معينة لتعداد مجموعات كاملة من ليمات النظرية بكفاءة باستخدام تقنيات قابلة للتوسع مثل "فرق تسد" والتعداد المسقط، مما يتغلب على قيود الترميزات الاستباقية الكلاسيكية ويحسن الأداء بشكل كبير لمهام SMT المعقدة مثل استخراج النواة غير القابلة للإرضاء (unsat-core extraction) وMaxSMT.
تؤيد هذه الورقة استخدام شبكات التماثل العميق (DHNs) كبنية قوية لقواعد البيانات العلاقاتية من خلال إثبات تكافؤها التعبيري الدقيق مع أجزاء محددة من المنطق من الدرجة الأولى ولغة SQL، وإثبات قابلية التقرير لمشكلات التحليل الساكن الرئيسية، والتحقق من أدائها المتفوق من خلال التجارب.
تقدم الورقة البحثية ImProver 2، وهو إطار عمل عصبي رمزي يجمع بين التكرار الخبير كفؤ البيانات ونظام سقالات هيكلي لتمكين النماذج اللغوية الصغيرة من تحسين البراهين الصورية المعقدة في Lean 4 بفعالية، متفوقةً بشكل كبير على النماذج الأكبر حجماً مع ترسيخ تحسين البراهين كمهمة قابلة للتعلم والتوسع.
تقدم هذه الورقة البحثية نظام "التركيب الاستقرائي الاستنباطي" (IDS)، وهو نظام لغوي كبير وكيل يقوم بتوليد التنفيذات والبراهين الصورية للأنظمة الموزعة بشكل مشترك، محققاً نسبة نجاح بلغت 100% في مواصفات مخازن القيم المفتاحية مع تقليل الوقت والتكلفة بشكل كبير مقارنة بكل من الخبراء البشريين ووكلاء البرمجة الأكثر تطوراً.