التحقق الرسمي من تحويل مصفوفة COO إلى CSR المتفرقة (ورقة مدعوة)

المعلومات الأساسية

• معرّف الورقة: 2510.13412
• العنوان: التحقق الرسمي من تحويل مصفوفة COO إلى CSR المتفرقة (ورقة مدعوة)
• المؤلف: Andrew W. Appel (جامعة برينستون)
• التصنيف: math.NA cs.LO cs.NA
• وقت النشر/المؤتمر: VSS 2025 (ورشة العمل الدولية للتحقق من برامج العلوم)، EPTCS 432، 2025
• رابط الورقة: https://arxiv.org/abs/2510.13412

الملخص

تصف هذه الورقة إثباتاً للصحة تم التحقق منه بواسطة الآلة لبرنامج C يقوم بتحويل مصفوفة متفرقة بصيغة الإحداثيات (COO) إلى مصفوفة الصفوف المتفرقة المضغوطة (CSR). على الرغم من أن الخوارزمية الكلاسيكية (ترتيب إدخالات COO حسب الترتيب المعجمي للصفوف والأعمدة؛ ملء مصفوفات CSR من اليسار إلى اليمين) موجزة، إلا أنها تتمتع بثوابت معقدة جداً. تعرض الورقة منهجية من الأسفل إلى الأعلى لاستخلاص الثوابت من البرنامج.

خلفية البحث والدافع

تعريف المشكلة

1. المشكلة الأساسية: تُستخدم المصفوفات المتفرقة على نطاق واسع في الحسابات الرقمية، لكن خوارزميات تحويل المصفوفات المتفرقة الموجودة تفتقر إلى التحقق الرسمي، مما قد يؤدي إلى أخطاء يصعب اكتشافها
2. الأهمية: ضرب المصفوفة المتفرقة بالمتجه هو عملية أساسية في الطرق الرقمية، والتحويل الخاطئ يؤدي إلى فشل السلسلة الحسابية بأكملها
3. القيود الحالية: تعتمد طرق التحقق التقليدية على اختبارات الانحدار وما شابه، ولا يمكنها توفير ضمانات رياضية للصحة
4. الدافع البحثي: من خلال إثبات رسمي يتم التحقق منه بواسطة الآلة، ضمان الصحة المطلقة لتحويل COO إلى CSR، ووضع أساس لبرامج علمية قابلة للتحقق

السياق التطبيقي

• تمثيل المصفوفات المتفرقة: صيغة COO مناسبة للبناء، وصيغة CSR مناسبة لعمليات الضرب
• تحليل العناصر المحدودة: كل رأس داخلي في الشبكة ينتج عنه عدة صفوف إحداثيات، مما ينتج بشكل طبيعي عن إدخالات مكررة
• الدقة الرقمية: عدم الترابطية للعمليات الحسابية بالفاصلة العائمة تجعل ترتيب جمع الإدخالات المكررة يؤثر على النتيجة

المساهمات الأساسية

1. أول إثبات تم التحقق منه بواسطة الآلة لصحة تحويل COO إلى CSR: باستخدام مجموعة أدوات البرامج القابلة للتحقق (VST) ومساعد إثبات Coq
2. منهجية مبتكرة لاستخلاص ثوابت الحلقة: اقتراح منهجية من الأسفل إلى الأعلى، واستخلاص ثوابت الحلقة المعقدة من الخصائص التي يجب أن يفي بها البرنامج
3. فصل البنية البيانية والاستدلال التقريبي: فصل استدلال بنية البيانات لبرنامج C عن استدلال التقريب بالفاصلة العائمة، مما يبسط تعقيد التحقق
4. مكونات التحقق القابلة للتركيب: توفير وحدة تحويل مصفوفة متفرقة تم التحقق منها يمكن إعادة استخدامها في أنظمة تحقق أكبر
5. اكتشاف الأخطاء العملية: اكتشاف وإصلاح 5 أخطاء في البرنامج أثناء عملية الإثبات (4 أخطاء off-by-one وخطأ واحد في معالجة الأعداد الصحيحة غير الموقعة)

شرح الطريقة

تعريف المهمة

الإدخال: مصفوفة متفرقة COO - تحتوي على الأبعاد rows×cols و n ثلاثية إحداثيات (row_indk, col_indk, valk) الإخراج: مصفوفة متفرقة CSR - تحتوي على ثلاث مصفوفات أحادية البعد (val, col_ind, row_ptr) القيود: الحفاظ على التكافؤ الدلالي للمصفوفة الرياضية، المعالجة الصحيحة لجمع الفاصلة العائمة للإدخالات المكررة

الخوارزمية الأساسية

struct csr_matrix *coo_to_csr_matrix(struct coo_matrix *p) {
    // 1. ترتيب إدخالات COO حسب الترتيب المعجمي (صف، عمود)
    coo_quicksort(p, 0, n);
    
    // 2. عد عدد الأزواج الإحداثية غير المكررة
    k = coo_count(p);
    
    // 3. تخصيص مساحة مصفوفات CSR
    // 4. المرور عبر إدخالات COO المرتبة، بناء بنية CSR
    for (i=0; i<n; i++) {
        // معالجة الإدخالات المكررة والأعمدة الجديدة والصفوف الجديدة وما إلى ذلك
    }
}

معمارية المواصفات الرسمية

1. تعريف الكائنات الرياضية

Record coo_matrix (t: type) := {
    coo_rows: Z;
    coo_cols: Z;
    coo_entries: list (Z * Z * ftype t)
}.

Record csr_matrix {t: type} := {
    csr_cols: Z;
    csr_vals: list (ftype t);
    csr_col_ind: list Z;
    csr_row_ptr: list Z;
    csr_rows: Z := Zlength (csr_row_ptr) - 1
}.

2. علاقة التمثيل في الذاكرة

• coo_rep (sh: share) (coo: coo_matrix Tdouble) (p: val) : mpred
• csr_rep (sh: share) (csr: csr_matrix Tdouble) (p: val) : mpred

3. علاقة دلالة المصفوفة

Definition coo_to_matrix {t: type} (coo: coo_matrix t) (m: matrix t) : Prop :=
    coo_rows coo = matrix_rows m ∧
    matrix_cols m (coo_cols coo) ∧
    ∀ i j, sum_any (قائمة قيم الإدخالات المكررة) (matrix_index m i j).

نقاط الابتكار التقني

1. نمذجة عدم التحديد لجمع الفاصلة العائمة

Inductive sum_any {t}: list (ftype t) → ftype t → Prop :=
| Sum_Any_0: sum_any nil (Zconst t 0)
| Sum_Any_1: ∀ x, sum_any [x] x  
| Sum_Any_split: ∀ al bl a b, sum_any al a → sum_any bl b →
    sum_any (al++bl) (BPLUS a b)
| Sum_Any_perm: ∀ al bl s, Permutation al bl → sum_any al s → sum_any bl s.

2. تعريف علاقة CSR الجزئية

الابتكار الرئيسي هو علاقة partial_CSR i r coo ROWPTR COLIND VAL، التي تمثل حالة CSR الجزئية عند معالجة الإدخال i من COO والصف r.

3. الاستخلاص المنهجي لثوابت الحلقة

من خلال تحليل نقاط التحول الحالة الحرجة في البرنامج، يتم استخلاص خصائص الثوابت المطلوبة بشكل منهجي:

• partial_CSR_0: الحالة الأولية
• partial_CSR_duplicate: معالجة الإدخالات المكررة
• partial_CSR_newcol: إدخالات العمود الجديد
• partial_CSR_newrow: إدخالات الصف الجديد
• partial_CSR_skiprow: تخطي الصفوف الفارغة

إعداد التجارب

سلسلة أدوات التحقق

• مساعد إثبات Coq: للمواصفات الرسمية والإثبات
• مجموعة أدوات البرامج القابلة للتحقق (VST): للتحقق من برامج C باستخدام منطق Hoare
• C القابل للتحقق: منطق البرنامج في VST، مدمج في Coq

نطاق التحقق

• التعريفات والمبرهنات: 1571 سطر من كود Coq لتعريفات وخصائص coo_csr و partial_CSR
• إثبات VST: 412 سطر لإثبات منطق Hoare الرئيسي
• أساس الثقة: المواصفات الأساسية حوالي 39 سطراً، الأجزاء الرئيسية التي تتطلب فحصاً يدوياً

طريقة التحقق

1. التحقق الهرمي: إثبات أن برنامج C ينفذ المواصفات منخفضة المستوى أولاً، ثم إثبات الصحة الرياضية للمواصفات منخفضة المستوى
2. التصميم المعياري: فصل استدلال بنية البيانات عن استدلال التقريب بالفاصلة العائمة
3. الاستخلاص من الأسفل إلى الأعلى: استخلاص ثوابت الحلقة من احتياجات إثبات منطق Hoare للبرنامج

نتائج التجارب

الإنجازات الرئيسية

1. إثبات الصحة الكاملة: إثبات ناجح للصحة الكاملة لتحويل COO إلى CSR
2. اكتشاف الأخطاء: اكتشاف 5 أخطاء فعلية أثناء التحقق:
   • 4 أخطاء off-by-one
   • خطأ واحد معقد في معالجة تهيئة المتغير الصحيح غير الموقع r إلى -1
3. القابلية للتركيب: يمكن دمج الوحدة المتحقق منها مع عمليات مصفوفة متفرقة أخرى تم التحقق منها

نطاق التغطية التحقق

• مواصفات الدالة: شروط سابقة ولاحقة كاملة
• ثوابت الحلقة: ثوابت معقدة لثلاث حلقات متداخلة
• سلامة الذاكرة: حدود المصفوفة وسلامة تخصيص الذاكرة
• الصحة الرياضية: الحفاظ على دلالة المصفوفة

الخصائص الأداء

• التحقق في وقت الترجمة: بدون تكاليف وقت التشغيل
• درجة الموثوقية: إثبات تم التحقق منه بواسطة الآلة بناءً على نواة Coq
• قابلية الصيانة: التصميم المعياري للمواصفات يسهل التعديلات والتوسعات اللاحقة

الأعمال ذات الصلة

مجال التحقق الرسمي

1. التحقق من برامج العلوم: هذه الورقة حالة مهمة للتحقق من نهاية إلى نهاية للخوارزميات الرقمية
2. سلسلة أدوات VST: توسيع إطار عمل التحقق من برامج C الموجود، مع التطبيق على تطبيقات المصفوفات المتفرقة
3. التحقق من العمليات الحسابية بالفاصلة العائمة: الجمع بين أدوات مثل VCFloat2 لمعالجة تحليل دقة الفاصلة العائمة

خوارزميات المصفوفات المتفرقة

1. الخوارزميات الكلاسيكية: تحويل COO إلى CSR هو خوارزمية قياسية لعقود من الزمن
2. الجبر الخطي الرقمي: متسق مع الخوارزميات في الأدبيات الكلاسيكية مثل Templates for Linear Systems
3. الحوسبة عالية الأداء: توفير مكونات أساسية لبرامج العلوم الحسابية القابلة للتحقق

منهجيات التحقق من البرامج

1. استخلاص ثوابت الحلقة: الطريقة من الأسفل إلى الأعلى المقترحة لها عمومية
2. منطق الفصل: معالجة فعالة لبنى البيانات المعقدة في الذاكرة
3. هندسة المواصفات: عرض مبادئ تصميم المواصفات لمشاريع التحقق الكبيرة

الخلاصة والمناقشة

الاستنتاجات الرئيسية

1. إثبات الجدوى: التحقق الرسمي الكامل للخوارزميات الرقمية المعقدة ممكن
2. المساهمة المنهجية: طريقة استخلاص الثوابت من الأسفل إلى الأعلى لها تطبيقات واسعة
3. القيمة العملية: الأخطاء الفعلية المكتشفة أثناء التحقق تثبت قيمة الطرق الرسمية
4. البنية الأساسية: وضع أساس للتحقق من برامج العلوم الحسابية على نطاق أوسع

القيود

1. قابلية إعادة الإنتاج بدقة البت: المواصفات الحالية تسمح بترتيب جمع فاصلة عائمة مختلفة، ولا تضمن قابلية إعادة الإنتاج على مستوى البت
2. الاعتبارات الأداء: الخوارزمية المتحقق منها لم تتم تحسينها لتحسين الأداء
3. وظيفة إعادة التجميع: لم يتم تنفيذ نسخة محسنة تعيد استخدام بنية CSR
4. تكاليف التحقق: برنامج قصير نسبياً يتطلب كمية كبيرة من عمل التحقق

الاتجاهات المستقبلية

1. مواصفات أقوى: نسخة مواصفات تدعم قابلية إعادة الإنتاج بدقة البت
2. تحسين الأداء: التحقق من متغيرات خوارزميات المصفوفات المتفرقة عالية الأداء
3. أنظمة أكبر: دمج هذه الوحدة في التحقق من حل PDE كامل
4. الأتمتة: تطوير أدوات أفضل لدعم الاستخلاص التلقائي لثوابت الحلقة

التقييم المتعمق

المميزات

1. العمق التقني: معالجة عدة تحديات تقنية في خوارزميات المصفوفات المتفرقة، بما في ذلك العمليات الحسابية بالفاصلة العائمة وإدارة الذاكرة والتحكم في التدفق المعقد
2. الابتكار المنهجي: طريقة استخلاص الثوابت من الأسفل إلى الأعلى توفر نموذجاً قابلاً للتكرار للتحقق المماثل
3. القيمة العملية: اكتشاف الأخطاء الفعلية يثبت الفائدة العملية للتحقق الرسمي
4. جودة الهندسة: التصميم المعياري وبنية المواصفات الواضحة تعكس هندسة تحقق عالية الجودة
5. الاكتمال: التحقق من نهاية إلى نهاية من كود C إلى المواصفات الرياضية

أوجه القصور

1. تكاليف التحقق: 1983 سطر من كود التحقق لبرنامج C قصير نسبياً، التكاليف مرتفعة نسبياً
2. قيود العمومية: موجهة خصيصاً لتحويل COO إلى CSR، القدرة على التعميم محدودة
3. عدم كفاية الاعتبارات الأداء: عدم الأخذ في الاعتبار احتياجات تحسين الأداء في التطبيقات الفعلية
4. اعتماد الأدوات: اعتماد عالي على نظام بيئة VST و Coq

التأثير

1. المساهمة الأكاديمية: توفير دراسة حالة مهمة ومنهجية للتحقق من برامج العلوم
2. التأثير العملي: يمكن أن تكون بمثابة مكون أساسي لبرامج العلوم الحسابية عالية الموثوقية
3. نشر المنهجية: يمكن تطبيق طريقة استخلاص ثوابت الحلقة على التحقق من خوارزميات معقدة أخرى
4. تطوير الأدوات: تعزيز تطبيق أدوات التحقق مثل VST في مجال الحسابات الرقمية

السيناريوهات المناسبة

1. الحسابات العلمية الحرجة: محاكاة رقمية وتحليل يتطلب درجة عالية من الموثوقية
2. الأنظمة الحرجة من حيث السلامة: برامج حرجة من حيث السلامة تتضمن حسابات رقمية
3. أبحاث التحقق: دراسة مرجعية للتحقق الرسمي من الخوارزميات المعقدة
4. الأغراض التعليمية: عرض قدرات وطرق تقنيات التحقق من البرامج الحديثة

المراجع

تتضمن المراجع الرئيسية المستشهد بها في هذه الورقة:

1. Barrett et al. (1994): Templates for the Solution of Linear Systems - مرجع كلاسيكي لخوارزميات المصفوفات المتفرقة
2. Appel & Kellison (2024): VCFloat2 - أداة تحليل أخطاء الفاصلة العائمة
3. Cao et al. (2018): VST-Floyd - أداة التحقق بمنطق الفصل
4. Kellison et al. (2023): LAProof - مكتبة الإثبات الرسمي لبرامج الجبر الخطي

الملخص: تعرض هذه الورقة جدوى التحقق الرسمي الكامل للخوارزميات الرقمية المعقدة، وتقترح منهجية تحقق عملية، وتقدم مساهمات مهمة لتطوير برامج العلوم الحسابية الموثوقة. على الرغم من ارتفاع تكاليف التحقق، فإن قيمة اكتشاف الأخطاء الفعلية والتوجيهات المنهجية المقدمة تجعلها عملاً مهماً في هذا المجال.