1215 ورقة بحثية
تضع هذه الورقة أسساً للاستنتاج الآلي حول التكافؤ المخططي، لا سيما بالنسبة للدوائر الكمومية، من خلال تقديم والتحقق رسمياً (باستخدام Isabelle/HOL) من أنظمة إعادة كتابة المصطلحات النهائية والمتوافقة التي تعمل على تطبيع فئتين من المخططات السلسلية.
تُعرّف هذه الورقة رسمياً وتقيس قدرة "القفزة" لدى النماذج اللغوية الكبيرة — وتحديداً قدرتها على التخلي عن إكمال معياري افتراضي لصالح نظام بديهي فريد وصحيح — مُثبتةً أن النماذج الرائدة تؤدي هذه الخطوة بنجاح في جميع التجارب، مما يشير إلى أن أي عجز مزعوم يكمن في توليد القيود أو الأطر بدلاً من القفزة نفسها.
تقدم هذه الورقة عائلة جديدة من المعايير المرجعية لتكافؤ الدوائر المخططة بصيغتي TPTP وSMT-LIB، مع توفير نصوص برمجية للتوليد الآلي وتقييم أدائها على أحدث مبرهناتي النظريات الآلية ومحللات SMT عبر ثلاثة متغيرات من حيث الصعوبة.
تقترح هذه الورقة تفسير الـ cofunctors (أو الـ retrofunctors) بوصفها تنفيذات جزئية تؤجل خيارات خلفية محددة، مثل تمثيلات البيانات والخوارزميات، حتى وقت التشغيل بناءً على حالة النظام.
تقدم هذه الورقة إطاراً جبرياً موحداً قائماً على المونادات المتدرجة والجبر الكلي لضبط وتوصيف التكافؤات السلوكية، وتحديداً احتواء الأثر والتكافؤ تحت دلالات الحداثة العالمية والمحلية، للأنظمة الاسمية ذات تخصيص الأسماء.
تقدم هذه الورقة صياغة في لغة Lean 4 لتكامل ديريكليه وتطبيقاته، بما في ذلك صيغة لوباتشيفسكي، وذلك عبر توظيف استراتيجية تستخدم دالة sinc المربعة القابلة للتكامل مطلقاً وكثافة كثيرات حدود جيب التمام للتعامل بصرامة مع التقارب الشرطي واشتقاق هويات تكامل مثلثية متنوعة.
توسع هذه الورقة تقنية تجريد المسار من احتمالات الوصول في سلاسل ماركوف ذات الزمن المنفصل إلى المكافآت المتوقعة في نماذج مكافأة ماركوف، حيث تثبت أنها تحافظ على بنية النموذج والرتابة مع توفير طريقة عددية لحسابها بناءً على أوقات الزيارة المتوقعة.
تقدم هذه الورقة FLARE، وهي طريقة تستفيد من النماذج اللغوية الكبيرة ومساعد الإثبات Lean للتحقق رسميًا من صحة إعادة صياغة البرمجة الخطية للأعداد الصحيحة المختلطة (MILP)، محققةً دقة بنسبة 100% على معيار مرجعي صعب مع توفير شهادات قابلة للتحقق آليًا.
تقدم الورقة البحثية MathAdv، وهو معيار تشخيصي شامل يمتد عبر 13 مجالاً رياضياً يقيم أثباتات النظريات من خلال مهام مساعدة متعددة للكشف عن الاختناقات الحرجة في الصياغة الرسمية، والتباينات في الأداء الخاصة بكل مجال، وحدود المتانة التي غالباً ما تحجبها مقاييس الدقة التجميعية.
تقدم هذه الورقة المنطق متعدد الوجوه الديناميكي عبر توسيع المنطق الطوبولوجي الديناميكي بدلالات متعددة الوجوه وعامل وصول مكاني قائم على المسار، مما يثبت في النهاية سلامة واكتمال بديهياته للأنظمة الديناميكية العكسية.