1215 ورقة بحثية
تقدم هذه الورقة خوارزمية قابلة للحل في وقت محدد بمعالم (fixed-parameter tractable) للمحاكاة القوية للدوائر الكمومية المكونة من بوابات هادامارد وبوابات قطرية عبر تقييم سعات المخرجات في زمن أسي فقط في عرض الرتبة (rank-width) لمخطط متغير المسار، مما يتفوق بذلك على طرق المخططات البيانية للقرار وشبكات الموتر الحالية في عائلات دوائر محددة مع توحيد حدودها النظرية.
تقدم هذه الورقة مسار تحقق سليم ومفحوص عبر النواة يدمج أدوات استخراج لغة Rust إلى Lean، والمكتبات التشفيرية الرسمية، والمثبتات القائمة على الذكاء الاصطناعي لتوليد براهين صحة مدققة آلياً لكود تشفير Rust الإنتاجي ضمن مشروع zkEVM التابع لمؤسسة إيثيريوم بنجاح.
تثبت الورقة البحثية أن النظرية الوجودية لمنطق لوكاسيفيتش غير المحدود هي مسألة (NP-complete) من خلال اختزالها إلى النظرية الوجودية لجبر (MV) القياسي، مما يوفر حداً علوياً لتعقيد نظريات المنطق وعلاقة الاستتباع المحدودة.
تحل هذه الورقة البحثية المسألة المفتوحة المتعلقة بتعقيد حساب الإغلاقات الهابطة للغات المفهرسة من خلال إرساء حدود عليا ثلاثية ورباعية الأسس للأوتوماتا غير الحتمية والحتمية، على التوالي، إلى جانب حدود دنيا مطابقة، والتي تم تحقيقها عبر منهجية مبتكرة تحول القواعد المفهرسة إلى قواعد خالية من السياق باستخدام ملخصات الكلمات القائمة على نصف الزمرة.
يحلل هذا المقال المفارقات الأربع التي تمت مكننتها في مكتبة coq-paradoxes لتوضيح كيف تحدد هذه المفارقات مجتمعةً الحدود التصميمية الضرورية لنواة Rocq — وتحديداً فيما يتعلق بعدم القدرة على التنبؤ (impredicativity)، والاستبعاد الكبير (large elimination)، وقيود الكون (universe constraints) — من خلال توضيل الأسباب الدقيقة التي تجعل النظام يرفض بناءات معينة للحفاظ على الاتساق.
تقدم هذه الورقة البحثية التراجع الرسومي (graph backtracking)، وهو مخطط جديد وسليم لحل مشكلات التناقض (SAT) يعتمد على خوارزمية التمرير المعتمد على التناقض (CDCL)، ويقوم بتعميم التراجع الزمني وغير الزمني عبر استخدام رسوم بيانية للاستلزام ودوال وزن محددة من قبل المستخدم لتقليل الحروف غير المعينة، مما يقلل من عمليات الانتشار ويحسن وقت التشغيل كما هو موضح في برنامج NapSAT.
تقدم هذه الورقة COVCAL، وهو إطار عمل للتحكم في المخاطر يصادق على موثوقية استخدام الصياغة الرسمية بلغة "Lean" كحكم للمسائل الرياضية ذات اللغة الطبيعية من خلال الاختيار الديناميكي للإجابات بناءً على تغطية البرهان وإشارات التشخيص، مما يثبت أنه بينما تنتج أدوات الصياغة الرسمية التلقائية الصغيرة إشارة نادرة للغاية تمنع القبول المتحكم فيه في المخاطر، فإن أدوات الصياغة الرسمية المتخصصة تمكّن من الاختيار عالي الدقة تحت حدود مخاطر صارمة.
تُصوّر هذه الورقة تحسين الرموز (token optimization) كمسألة تحويل متعددة الأهداف ومقيدة لعملية الهجرة من Oracle إلى PostgreSQL القائمة على النماذج اللغوية الكبيرة (LLM)، حيث تقيم اثنتي عشرة استراتيجية لتثبت أنه بينما يؤدي الضغط الشديد إلى خفض الدقة الدلالية بشكل جذري، فإن التوجيه التكيفي وتقليم السياق الطفيف يقدمان أكثر المقايضات فعالية بين كفاءة الرموز وجودة الكود.
تحلل هذه الورقة تعقيد البيانات لاستعلام الاستلزام وتعداد الإصلاح لقواعد المعرفة ذات الأولوية غير المتسقة باستخدام ثلاثة مفاهيم إصلاح مثالية، مع إقامة مراسلات دقيقة بين هذه الإصلاحات وامتدادات أطر الحجاج لاقتراح دلالات جديدة وفعالة حاسوبياً مستوحاة من الامتدادات الراسخة.
تقدم هذه الورقة البحثية xMapleLCM، وهو برنامج لحل مشكلات التناقض المنطقي (SAT solver) يعتمد على خوارزمية CDCL، والذي يعزز الأداء في صيغ Tseitin وXORified من خلال إدخال متغيرات جديدة ديناميكياً لتعريف نقاط الاستلزام المزدوج (DIPs) داخل رسم الاستلزام البياني، مما يؤدي إلى تنفيذ استراتيجية تعلم بنود الاستدلال الموسعة التي تتفوق على البرامج الرائدة مثل MapleLCM وKissat وGlucoseER.