Correctness in scientific computing (SC) is gaining increasing attention in the formal methods (FM) and programming languages (PL) community. Existing PL/FM verification techniques struggle with the complexities of realistic SC applications. Part of the problem is a lack of a common understanding between the SC and PL/FM communities of machine-verifiable correctness challenges and dimensions of correctness in SC applications.
To address this gap, we call for specialized challenge problems to inform the development and evaluation of FM/PL verification techniques for correctness in SC. These specialized challenges are intended to augment existing problems studied by FM/PL researchers for general programs to ensure the needs of SC applications can be met. We propose several dimensions of correctness relevant to scientific computing, and discuss some guidelines and criteria for designing challenge problems to evaluate correctness in scientific computing.
- পেপার আইডি: 2510.13423
- শিরোনাম: বৈজ্ঞানিক কম্পিউটিং সঠিকতার জন্য আরও সমৃদ্ধ চ্যালেঞ্জ সমস্যার দিকে
- লেখক: ম্যাথিউ সোটিল, মোহিত টেক্রিওয়াল, জন সারাসিনো (লরেন্স লিভারমোর ন্যাশনাল ল্যাবরেটরি)
- শ্রেণীবিভাগ: cs.SE cs.MS
- প্রকাশিত সম্মেলন: আন্তর্জাতিক বৈজ্ঞানিক সফটওয়্যার যাচাইকরণ কর্মশালা (VSS 2025), EPTCS 432
- পেপার লিঙ্ক: https://arxiv.org/abs/2510.13423
বৈজ্ঞানিক কম্পিউটিং (SC) এর সঠিকতা সমস্যা আনুষ্ঠানিক পদ্ধতি (FM) এবং প্রোগ্রামিং ভাষা (PL) সম্প্রদায়ে ক্রমবর্ধমান মনোযোগ পাচ্ছে। বিদ্যমান PL/FM যাচাইকরণ কৌশলগুলি বাস্তব বৈজ্ঞানিক কম্পিউটিং অ্যাপ্লিকেশনের জটিলতা পরিচালনায় অসুবিধার সম্মুখীন হয়। সমস্যার একটি অংশ SC এবং PL/FM সম্প্রদায়ের মধ্যে যন্ত্র-যাচাইযোগ্য সঠিকতা চ্যালেঞ্জ এবং SC অ্যাপ্লিকেশনে সঠিকতার মাত্রা সম্পর্কে সাধারণ বোঝাপড়ার অভাব। এই ব্যবধান সমাধানের জন্য, লেখকরা FM/PL যাচাইকরণ কৌশলের উন্নয়ন এবং মূল্যায়নকে গাইড করার জন্য বিশেষায়িত চ্যালেঞ্জ সমস্যা প্রতিষ্ঠার আহ্বান জানান। এই বিশেষায়িত চ্যালেঞ্জগুলি FM/PL গবেষকদের দ্বারা অধ্যয়ন করা বিদ্যমান সাধারণ প্রোগ্রাম সমস্যাগুলি বৃদ্ধি করার জন্য ডিজাইন করা হয়েছে, যাতে SC অ্যাপ্লিকেশনের চাহিদা পূরণ করা যায়।
- সম্প্রদায়ের মধ্যে বোঝাপড়ার ব্যবধান: বৈজ্ঞানিক কম্পিউটিং সম্প্রদায় এবং আনুষ্ঠানিক পদ্ধতি/প্রোগ্রামিং ভাষা সম্প্রদায়ের মধ্যে সঠিকতা চ্যালেঞ্জ সম্পর্কে সাধারণ বোঝাপড়ার অভাব
- বিদ্যমান যাচাইকরণ কৌশলের সীমাবদ্ধতা: বিদ্যমান PL/FM যাচাইকরণ কৌশলগুলি বাস্তব বৈজ্ঞানিক কম্পিউটিং অ্যাপ্লিকেশনের জটিলতা পরিচালনা করতে অসুবিধা পায়
- চ্যালেঞ্জ সমস্যার অপর্যাপ্ততা: বৈজ্ঞানিক কম্পিউটিং সঠিকতার জন্য বিশেষভাবে মানসম্মত চ্যালেঞ্জ সমস্যার সেট অভাব
বৈজ্ঞানিক কম্পিউটিং অ্যাপ্লিকেশনগুলি জটিল সংখ্যাগত গণনা, সমান্তরাল প্রক্রিয়াকরণ, শারীরিক মডেলিং এবং অন্যান্য একাধিক স্তর জড়িত, যার সঠিকতা বৈজ্ঞানিক গবেষণা ফলাফলের নির্ভরযোগ্যতা সরাসরি প্রভাবিত করে। ঐতিহ্যবাহী সফটওয়্যার যাচাইকরণ পদ্ধতিগুলি প্রায়শই বৈজ্ঞানিক কম্পিউটিং-এর অনন্য সঠিকতা প্রয়োজনীয়তা পর্যাপ্তভাবে কভার করতে পারে না।
- বিদ্যমান আনুষ্ঠানিক যাচাইকরণ চ্যালেঞ্জ সমস্যাগুলি প্রধানত সাধারণ প্রোগ্রামের জন্য, বৈজ্ঞানিক কম্পিউটিং-এর অনন্য জটিলতার অভাব
- সংখ্যাগত যাচাইকরণ সম্প্রদায়ের সম্পর্কিত কাজ থাকলেও, একীভূত চ্যালেঞ্জ সমস্যার সেট অভাব
- বিদ্যমান বেঞ্চমার্ক স্যুটগুলি প্রধানত কর্মক্ষমতার উপর দৃষ্টি নিবদ্ধ করে, সঠিকতা নয়
উচ্চ-কর্মক্ষমতা কম্পিউটিং ক্ষেত্রে কর্মক্ষমতা বেঞ্চমার্ক স্যুটের সাফল্যের অভিজ্ঞতা থেকে শিখে (যেমন NAS সমান্তরাল বেঞ্চমার্ক, Mantevo ইত্যাদি), বৈজ্ঞানিক কম্পিউটিং সঠিকতার জন্য অনুরূপ চ্যালেঞ্জ সমস্যা কাঠামো প্রতিষ্ঠা করা।
- বৈজ্ঞানিক কম্পিউটিং সঠিকতার ছয়টি মাত্রা প্রস্তাব: সংখ্যাগত গণনা, ডেটা কাঠামো, ডোমেইন মডেলিং কাঠামো, অবকল সমীকরণ, সমসাময়িকতা এবং সমান্তরালতা, আনুমানিক স্কিম
- চ্যালেঞ্জ সমস্যা ডিজাইনের মূল ফাঁদগুলি চিহ্নিত করা: অত্যধিক বিশেষীকরণ, "খেলনা" সমস্যা, বৈজ্ঞানিক কম্পিউটিং অনন্যতা উপেক্ষা ইত্যাদি
- চ্যালেঞ্জ সমস্যা এবং বেঞ্চমার্ক পরীক্ষার মধ্যে পার্থক্য প্রতিষ্ঠা: চ্যালেঞ্জ সমস্যা লক্ষ্য এবং মূল্যায়ন মানদণ্ড সংজ্ঞায়িত করে, বেঞ্চমার্ক পরীক্ষা উদ্দেশ্যমূলক পরিমাপ প্রদান করে
- ডিজাইন নির্দেশিকা নীতি প্রদান: অনিশ্চয়তা বিবেচনা করা, গণিত এবং বাস্তবায়ন বিচ্ছিন্ন করা, অপরীক্ষিত অনুমান অনুমতি দেওয়া ইত্যাদি
এই পেপারটি একটি অবস্থান পত্র (position paper), যা বৈজ্ঞানিক কম্পিউটিং সঠিকতার জন্য একটি ব্যাপক চ্যালেঞ্জ সমস্যা কাঠামো প্রতিষ্ঠার লক্ষ্যে, নির্দিষ্ট প্রযুক্তিগত পদ্ধতি প্রস্তাব করে না।
লেখক বৈজ্ঞানিক কম্পিউটিং সঠিকতাকে তিনটি বিমূর্ত স্তরে বিভক্ত করেন:
- নিম্ন স্তর: সংখ্যাগত গণনা, ঐতিহ্যবাহী ডেটা কাঠামো
- মধ্য স্তর: মডেল-নির্দিষ্ট ডেটা কাঠামো এবং গণনা
- উচ্চ স্তর: গাণিতিক বিমূর্ততা, শারীরিক সিস্টেম অপরিবর্তনীয়
- সংখ্যাগত গণনা (Numerics)
- গাণিতিক ক্রিয়াকলাপ এবং হার্ডওয়্যার/সফটওয়্যার বাস্তবায়নের মধ্যে সঠিক সামঞ্জস্য
- ফ্লোটিং-পয়েন্ট গণনার নির্ভুলতা সমস্যা
- মিশ্র-নির্ভুলতা অ্যালগরিদমের চ্যালেঞ্জ
- ডেটা কাঠামো (Data Structures)
- মান ডেটা কাঠামোর সঠিকতা
- কর্মক্ষমতা অপ্টিমাইজেশন দ্বারা সৃষ্ট কাঠামো রূপান্তর (যেমন SOA থেকে AOS রূপান্তর)
- শব্দার্থগত সমতা নিশ্চিতকরণ
- ডোমেইন-মডেলিং কাঠামো (Domain-modeling Structures)
- জাল, গ্রাফ ইত্যাদি জটিল ডেটা কাঠামো
- শারীরিক সিস্টেম সীমাবদ্ধতার সন্তুষ্টি
- সংরক্ষণ আইন ইত্যাদি উচ্চ-স্তরের অপরিবর্তনীয়
- অবকল সমীকরণ (Differential Equations)
- PDE এবং শারীরিক মডেলিং এর সামঞ্জস্য
- সংখ্যাগত স্থিতিশীলতা, সীমানা শর্ত সামঞ্জস্য
- সুনির্ধারিততা (well-posedness)
- সমসাময়িকতা এবং সমান্তরালতা (Concurrency and Parallelism)
- একাধিক সমান্তরাল প্রোগ্রামিং মডেলের সমন্বয়
- ভাগ করা মেমরি, ভেক্টরাইজেশন, বিতরণকৃত মেমরি সমান্তরালতা
- কর্মক্ষমতা এবং সঠিকতার ভারসাম্য
- আনুমানিক স্কিম (Approximation Schemes)
- অ্যালগরিদম হিউরিস্টিক পদ্ধতি
- ইন্টারপোলেশন পদ্ধতি
- সংখ্যাগত পদ্ধতির সাথে পার্থক্য
- বহু-স্তরীয় বিমূর্ততা একীকরণ: প্রথমবারের মতো বৈজ্ঞানিক কম্পিউটিং সঠিকতা সমস্যাগুলিকে নিম্ন-স্তরের বাস্তবায়ন বিবরণ থেকে উচ্চ-স্তরের শারীরিক সীমাবদ্ধতা পর্যন্ত সিস্টেমেটিকভাবে একীভূত কাঠামোতে রূপান্তরিত করা
- সম্প্রদায় সেতু ভূমিকা: আনুষ্ঠানিক পদ্ধতি সম্প্রদায় এবং বৈজ্ঞানিক কম্পিউটিং সম্প্রদায়ের মধ্যে সাধারণ ভাষা প্রতিষ্ঠা করা
- ব্যবহারিক-কেন্দ্রিক অভিমুখ: অত্যধিক তাত্ত্বিকীকরণ এড়ানো, বাস্তব অ্যাপ্লিকেশনে সঠিকতার চাহিদার উপর দৃষ্টি নিবদ্ধ করা
এই পেপারটি একটি অবস্থান পত্র হিসাবে, ঐতিহ্যবাহী অর্থে পরীক্ষামূলক সেটআপ অন্তর্ভুক্ত করে না, বরং বিদ্যমান বেঞ্চমার্ক স্যুট এবং চ্যালেঞ্জ সমস্যাগুলি বিশ্লেষণ করে তার দৃষ্টিভঙ্গি সমর্থন করে।
- কর্মক্ষমতা বেঞ্চমার্ক পরীক্ষা: NAS সমান্তরাল বেঞ্চমার্ক, Mantevo, Salishan সমস্যা, Shonan চ্যালেঞ্জ
- সঠিকতা চ্যালেঞ্জ: VerifyThis, NSV-3 বেঞ্চমার্ক, যাচাইকৃত প্রোগ্রামের গ্যালারি
- বিশেষায়িত বেঞ্চমার্ক: FPbench, DataRaceBench, SPEC
লেখক চ্যালেঞ্জ সমস্যাগুলির যা বৈশিষ্ট্য থাকা উচিত তা প্রস্তাব করেন:
- একাধিক সঠিকতা মাত্রা কভার করা
- অত্যধিক বিশেষীকরণ এড়ানো
- বাস্তব প্রাসঙ্গিকতা রাখা
- বৈজ্ঞানিক কম্পিউটিং অনন্য চাহিদার উপর দৃষ্টি নিবদ্ধ করা
লেখক বিশ্লেষণ করে দেখেন যে বিদ্যমান চ্যালেঞ্জ সমস্যাগুলি নিম্নলিখিত অপর্যাপ্ততা রয়েছে:
- কভারেজ অপর্যাপ্ততা: গ্রাফ অ্যালগরিদম, বিরল ম্যাট্রিক্স প্রতিনিধিত্ব ইত্যাদি জটিল অ্যালগরিদম বিভাগের অভাব
- সহজ ডেটা কাঠামো: মৌলিক CSR এর বাইরে জটিল বিরল ম্যাট্রিক্স প্রতিনিধিত্ব কভারেজ অপর্যাপ্ত
- গাণিতিক ক্ষেত্র অসম্পূর্ণ: মৌলিক গাণিতিক ক্ষেত্র কভারেজ অপর্যাপ্ত
কর্মক্ষমতা বেঞ্চমার্ক পরীক্ষার বিবর্তন প্রক্রিয়া:
- Linpack → Livermore Loops → NAS সমান্তরাল বেঞ্চমার্ক → Mantevo
- জটিলতা ক্রমান্বয়ে বৃদ্ধি, সহজ রৈখিক বীজগণিত থেকে সম্পূর্ণ অ্যাপ্লিকেশন কোড পর্যন্ত
- মূল্যায়ন মেট্রিক্স একক কর্মক্ষমতা থেকে সঠিকতা এবং স্কেলেবিলিটি পর্যন্ত প্রসারিত
- প্রাথমিক বেঞ্চমার্ক: Linpack ফ্লোটিং-পয়েন্ট অপারেশন কর্মক্ষমতায় ফোকাস করে
- লুপ কার্নেল: Livermore Loops নির্দিষ্ট গণনা প্যাটার্ন পরীক্ষা করে
- সমান্তরাল বেঞ্চমার্ক: NAS সমান্তরাল বেঞ্চমার্ক সমান্তরালতা বিবেচনা প্রবর্তন করে
- অ্যাপ্লিকেশন-ভিত্তিক: Mantevo প্রকৃত অ্যাপ্লিকেশনের কাছাকাছি মিনি-অ্যাপ্লিকেশন প্রদান করে
- সাধারণ যাচাইকরণ: VerifyThis ইত্যাদি প্রতিযোগিতা মৌলিক চ্যালেঞ্জ প্রদান করে
- সংখ্যাগত যাচাইকরণ: coq-num-analysis, গাণিতিক উপাদান লাইব্রেরি
- বিশেষায়িত ক্ষেত্র: FPbench (ফ্লোটিং-পয়েন্ট), DataRaceBench (ডেটা প্রতিযোগিতা)
- ASME V&V নির্দেশিকা নীতি প্রকৌশল শৃঙ্খলার জন্য যাচাইকরণ বৈধতা মান প্রদান করে
- যাচাইকরণ (verification) এবং বৈধতা (validation) সমস্যা মধ্যে পার্থক্য
- বৈজ্ঞানিক কম্পিউটিং সঠিকতার জন্য আনুষ্ঠানিক পদ্ধতি উন্নয়ন চালিত করার জন্য বিশেষায়িত চ্যালেঞ্জ সমস্যা প্রয়োজন
- চ্যালেঞ্জ সমস্যাগুলি গণনা বিমূর্ততা স্তর জুড়ে থাকতে হবে, নিম্ন-স্তরের বাস্তবায়ন এবং উচ্চ-স্তরের ডোমেইন সীমাবদ্ধতা একীভূত করতে হবে
- অত্যধিক বিশেষীকরণ এবং "খেলনা" সমস্যা এড়াতে হবে, বাস্তব অ্যাপ্লিকেশন প্রাসঙ্গিকতার উপর দৃষ্টি নিবদ্ধ করতে হবে
- তাত্ত্বিক প্রকৃতি: একটি অবস্থান পত্র হিসাবে, নির্দিষ্ট চ্যালেঞ্জ সমস্যা উদাহরণের অভাব
- বাস্তবায়ন জটিলতা: ব্যাপক চ্যালেঞ্জ সমস্যা সেট প্রতিষ্ঠা করতে আন্তঃশৃঙ্খলা সহযোগিতা প্রয়োজন
- মূল্যায়ন মানদণ্ড: চ্যালেঞ্জ সমস্যার গুণমান উদ্দেশ্যমূলকভাবে মূল্যায়ন কীভাবে করতে হয় তা এখনও আরও গবেষণা প্রয়োজন
- বৈজ্ঞানিক কম্পিউটিং এবং আনুষ্ঠানিক পদ্ধতি বিশেষজ্ঞদের সাথে সহযোগিতা করে নির্দিষ্ট চ্যালেঞ্জ সমস্যা ডিজাইন করা
- মানসম্মত মূল্যায়ন কাঠামো এবং পরিমাপ মানদণ্ড প্রতিষ্ঠা করা
- অনিশ্চয়তা পরিমাণকরণ এবং পরিসংখ্যানগত মডেলিং একীকরণ বিবেচনা করা
- যাচাইকরণ বৈধতা (V&V) সমস্যায় প্রসারিত করা
- সমস্যা চিহ্নিতকরণ নির্ভুল: বৈজ্ঞানিক কম্পিউটিং সঠিকতা যাচাইকরণের মূল চ্যালেঞ্জগুলি নির্ভুলভাবে চিহ্নিত করা
- কাঠামো সিস্টেমেটিকতা: প্রস্তাবিত সঠিকতা মাত্রা কাঠামো ভাল সিস্টেমেটিকতা এবং সম্পূর্ণতা রয়েছে
- ব্যবহারিক-কেন্দ্রিক অভিমুখ: বিশুদ্ধ তাত্ত্বিক আলোচনা এড়ানো, বাস্তব অ্যাপ্লিকেশন চাহিদার উপর দৃষ্টি নিবদ্ধ করা
- আন্তঃশৃঙ্খলা দৃষ্টিভঙ্গি: আনুষ্ঠানিক পদ্ধতি এবং বৈজ্ঞানিক কম্পিউটিং দুটি সম্প্রদায়কে কার্যকরভাবে সংযুক্ত করা
- ঐতিহাসিক ধার: কর্মক্ষমতা বেঞ্চমার্ক পরীক্ষা উন্নয়ন প্রক্রিয়া থেকে মূল্যবান অভিজ্ঞতা সংগ্রহ করা
- নির্দিষ্ট উদাহরণের অভাব: কাঠামোর সম্ভাব্যতা যাচাই করার জন্য নির্দিষ্ট চ্যালেঞ্জ সমস্যা উদাহরণ প্রদান করা হয়নি
- বাস্তবায়ন পথ অস্পষ্ট: তাত্ত্বিক কাঠামো থেকে বাস্তব চ্যালেঞ্জ সমস্যা সেটে কীভাবে রূপান্তরিত করতে হয় তা বিস্তারিত পরিকল্পনার অভাব
- মূল্যায়ন প্রক্রিয়া অনুপস্থিত: চ্যালেঞ্জ সমস্যার গুণমান এবং কার্যকারিতা মূল্যায়নের নির্দিষ্ট প্রক্রিয়া অভাব
- সম্প্রদায় গ্রহণযোগ্যতা অজানা: দুটি সম্প্রদায়ের এই কাঠামোর প্রতি গ্রহণযোগ্যতা এবং অংশগ্রহণের ইচ্ছা অজানা
- একাডেমিক মূল্য: বৈজ্ঞানিক কম্পিউটিং সঠিকতা গবেষণার জন্য গুরুত্বপূর্ণ তাত্ত্বিক কাঠামো প্রদান করা
- ব্যবহারিক সম্ভাবনা: আরও ব্যবহারিক আনুষ্ঠানিক যাচাইকরণ প্রযুক্তি উন্নয়ন চালিত করার সম্ভাবনা
- সম্প্রদায় নির্মাণ: বৈজ্ঞানিক কম্পিউটিং এবং আনুষ্ঠানিক পদ্ধতি সম্প্রদায়ের গভীর সহযোগিতা প্রচার করতে পারে
- দীর্ঘমেয়াদী তাৎপর্য: বৈজ্ঞানিক কম্পিউটিং সফটওয়্যার গুণমান নিশ্চিতকরণের জন্য নতুন গবেষণা দিকনির্দেশনা প্রদান করা
- গবেষণা নির্দেশনা: আনুষ্ঠানিক পদ্ধতি গবেষকদের বৈজ্ঞানিক কম্পিউটিং অ্যাপ্লিকেশনের গবেষণা দিকনির্দেশনা প্রদান করা
- সরঞ্জাম উন্নয়ন: বৈজ্ঞানিক কম্পিউটিং যাচাইকরণ সরঞ্জাম ডিজাইন এবং মূল্যায়ন নির্দেশনা দেওয়া
- শিক্ষা প্রশিক্ষণ: বৈজ্ঞানিক কম্পিউটিং সঠিকতা শিক্ষার জন্য সিস্টেমেটিক কাঠামো প্রদান করা
- মান নির্ধারণ: বৈজ্ঞানিক কম্পিউটিং সফটওয়্যার গুণমান মান নির্ধারণের জন্য রেফারেন্স প্রদান করা
পেপারটি 26টি গুরুত্বপূর্ণ তথ্যসূত্র উদ্ধৃত করে, যা অন্তর্ভুক্ত করে:
- কর্মক্ষমতা বেঞ্চমার্ক পরীক্ষা: NAS সমান্তরাল বেঞ্চমার্ক 7,8, Mantevo 11, Linpack 14
- আনুষ্ঠানিক যাচাইকরণ: যাচাইকৃত প্রোগ্রামের গ্যালারি 1,17, VerifyThis 20
- সংখ্যাগত যাচাইকরণ: coq-num-analysis 6, গাণিতিক উপাদান 2
- বিশেষায়িত বেঞ্চমার্ক: FPbench 12, DataRaceBench 21, SPEC 13
- V&V মান: ASME নির্দেশিকা নীতি 18
যদিও এই পেপারটি একটি অবস্থান পত্র, তবে এটি বৈজ্ঞানিক কম্পিউটিং সঠিকতা যাচাইকরণ ক্ষেত্রের জন্য গুরুত্বপূর্ণ তাত্ত্বিক কাঠামো এবং উন্নয়ন দিকনির্দেশনা প্রদান করে। এর প্রস্তাবিত ছয়-মাত্রা সঠিকতা কাঠামো এবং ডিজাইন নির্দেশিকা নীতি ক্ষেত্রের উন্নয়ন চালিত করার জন্য গুরুত্বপূর্ণ, তবে এই ধারণাগুলি নির্দিষ্টভাবে বাস্তবায়ন এবং যাচাই করার জন্য পরবর্তী কাজ প্রয়োজন।