1215 ورقة بحثية
تقدم هذه الورقة لغة توصيف ممتدة قائمة على المجموعات وخوارزمية ترجمة ذات تعقيد خطي تتيح التحقق الآلي بالكامل وقابل للتوسع من البرامج الكمومية بأسلوب "هوار" (Hoare-style) عبر تجنب التضخم الأسي المتأصل في النهج السابق القائم على الأتمتة.
تقترح هذه الورقة إطاراً للمنطق الإبستيمي الديناميكي لبروتوكولات النميمة ذات التصحيح الذاتي، مما يمكّن الأنظمة الموزعة من تصحيح أخطاء الإرسال ذاتياً دون تنسيق مركزي، مع تحليل التأثيرات الناتجة على الأمثلية ومقارنة النهج ببروتوكولات الذاكرة المحدودة والبروتوكولات كاملة المعلومات.
تُثبت هذه الورقة البحثية قابلية الحوسبة لمسافة التحرير للمحولات ذات القيم المحددة، مما يوسع نتيجة معروفة سابقاً للمحولات الوظيفية إلى فئة أكثر تعبيراً بشكل صريح.
تقدم الورقة البحثية إطار عمل MANTRA، الذي يقوم تلقائياً بتوليف والتحقق رسمياً من معايير قياس الامتثال القابلة للتوسع والقابلة للفحص آلياً لوكلاء النماذج اللغوية الكبيرة (LLMs) المستخدمة للأدوات، وذلك عبر توليد نماذج عالم رمزية وفحوصات على مستوى التتبع مدعومة ببرمجيات التحقق من النماذج (SMT) من أدلة إجرائية مكتوبة بلغة طبيعية.
تقدم هذه الورقة براهين الصحة الدلالية للتفاضل الآلي في الوضع الأمامي في لغة ذات رتبة أعلى مع أنواع بيانات جبرية من خلال توصيف الطريقة بوصفها ماكرو فريداً حافظاً للبنية وتأسيس صلاحيتها عبر بناء لصق على الفضاءات التفاضلية (diffeological spaces) يمتد إلى المشتقات من الرتب العليا عبر تقريب تايلور.
تقدم هذه الورقة دلالات جبرية جديدة لمنطق هورن العلائقي والجزئي عبر بناء نماذج حرة باستخدام حجة الكائن الصغير، والتي تُوصّف الإرضاء المنطقي من خلال المورفيزمات المصنِّفة وتوفر الأساس النظري لمحرك Eqlog Datalog.
تقدم هذه الورقة نماذج كريبكي من الرتب العليا (المتداخلة)، وهي تعميم تكون فيه العوالم نفسها نماذج من رتب أدنى، لتوفير إطار موحد للمنطقات الحدسية وغير الكلاسيكية التي تحافظ على التناظر بين علاقات الوصول والبديهيات الجهوية.
تقدم هذه المساهمة "حلقة التخمين والإثبات" (CPL)، وهي مسار عمل يستفيد من التعلم القائم على السياق لنموذج لغوي كبير عبر تغذيته بشكل تكراري بنظرياته وبراهينه التي تم التحقق من صحتها رسميًا بلغة "Lean 4"، مما يؤدي إلى زيادة كبيرة في معدل اكتشاف ونجاح التخمينات الرياضية الجديدة والصعبة الإثبات.
تقترح هذه الورقة نهجاً احتمالياً قابلاً للتوسع لتحليل أخطاء التقريب في الفاصلة العائمة من خلال تطبيق متباينات التركيز على متسلسلات تايلور، مستخدمةً تقريبات عليا سليمة وتقسيماً للنطاقات للتغلب على العقبات الحسابية مع تحقيق كفاءة زمنية أعلى بكثير من الأساليب المتطورة الحالية بدقة مماثلة.
تُثبت هذه الورقة أن نماذج "ترانسفورمر" ثنائية الاتجاه العميقة بما يكفي يمكنها تحقيق أداء بمستوى "سلسلة الأفكار" الصريحة في الاستنتاج الاستنباطي الضمني لـ "جمل هورن"، وذلك عبر القضاء على الارتباطات الزائفة وفرض المحاذاة الخوارزمية، رغم أن الاستدلال الصريح يظل ضرورياً للاستقراء إلى أعماق أكبر.