1215 ورقة بحثية
تقدم هذه الورقة البحثية \textsc{CB-Ver}, وهو إطار عمل معياري يتحقق من خصائص مستوى التحكم في الشبكة المستقرة نهائياً عبر تركيب والتحقق من صحة "رسم بياني للتقارب قبل" (converges-before graph) من خلال فحوصات مكونات متوازية قائمة على حل مشكلات التماثل (SMT) وبراهين سلامة صورية في لغة Lean، مع تمكين التوليد التلقائي لواجهات المكونات من خصائص الصحة المنشودة.
تقدم هذه الورقة إطار عمل للتحقق الرسمي ينمذج حيز عمل آلة التحكم الرقمي بالحاسوب (CNC) ككومة مكانية ويطبق منطق الفصل للكشف عن التصادمات الفيزيائية باعتبارها سباقات بيانات منطقية، مما يقلل الاعتماد على المحاكاة التكرارية من أجل تصنيع ذاتي أكثر أماناً.
يُعد Lean Refactor إطار عمل وكيلًا يعتمد على الاسترجاع المعزز، يعمل على تحسين براهين Lean لتحقيق أهداف متعددة — بما في ذلك ضغط الرموز (tokens)، وسرعة التجميع، وتوافق الإصدارات — من خلال الاختيار الديناميكي لاستراتيجيات إعادة الهيكلة المنسقة دون الحاجة إلى إعادة تدريب النموذج.
تقدم هذه الورقة "الصورية الزائفة" (Pseudo-Formalization)، وهي تنسيق برهان هجين يجمع بين مرونة اللغة الطبيعية والنمطية الصورية، وخوارزمية "التحقق بالكتل" (Block Verification) المقابلة لها والتي تتفوق بشكل كبير على النماذج المرجعية الحالية لـ "النماذج اللغوية الكبيرة كحكم" (LLM-as-judge) في التحقق بدقة من البراهن الرياضية عبر اختبارات مستوى الأولمبياد والمستوى البحثي.
تقدم هذه الورقة "منطق الماضي السببي" (CPL)، وهو منطق زمني على مستوى المصدر مدمج في إطار عمل "ZiZiGen"، والذي يُمكّن وكلاء النماذج اللغوية الكبيرة (LLMs) الموزعين من إجراء التحقق من صحة وقت التشغيل لتدفق التحكم بناءً على الأحداث المرئية سببيًا بدلاً من السجلات التسلسلية، وذلك باستخدام مراقب ساعة المتجهات لضمان الصحة الدلالية.
تقدم هذه الورقة منهجية عامة تُفكك خصائص -منتظمة إلى التزامات توقف شبه مؤكد، مما يُمكّن من بناء أول شهادات سوبر مارتينجال (supermartingale) سليمة وكاملة (أو -كاملة) للتحقق من الخصائص -المنتظمة شبه المؤكدة والكمية على سلاسل ماركوف متجانسة زمنياً ذات فضاءات حالات قابلة للعد اللانهائي.
تقدم هذه الورقة Krympa، وهي أداة لتقليص البراهين نجحت في اختزال برهان تيرينس تاووي المكون من 62 خطوة إلى 20 خطوة، كما ضغطت بشكل كبير براهين أخرى معقدة عبر الجمع بين القوة الغاشمة، والاستدلالات، وعدة أدوات إثبات آلية.
تقترح هذه الورقة إطار عمل للتحقق الاستنتاجي القائم على العقود باستخدام برنامج التحقق Dafny لإثبات صحة جميع التجسيدات القانونية ضمن أنظمة الجدولة المقيدة غير المتزامنة (SRA) القابلة للضبط، وذلك عبر الجمع بين قواعد الإثبات التركيبية، والتلخيص التلقائي للطرق، وتبسيط فضاء التكوين.
تقدم هذه الورقة نظرية نوع خطي معتمد مبتكرة تتيح للمتعددات المتغيرة أن تعتمد على متغيرات أخرى، مما يوفر توصيفات دقيقة للموارد للبرامج التفرعية والعودية من خلال تضمين المنطق الخطي في نظرية النوع المعتمد، مدعومة بدلالات فئوية وتنفيذ بلغة Agda.
تقدم هذه الورقة تقنية جديدة لإزالة الفسيفساء الفائقة (hypermosaic elimination) لإثبات إمكانية حساب مستنتجات كرايغ (Craig interpolants) في المنطقيات الجهوية الهجينة القياسية في زمن أسي رباعي، مع إثبات عدم قابلية التقرير في وجود المستنتجات الموحدة (uniform interpolants) في هذه المنطقيات في الوقت ذاته.