2025-11-23T21:58:17.757337

Towards Richer Challenge Problems for Scientific Computing Correctness

Sottile, Tekriwal, Sarracino

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.

academic

科学計算の正確性に向けたより豊かなチャレンジ問題

基本情報

論文ID: 2510.13423
タイトル: Towards Richer Challenge Problems for Scientific Computing Correctness
著者: Matthew Sottile, Mohit Tekriwal, John Sarracino (Lawrence Livermore National Laboratory)
分類: cs.SE cs.MS
発表会議: International Workshop on Verification of Scientific Software (VSS 2025), EPTCS 432
論文リンク: https://arxiv.org/abs/2510.13423

要旨

科学計算(SC)の正確性問題は、形式化手法(FM)およびプログラミング言語(PL)コミュニティにおいて、ますます注目を集めています。既存のPL/FM検証技術は、現実的な科学計算アプリケーションの複雑性に対処する際に困難に直面しています。問題の一部は、SC社区とPL/FM社区の間で、機械検証可能な正確性チャレンジおよびSCアプリケーションにおける正確性の次元に関する共通の理解が欠けていることにあります。このギャップに対処するため、著者らは、FM/PL検証技術のSCにおける開発と評価を指導するための専門的なチャレンジ問題の確立を呼びかけています。これらの専門的なチャレンジは、FM/PL研究者が研究する既存の汎用プログラム問題を強化し、SCアプリケーションのニーズを満たすことができることを確保することを目的としています。

研究背景と動機

解決すべき問題

コミュニティ間の理解ギャップ：科学計算コミュニティと形式化手法/プログラミング言語コミュニティの間で、正確性チャレンジに関する共通の理解が欠けている
既存検証技術の限界：既存のPL/FM検証技術は、現実的な科学計算アプリケーションの複雑性に対処することが困難である
チャレンジ問題の不足：科学計算の正確性に特化した標準化されたチャレンジ問題セットが欠けている

問題の重要性

科学計算アプリケーションは、複雑な数値計算、並列処理、物理モデリングなど複数のレベルを含み、その正確性は科学研究結果の信頼性に直接影響します。従来のソフトウェア検証方法は、科学計算に固有の正確性要件を十分にカバーできないことが多いです。

既存手法の限界

既存の形式化検証チャレンジ問題は主に汎用プログラムを対象としており、科学計算に固有の複雑性が欠けている
数値検証コミュニティは関連する研究を行っていますが、統一されたチャレンジ問題セットが欠けている
既存のベンチマークスイートは主にパフォーマンスに焦点を当てており、正確性ではない

研究動機

高性能計算分野のパフォーマンスベンチマークスイート(NAS Parallel Benchmarks、Mantevaなど)の成功経験に倣い、科学計算の正確性のための同様のチャレンジ問題フレームワークを確立すること。

核心的貢献

科学計算の正確性の6つの次元を提案：数値計算、データ構造、領域モデリング構造、微分方程式、並行並列処理、近似スキーム
チャレンジ問題設計の重要な落とし穴を特定：過度な専門化、「玩具」問題、科学計算の独自性の無視など
チャレンジ問題とベンチマークテストの区別を確立：チャレンジ問題は目標と評価基準を定義し、ベンチマークテストは客観的な測定を提供する
設計指導原則を提供：不確実性の考慮、数学と実装の分離、未検証の仮定の許容など

方法論の詳細

タスク定義

本論文は立場論文(position paper)であり、科学計算の正確性のための包括的なチャレンジ問題フレームワークを確立することを目的としており、具体的な技術手法を提案するものではありません。

フレームワーク設計

正確性次元の分類

著者らは科学計算の正確性を3つの抽象レベルに分類しています：

低レベル：数値計算、従来のデータ構造
中レベル：モデル固有のデータ構造と計算
高レベル：数学的抽象化、物理システムの不変量

6つの核心的次元

数値計算(Numerics)
- 数学演算とハードウェア/ソフトウェア実装の正確な対応
- 浮動小数点演算の精度問題
- 混合精度アルゴリズムの課題
データ構造(Data Structures)
- 標準データ構造の正確性
- パフォーマンス最適化による構造変換(SOAからAOSへの変換など)
- セマンティック等価性の保証
領域モデリング構造(Domain-modeling Structures)
- メッシュ、グラフなどの複雑なデータ構造
- 物理システム制約の充足
- 保存則などの高レベルの不変量
微分方程式(Differential Equations)
- PDEと物理モデリングの一貫性
- 数値安定性、境界条件の互換性
- 適切性(well-posedness)
並行並列処理(Concurrency and Parallelism)
- 複数の並列プログラミングモデルの組み合わせ
- 共有メモリ、ベクトル化、分散メモリ並列処理
- パフォーマンスと正確性のバランス
近似スキーム(Approximation Schemes)
- アルゴリズムのヒューリスティック手法
- 補間方法
- 数値手法との区別

技術的革新点

多層抽象の統合：科学計算の正確性問題を低レベルの実装詳細から高レベルの物理制約まで、初めて体系的に統一フレームワーク化した
コミュニティ橋渡し機能：形式化手法コミュニティと科学計算コミュニティの共通言語を確立した
実用性志向：過度な理論化を避け、実際のアプリケーションにおける正確性要件に焦点を当てた

実験設定

本論文は立場論文として、従来の意味での実験設定を含まず、既存のベンチマークスイートとチャレンジ問題の分析を通じてその見解を支持しています。

分析対象

パフォーマンスベンチマーク：NAS Parallel Benchmarks、Mantevo、Salishan problems、Shonan challenge
正確性チャレンジ：VerifyThis、NSV-3 benchmarks、Gallery of Verified Programs
専門的ベンチマーク：FPbench、DataRaceBench、SPEC