1215 ورقة بحثية
تقترح هذه الورقة نهجاً مبتكراً لتعداد النماذج القضوية الجزئية المنفصلة يلغي الحاجة إلى بنود الحجب من خلال دمج تعلم البنود المدفوع بالصراع، والتراجع الزمني، وتقليص المقتضيات، مما يتغلب على القيود المتعلقة بالذاكرة والأداء المرتبطة بالطرق التقليدية.
تقدم هذه الورقة حليّين جديدين، tabularAllSAT وtabularAllSMT، اللذين يستخدِمان تعلم العبارات المدفوع بالصراع مع التراجع الزمني وخوارزمية تقليص المقتضيات الهجومية لحصر التعيينات المرضية المنفصلة لمسائل SAT وSMT بكفاءة دون الاعتماد على عبارات الحظر.
تُثبت هذه الورقة أن مبرهنات البرهان الهرمية تحقق اختزالاً أسياً في تعقيد العينات مقارنة بالمبرهنات المسطحة، وذلك من خلال تعلم هياكل برهان قابلة لإعادة الاستخدام من آثار المعلم، مما يتجنب التكرار غير الضروري للبرهنات الفرعية الصعبة المتأصل في التمثيلات المسطحة.
تقدم الورقة البحثية MathlibPR، وهو معيار مستمد من سجلات طلبات السحب الحقيقية لـ Lean/Mathlib4، لتقييم قدرة النماذج اللغوية الكبيرة والوكلاء على التمييز بين المساهمات الجاهزة للدمج وتلك غير المدمجة، مما يكشف عن معاناتهم الحالية ويسلط الضوء على إمكانات المعيار في تطوير مساعدي المراجعة ونماذج المكافأة.
تقدم هذه الورقة Piccolo، وهو إطار عمل "الاعتماد-الضمان" (rely-guarantee) مبتكر يعمم الاستدلال التركيبي على أي نموذج ذاكرة بديهي، ويوفر تحديداً أول تقنية إثبات للذاكرة المشتركة المتسقة سببيًا باستخدام دلالات تشغيلية قائمة على الجهد ولغة تأكيد قادرة على تحديد تسلسلات مرتبة من حالات الخيوط.
يُعد AutoQ 2.0 مُحقِّقاً متقدماً يوسع نطاق التحقق من الدوائر الكمومية ليشمل البرامج الكمومية الكاملة عبر معالجة التحديات النظرية والهندسية المتعلقة بالتدفق الكلاسيكي للتحكم، وقد أثبت نجاحه بكفاءة في خوارزميات معقدة مثل "التكرار حتى النجاح" والبحث في خوارزمية "غروفر" القائم على القياس الضعيف.
تقدم هذه الورقة أول تقنية للإجابة على الاستعلامات الموجهة بالأهداف للتبعية من الدرجة الأولى والدرجة الثانية مع المساواة، والتي تجمع بين متغير تصغير مصحح، وتحليل صلة، وتكييف لمجموعات السحر لتسريع معالجة الاستعلام بشكل كبير عن طريق تجنب الاستنتاجات غير ذات الصلة.
تضع هذه المقالة حدوداً عليا وسفلى جديدة للعدد الأدنى من الحدود أو البنود المطلوبة لإنشاء صيغة DNF أو CNF تحتوي على من التعيينات المرضية بالضبط، وذلك من خلال إثبات إمكانية إنشاء صيغة DNF رتيبة (monotone) بـ من الحدود، مع إظهار أن من الحدود ضرورية لقيم معينة لـ في الوقت ذاته.
تقدم هذه الورقة البحثية "الدوال الأسية المنتظمة" (expregular functions)، وهي فئة متينة من الدوال التي تحول السلاسل إلى سلاسل وتتميز بنمو أسي، مُعرفة عبر ثلاثة نماذج متكافئة (تفسيرات مجموعات MSO، وآلات yield-Hennie، ومحولات Ariadne)، وتثبت تكافؤها لإثبات أن تفسيرات مجموعات MSO هي عاكسة للانتظام، مما يحل حدسية كبرى تتعلق بنظرية MSO القابلة للتقرير للكلمات -الآلية.
تقدم هذه الورقة دلالات نظرية برهانية بيانية للمربع السيميائي لغريماس باستخدام المخططات العنكبوتية، حيث يتم التقاط عملية تكوين المصطلح الفوقي كعملية اشتقاق بنائية، ويُعاد تفسير النفي بوصفه تقابلاً دلالياً مقيداً بدلاً من كونه مكملاً بولياً.