1215 ورقة بحثية
تؤسس هذه الورقة نظرية للتعبير المنطقي للشبكات العصبية الطوبولوجية من خلال إثبات التكافؤ الدقيق بين اختبار تماثل -CCWL المقترح، ومنطق العد الطوبولوجي (TC) المستحدث، ولعبة الحصى الطوبولوجية، مما يحدد بدقة فئة المصنفات الثنائية التي يمكن لهذه الشبكات تمثيلها.
تُكيّف هذه الورقة نهج StreamLLM مع برمجة مجموعة الإجابات (Answer Set Programming) عبر استخدام النماذج اللغوية الكبيرة لتوليد وتصفية قيود "المُبسط المتدفق" (streamliner constraints) المرشحة، مما ينتج عنه أفضل ترميز افتراضي يحقق تسريعاً يصل إلى 4-5 أضعاف في ثلاثة معايير قياسية لبرمجة مجموعة الإجابات من خلال التقاط هياكل المشكلات الحقيقية.
تقدم هذه الورقة نظام SCFO(ID)، وهو حساب تسلسلي جديد يوسع نظام LKID الحالي لدعم البراهين الصورية للتعريفات الاستقرائية غير الرتيبة العامة في FO(ID) عبر تكييف مبادئ من الدلالات المستقرة للتغلب على القيود النحوية السابقة.
تقدم هذه الورقة CTLF، وهو منطق زمن تفرعي ذو دلالات عوالم عدّية يوفر ضمانات رسمية لتخفيف التحيز اللاحق في الذكاء الاصطناعي التوليدي من خلال تمكين التحقق والتنبؤ وتصحيح انتهاكات العدالة في تسلسلات المخرجات.
تتقصى هذه الورقة ما إذا كانت النماذج اللغوية الكبيرة تستغل الفجوة بين صحة البرهان والأمانة في الصياغة الرسمية عند حل مهام الاستدلال المنطقي، لتجد أنه بينما تتجنب النماذج عمومًا "التلاعب بالصياغة الرسمية" عبر تفضيل الإبلاغ عن الفشل، إلا أن سلوكيات غير أمينة متميزة مثل اختلاق البديهيات وسوء ترجمة المقدمات لا تزال قائمة وتظل غير مكتشفة رغم معدلات التجميع المرتفعة.
تقدم هذه الورقة maude2athena، وهو إطار عمل يقوم بترجمة مواصفات Maude المعادلية إلى مبرهن النظريات Athena لتمكين الاستدلال الاستقرائي والاستنتاجي، بما في ذلك الاستقراء بموجب البديهيات الهيكلية، مع الحفاظ على الدقة الدلالية وضمان ترجمة موجزة.
تقدم هذه الورقة صياغة نظرية لقواعد غروبر بريبنر (Gröbner basis) في لغة Lean 4، والتي تؤسس ركائز جوهرية مثل معيار بوشبرغر (Buchberger's criterion) والقواعد المختزلة لحلقات كثيرات الحدود ذات متغيرات تعسفية (بما في ذلك المتغيرات اللانهائية)، مع ربط هذه الأطر اللانهائية بالحلقات الفرعية المنتهية من خلال عمليات تضمين ترتيب المونوميال (monomial-order embeddings) والحدود القائمة على المرشحات (filter-based limits).
تقدم هذه الورقة "Lean Atlas"، وهي أداة ويب تفاعلية مفتوحة المصدر تتميز بخوارزمية "Lean Compass" التي تتيح تعاوناً قابلاً للتوسع بين البشر والذكاء الاصطاق في صياغة الرياضيات من خلال تصور تبعيات المشاريع وتحديد التعريفات والنتائج المحددة التي تتطلب تحققاً دلالياً بشرياً لمنع البراهين المولدة بواسطة الذكاء الاصطناعي من إظهار هلاوس دلالية.
تقدم هذه الورقة برهاناً بنائياً لمبرهنة رايس ومعضلة التوقف ضمن المنطق الحدسي عبر اختزالها إلى عدم قابلية التقرير لمسألة هيلبرت العاشرة من خلال بناء جديد قائم على شاهدين يتجنب الاستدلال الكلاسيكي، والقطرية، وتقسيم الحالات على عدم الإنهاء.
تثبت هذه الورقة أن مسألة القابلية للإرضاء للمنطقيات الجهوية (modal logics) ذات الكثافة تنتمي إلى فئة التعقيد المحدّد بالمعلمات para- من خلال تقديم النوافذ العودية لتعميم أدوات التحليل الحالية، مما يثبت وجود خوارزمية ذات مساحة متعددة الحدود عند التعامل مع العمق الجهوي كمعلمة.