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

Towards Richer Challenge Problems for Scientific Computing Correctness

基本信息

  • 论文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应用的需求。

研究背景与动机

要解决的问题

  1. 社区间理解差距：科学计算社区和形式化方法/编程语言社区之间缺乏对正确性挑战的共同理解
  2. 现有验证技术局限性：现有的PL/FM验证技术难以处理现实科学计算应用的复杂性
  3. 挑战问题不足：缺乏专门针对科学计算正确性的标准化挑战问题集

问题重要性

科学计算应用涉及复杂的数值计算、并行处理、物理建模等多个层面，其正确性直接影响科学研究结果的可靠性。传统的软件验证方法往往无法充分覆盖科学计算特有的正确性需求。

现有方法局限性

  • 现有的形式化验证挑战问题主要针对通用程序，缺乏科学计算特有的复杂性
  • 数值验证社区虽然有相关工作，但缺乏统一的挑战问题集
  • 现有基准测试套件主要关注性能而非正确性

研究动机

借鉴高性能计算领域性能基准测试套件(如NAS Parallel Benchmarks、Mantevo等)的成功经验，为科学计算正确性建立类似的挑战问题框架。

核心贡献

  1. 提出科学计算正确性的六个维度：数值计算、数据结构、领域建模结构、微分方程、并发并行、近似方案
  2. 识别挑战问题设计的关键陷阱：过度专业化、"玩具"问题、忽视科学计算独特性等
  3. 建立挑战问题与基准测试的区别：挑战问题定义目标和评估标准，基准测试提供客观度量
  4. 提供设计指导原则：考虑不确定性、分离数学与实现、允许未检查假设等

方法详解

任务定义

本文是一篇立场论文(position paper)，旨在为科学计算正确性建立一套综合性的挑战问题框架，而非提出具体的技术方法。

框架设计

正确性维度分类

作者将科学计算正确性分为三个抽象层次：

  • 低级层面：数值计算、传统数据结构
  • 中级层面：模型特定的数据结构和计算
  • 高级层面：数学抽象、物理系统不变量

六个核心维度

  1. 数值计算(Numerics)
    • 数学运算与硬件/软件实现的正确对应
    • 浮点运算的精度问题
    • 混合精度算法的挑战
  2. 数据结构(Data Structures)
    • 标准数据结构的正确性
    • 性能优化导致的结构变换(如SOA到AOS转换)
    • 语义等价性保证
  3. 领域建模结构(Domain-modeling Structures)
    • 网格、图等复杂数据结构
    • 物理系统约束的满足
    • 守恒定律等高级不变量
  4. 微分方程(Differential Equations)
    • PDE与物理建模的一致性
    • 数值稳定性、边界条件兼容性
    • 适定性(well-posedness)
  5. 并发并行(Concurrency and Parallelism)
    • 多种并行编程模型的组合
    • 共享内存、向量化、分布式内存并行
    • 性能与正确性的平衡
  6. 近似方案(Approximation Schemes)
    • 算法启发式方法
    • 插值方法
    • 与数值方法的区别

技术创新点

  1. 多层次抽象整合：首次系统性地将科学计算正确性问题从低级实现细节到高级物理约束进行统一框架化
  2. 社区桥梁作用：为形式化方法社区和科学计算社区建立共同语言
  3. 实用性导向：避免过度理论化，关注实际应用中的正确性需求

实验设置

本文作为立场论文，不包含传统意义上的实验设置，而是通过分析现有基准测试套件和挑战问题来支持其观点。

分析对象

  • 性能基准测试：NAS Parallel Benchmarks、Mantevo、Salishan problems、Shonan challenge
  • 正确性挑战：VerifyThis、NSV-3 benchmarks、Gallery of Verified Programs
  • 专门基准：FPbench、DataRaceBench、SPEC

评价标准

作者提出挑战问题应该具备的特征：

  • 覆盖多个正确性维度
  • 避免过度专业化
  • 具有现实相关性
  • 关注科学计算独特需求

实验结果

现状分析

作者分析发现现有挑战问题存在以下不足：

  1. 覆盖面不足：缺乏图算法、稀疏矩阵表示等复杂算法类别
  2. 数据结构简单：基本CSR之外的复杂稀疏矩阵表示覆盖不足
  3. 数学领域不全：基础数学领域覆盖不充分

成功案例借鉴

性能基准测试的演进历程：

  • Linpack → Livermore Loops → NAS Parallel Benchmarks → Mantevo
  • 复杂性逐步增加，从简单线性代数到完整应用代码
  • 评价指标从单纯性能扩展到正确性和可扩展性

相关工作

性能基准测试发展

  • 早期基准：Linpack专注浮点运算性能
  • 循环内核：Livermore Loops测试特定计算模式
  • 并行基准：NAS Parallel Benchmarks引入并行性考量
  • 应用导向：Mantevo提供接近真实应用的mini-apps

正确性验证挑战

  • 通用验证：VerifyThis等竞赛提供基础挑战
  • 数值验证：coq-num-analysis、Mathematical Components Library
  • 专门领域：FPbench(浮点)、DataRaceBench(数据竞争)

验证与确认(V&V)

  • ASME V&V指导原则为工程学科提供验证确认标准
  • 区分验证(verification)和确认(validation)问题

结论与讨论

主要结论

  1. 科学计算正确性需要专门的挑战问题来推动形式化方法发展
  2. 挑战问题必须跨越计算机抽象层次，整合低级实现和高级领域约束
  3. 需要避免过度专业化和"玩具"问题，关注现实应用相关性

局限性

  1. 理论性质：作为立场论文，缺乏具体的挑战问题实例
  2. 实施复杂性：建立综合性挑战问题集需要跨学科合作
  3. 评价标准：如何客观评估挑战问题的质量仍需进一步研究

未来方向

  1. 与科学计算和形式化方法专家合作设计具体挑战问题
  2. 建立标准化的评价框架和度量标准
  3. 考虑不确定性量化和统计建模的整合
  4. 扩展到验证确认(V&V)问题

深度评价

优点

  1. 问题识别准确：准确识别了科学计算正确性验证的关键挑战
  2. 框架系统性：提出的正确性维度框架具有很好的系统性和完整性
  3. 实用导向：避免纯理论讨论，关注实际应用需求
  4. 跨学科视角：有效连接了形式化方法和科学计算两个社区
  5. 历史借鉴：从性能基准测试发展历程中汲取有价值的经验

不足

  1. 缺乏具体实例：没有提供具体的挑战问题示例来验证框架的可行性
  2. 实施路径不明：如何从理论框架转向实际的挑战问题集缺乏详细规划
  3. 评价机制缺失：缺乏评估挑战问题质量和有效性的具体机制
  4. 社区接受度未知：两个社区对此框架的接受程度和参与意愿未知

影响力

  1. 学术价值：为科学计算正确性研究提供了重要的理论框架
  2. 实用潜力：有望推动更实用的形式化验证技术发展
  3. 社区建设：可能促进科学计算和形式化方法社区的深度合作
  4. 长远意义：为科学计算软件质量保证提供新的研究方向

适用场景

  1. 研究指导：为形式化方法研究人员提供科学计算应用的研究方向
  2. 工具开发：指导科学计算验证工具的设计和评估
  3. 教育培训：为科学计算正确性教育提供系统性框架
  4. 标准制定：为科学计算软件质量标准制定提供参考

参考文献

论文引用了26篇重要文献，涵盖：

  • 性能基准测试：NAS Parallel Benchmarks 7,8, Mantevo 11, Linpack 14
  • 形式化验证：Gallery of Verified Programs 1,17, VerifyThis 20
  • 数值验证：coq-num-analysis 6, Mathematical Components 2
  • 专门基准：FPbench 12, DataRaceBench 21, SPEC 13
  • V&V标准：ASME指导原则 18

这篇论文虽然是立场论文，但为科学计算正确性验证领域提供了重要的理论框架和发展方向。其提出的六维度正确性框架和设计指导原则对于推动该领域的发展具有重要意义，但需要后续工作来具体实施和验证这些理念。