COO से CSR विरल आव्यूह रूपांतरण का औपचारिक सत्यापन (आमंत्रित पत्र)

मूल जानकारी

• पत्र ID: 2510.13412
• शीर्षक: Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)
• लेखक: Andrew W. Appel (Princeton University)
• वर्गीकरण: math.NA cs.LO cs.NA
• प्रकाशन समय/सम्मेलन: VSS 2025 (International Workshop on Verification of Scientific Software), EPTCS 432, 2025
• पत्र लिंक: https://arxiv.org/abs/2510.13412

सारांश

यह पत्र निर्देशांक रूप (COO) विरल आव्यूह को संपीड़ित विरल पंक्ति (CSR) आव्यूह में परिवर्तित करने वाले C प्रोग्राम के सत्यापन के लिए एक मशीन-जाँचा गया सही प्रमाण प्रस्तुत करता है। शास्त्रीय एल्गोरिदम (COO प्रविष्टियों को पंक्ति, स्तंभ के शब्दकोश क्रम में क्रमबद्ध करना; बाएं से दाएं CSR सरणियों को भरना) संक्षिप्त होने के बावजूद, काफी जटिल अपरिवर्तनीयों को प्रदर्शित करता है। लेख प्रोग्राम से अपरिवर्तनीयों को प्राप्त करने के लिए एक नीचे-ऊपर की कार्यप्रणाली प्रदर्शित करता है।

अनुसंधान पृष्ठभूमि और प्रेरणा

समस्या परिभाषा

1. मूल समस्या: विरल आव्यूह संख्यात्मक गणना में व्यापक रूप से उपयोग किए जाते हैं, लेकिन मौजूदा विरल आव्यूह रूपांतरण एल्गोरिदम में औपचारिक सत्यापन की कमी है, जिससे कठिन-से-खोजे जाने वाले त्रुटियां हो सकती हैं
2. महत्व: विरल आव्यूह-सदिश गुणन संख्यात्मक विधियों में एक मौलिक संचालन है, गलत रूपांतरण पूरी गणना श्रृंखला की विफलता का कारण बन सकता है
3. मौजूदा सीमाएं: पारंपरिक सत्यापन विधियां प्रतिगमन परीक्षण आदि पर निर्भर करती हैं, गणितीय सही प्रमाण प्रदान नहीं कर सकते
4. अनुसंधान प्रेरणा: मशीन-जाँचे गए औपचारिक प्रमाण के माध्यम से, COO से CSR रूपांतरण की पूर्ण सही प्रमाण सुनिश्चित करना, सत्यापन योग्य संख्यात्मक सॉफ्टवेयर के लिए आधार स्थापित करना

अनुप्रयोग पृष्ठभूमि

• विरल आव्यूह प्रतिनिधित्व: COO प्रारूप निर्माण के लिए सुविधाजनक है, CSR प्रारूप गुणन संचालन के लिए सुविधाजनक है
• परिमित तत्व विश्लेषण: जाल में प्रत्येक आंतरिक शीर्ष कई निर्देशांक टुपल्स उत्पन्न करता है, स्वाभाविक रूप से डुप्लिकेट प्रविष्टियां उत्पन्न करता है
• संख्यात्मक सटीकता: फ्लोटिंग-पॉइंट संचालन की गैर-सहयोगिता डुप्लिकेट प्रविष्टियों के योग क्रम को परिणाम को प्रभावित करती है

मुख्य योगदान

1. पहली बार मशीन-जाँचा गया COO से CSR रूपांतरण सही प्रमाण: Verifiable Software Toolchain (VST) और Coq प्रमाण सहायक का उपयोग करना
2. लूप अपरिवर्तनीय व्युत्पत्ति की नवीन विधि: नीचे-ऊपर की कार्यप्रणाली प्रस्तावित करना, प्रोग्राम को संतुष्ट करने वाले गुणों से जटिल लूप अपरिवर्तनीयों को प्राप्त करना
3. डेटा संरचना और सन्निकटन तर्क का पृथक्करण: C प्रोग्राम के डेटा संरचना तर्क को फ्लोटिंग-पॉइंट सन्निकटन तर्क से अलग करना, सत्यापन जटिलता को सरल बनाना
4. संयोजनीय सत्यापन घटक: बड़े सत्यापन प्रणालियों में पुनः उपयोग के लिए सत्यापित विरल आव्यूह रूपांतरण मॉड्यूल प्रदान करना
5. व्यावहारिक त्रुटि खोज: प्रमाण प्रक्रिया में 5 प्रोग्राम त्रुटियां खोजना और ठीक करना (4 off-by-one त्रुटियां और 1 अहस्ताक्षरित पूर्णांक हैंडलिंग त्रुटि)

विधि विवरण

कार्य परिभाषा

इनपुट: 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 संबंध है, जो i-वीं COO प्रविष्टि, r-वीं पंक्ति को संसाधित करते समय आंशिक CSR स्थिति का प्रतिनिधित्व करता है।

3. लूप अपरिवर्तनीय की व्यवस्थित व्युत्पत्ति

प्रोग्राम में महत्वपूर्ण स्थिति संक्रमण बिंदुओं का विश्लेषण करके, आवश्यक अपरिवर्तनीय गुणों को व्यवस्थित रूप से प्राप्त करना:

• partial_CSR_0: प्रारंभिक स्थिति
• partial_CSR_duplicate: डुप्लिकेट प्रविष्टियों को संभालना
• partial_CSR_newcol: नई स्तंभ प्रविष्टि
• partial_CSR_newrow: नई पंक्ति प्रविष्टि
• partial_CSR_skiprow: खाली पंक्तियों को छोड़ना

प्रायोगिक सेटअप

सत्यापन उपकरण श्रृंखला

• Coq प्रमाण सहायक: औपचारिक विनिर्देश और प्रमाण के लिए
• Verifiable Software Toolchain (VST): C प्रोग्राम के Hoare तर्क सत्यापन के लिए
• Verifiable C: VST में प्रोग्राम तर्क, Coq में एम्बेड किया गया

सत्यापन पैमाना

• परिभाषाएं और लेम्मा: coo_csr और partial_CSR की परिभाषा और गुणों के लिए 1571 पंक्तियां Coq कोड
• VST प्रमाण: मुख्य Hoare तर्क प्रमाण के लिए 412 पंक्तियां
• विश्वास आधार: मूल विनिर्देश लगभग 39 पंक्तियां, मानव जांच की आवश्यकता वाले महत्वपूर्ण भाग

सत्यापन विधि

1. स्तरीय सत्यापन: पहले C प्रोग्राम को निम्न-स्तरीय विनिर्देश को लागू करने के लिए सिद्ध करें, फिर निम्न-स्तरीय विनिर्देश की गणितीय सही प्रमाण करें
2. मॉड्यूलर डिजाइन: डेटा संरचना तर्क को फ्लोटिंग-पॉइंट सन्निकटन तर्क से अलग करना
3. नीचे-ऊपर व्युत्पत्ति: प्रोग्राम के Hoare तर्क प्रमाण आवश्यकताओं से लूप अपरिवर्तनीयों को विपरीत रूप से प्राप्त करना

प्रायोगिक परिणाम

मुख्य उपलब्धियां

1. संपूर्ण सही प्रमाण: COO से CSR रूपांतरण की पूर्ण सही प्रमाण में सफलतापूर्वक सिद्ध किया
2. त्रुटि खोज: सत्यापन प्रक्रिया में 5 व्यावहारिक त्रुटियां खोजी गईं:
   • 4 off-by-one त्रुटियां
   • 1 अहस्ताक्षरित पूर्णांक 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 - रैखिक बीजगणित प्रोग्राम के औपचारिक प्रमाण पुस्तकालय

सारांश: यह पत्र जटिल संख्यात्मक एल्गोरिदम के पूर्ण औपचारिक सत्यापन की व्यवहार्यता को प्रदर्शित करता है, व्यावहारिक सत्यापन कार्यप्रणाली प्रस्तावित करता है, और विश्वसनीय वैज्ञानिक कंप्यूटिंग सॉफ्टवेयर के विकास में महत्वपूर्ण योगदान देता है। यद्यपि सत्यापन लागत अधिक है, व्यावहारिक त्रुटियों की खोज का मूल्य और प्रदान की गई कार्यप्रणाली मार्गदर्शन इसे इस क्षेत्र का एक महत्वपूर्ण कार्य बनाता है।