1215 ورقة بحثية
يُعد Agentproof نظام تحقق استاتيكي يقوم تلقائياً باستخراج نماذج رسوم بيانية موحدة من أطر عمل الوكلاء الرئيسية للكشف عن العيوب الهيكلية وفرض سياسات السلامة الزمنية عبر لغة وصفية متخصصة وتحليل قائم على الأوتوماتات المحدودة الحتمية (DFA)، مما يكمل حواجز الحماية أثناء التشغيل من خلال تحديد المشكلات على مستوى الطوبولوجيا قبل النشر.
تقدم هذه الورقة "ألعاب التغطية"، وهي إطار عمل جديد للتخطيط متعدد الوكلاء حيث يتنافس "المُغطي" الذي يدير عدة وكلاء ضد "مُعطّل" لتحقيق مجموعة من الأهداف، مع تقديم تحليل نظري شامل لمدى حتميتها، وتفكيك أهدافها، وتعقيدها الحسابي.
تفيد هذه الورقة أن نموذج Claude Opus 4.6، باستخدام أدوات بروتوكول سياق النموذج (Model Context Protocol) لمساعد الإثبات Rocq واستراتيجية "التجميع أولاً، ثم التراجع التفاعلي"، قد حل بشكل مستقل 10 من أصل 12 مسألة من مسابقة بوتنام الرياضية لعام 2025 في بيئة غير متصلة بالإنترنت.
تقترح هذه الورقة "المنهج الحر" للرياضيات الصورية، وهو بديل متاح للمنهج المعياري المعقد الذي يركز على التصديق ويعطي الأولوية للتواصل وسهولة الاستخدام للممارسين العاديين عبر إزالة الالتزام بالتحقق الميكانيكي من كل تفصيل.
تكشف هذه الورقة أن حساسية ضغط المحولات (transformer compression) تتفاوت بخمس مراتب عشرية عبر أنواع محددة من المصفوفات، مما يثبت أنه بينما يضمن استقرار ليابونوف (Lyapunov stability) تقليص الخطأ، فإن الفائض المرتبط بالبنية المعمارية (architecture-specific redundancy) يعد حاسماً بنفس القدر لتحقيق المتانة، وهو اكتشاف تم التحقق من صحته من خلال اختبار تجريبي واسع النطاق وتم إثباته رسمياً عبر عشر مبرهنات في لغة "لين 4" (Lean 4) تم التحقق منها آلياً.
تقدم هذه الورقة خوارزمية ذات زمن حدودي تقرر وجود حالات التعليق الحي (livelocks) في الحلقات المتناظرة أحادية الاتجاه ذات المعلمات من العمليات ذات التعطيل الذاتي، وذلك عبر حساب النقطة الثابتة العظمى لمؤثر رتيب على الانتقالات المحلية، مما يضمن خلو الحلقات من التعليق الحي لجميع أحجام الحلقات دون بحث صريح.
تنتقد هذه الورقة بديهية "المسارات متصلة" في الفئات الشجرية عبر اقتراح المفهوم المنقح لـ "الاتصال الشجري" لمعالما أوجه القصور فيها مع الحفاظ على الخصائص الجوهرية، وتثبت علاوة على ذلك أن دالة المسار تشكل رفيراً من نوع ستريت (Street fibration).
تثبت هذه الورقة أنه في حين أن توسيع الأنظمة التوليدية يمكن أن يزيد من قدراتها، إلا أنها تواجه عوائد تناقصية تقاربية في تغطية المهام وقيوداً منطقية جوهرية على الاستنتاج مستمدة من مبرهنات غودل-تارسكي-لوب.
تحلل هذه الورقة مدى إيجاز سلاسل أوتوماتا كوه-بوشي (COCOA)، مبيّنة أنه بينما يمكن أن تكون أكثر إيجازاً بشكل أسي من أوتوماتا التكافؤ الحتمية، إلا أن هذه الميزة تُفقد عند إجراء العمليات البولية مثل الفصل أو التقاطع أو الاستكمال، والتي تستلزم زيادة أسية في الحجم.
تقترح هذه الورقة مراقباً وقت تشغيل جديداً، قابلاً لإعادة البرمجة ديناميكياً، ومُنفذاً باستخدام خلايا قياسية على نفس الرقاقة مع النظام الخاضع للتحقق، مما يتيح مراقبة عالية السرعة وبسرعة التشغيل لخصائص المنطق الزمني الممتد (MTL) محددة الوقت، بمساحة مدمجة تبلغ 0.55 مم² وتردد تشغيل يصل إلى 1.25 جيجاهرتز.