1215 ورقة بحثية
تقدم الورقة البحثية "التعلم التعزيزي عبر التغذية الراجعة الرمزية" (RLSF)، وهو نموذج جديد للضبط الدقيق يستفيد من أدوات الاستدلال الرمزي لتوفير تغذية راجعة دقيقة على مستوى الرمز (token-level)، مما يمكّن النماذج اللغوية الكبيرة الأصغر حجماً من التفوق بشكل كبير على النماذج المغلقة الأكبر حجماً في المهام التي تتطلب توافقاً منطقياً خاصاً بمجال معين.
تقدم هذه الورقة الـ EU-automata للأشجار اللانهائية ذات التعددية (arity) التعسفية، وتؤسس لخصائصها الخوارزمية وحدود تعقيدها، وتستفيد منها لاستخلاص إجراءات قرار مثلى ونتائج تقليل تبادل المكممات لـ QCTL وMSO.
تقدم هذه الورقة ألعاب المُثبِت-الخصم (Prover-Adversary games) بأسلوب بودلاك-بوس لتوصيف أنظمة الإثبات لبرامج التفرع الحتمية وغير الحتمية، حيث تُثبت وجود تكافؤات متعددة الحدود بين هذه الألعاب وأنظمة الإثبات eLDT وeLNDT، مع استخلاص نسخة من نظرية إيمر مان-سيزيلبيني في تعقيد الإثبات.
تؤسس هذه الورقة لبناء جبرات كليين (Kleene algebras) تلافيفية على فئات موبيوس (Möbius categories) معممة عبر تعريف عملية نجمة (star operation) مناسبة، مما يتيح الاستدلال والتحقق الجبري للبرامج الموزونة والاحتمالية والمتزامنة، وكذلك إعادة الكتابة عالية الأبعاد.
تقدم هذه الورقة LeanCat، وهي مجموعة معيارية من 100 مهمة في نظرية الفئات الرسمية بلغة Lean، والتي تكشف عن فجوة تجريد حادة في النماذج اللغوية الكبيرة الحالية، مما يثبت أن الوكلاء المعززين بالاسترجاع مثل LeanBridge ضروريون لتحقيق تقدم ملموس في الاستدلال الرياضي عالي المستوى والمستند إلى المكتبات.
تقترح هذه الورقة طريقةً للتفسير القائم على المنطق مع ضمانات للصحة تحقق دقة تفسير بنسبة 100% ومتانة فائقة مقارنةً بالنهج التجريبي، مما يعزز الثقة السريرية ويسهل نشر الأدوات المدعومة بالذكاء الاصطناًعي للتنبؤ بالموت المفاجئ بسبب السكتة القلبية لدى مرضى اعتلال عضلة القلب بمرض شاغاس.
تقدم هذه الورقة نماذج فيبرالية (fibrational)، وأوفيبرالية (opfibrational)، وديفلاسيونية (deflational) للنظريات المونيدية الطبقية، مع إثبات سلامتها واكتمالها، وتأسيس روابط مع البنى الفئوية الراسخة مثل فيبرات غروثنديك (Grothendieck fibrations) والفئات المعروضة (displayed categories).
تقدم هذه الورقة RustyDL، وهو منطق برامج جديد على مستوى المصدر صُمم لتمكين التحقق الاستنتاجي للبرامج بلغة Rust بمشاركة العنصر البشري، مع معالجة تحديات لغوية محددة وإثبات جدواه من خلال تنفيذ نموذج أولي ضمن أداة التحقق KeY.
تقترح هذه الورقة نهج تقطيع النطاق لتعزيز قابلية التوسع في التفسيرات القائمة على المنطق للشبكات العصبية، مما يظهر انخفاضاً في وقت التفسير يصل إلى 40% من خلال تجارب مقارنة.
تقدم هذه الورقة نظام ذكاء اصطناعي قابل للتفسير قائم على المنطق يعزز شفافية "مقياس فرامينغهام للمخاطر" من خلال تحديد الحد الأدنى من عوامل الخطر وتوليد سيناريوهات قاب la للتنفيذ لمساعدة الأطباء على فهم وتقليل مخاطر القلب والأوعية الدموية لدى المرضى.