Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)

基本信息

• 论文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中

验证规模

• 定义和引理: 1571行Coq代码用于coo_csr和partial_CSR的定义和性质
• VST证明: 412行用于主要的Hoare逻辑证明
• 信任基础: 核心规约约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. bit-for-bit可重现性: 当前规约允许不同的浮点求和顺序，不保证位级重现性
2. 性能考虑: 验证的算法未针对性能优化
3. 重组装功能: 未实现CSR结构重用的优化版本
4. 验证成本: 相对简短的程序需要大量的验证工作

未来方向

1. 更强规约: 支持bit-for-bit重现性的规约版本
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 - 线性代数程序的形式化证明库

总结: 这篇论文展示了复杂数值算法完全形式化验证的可行性，提出了实用的验证方法论，并为可信科学计算软件的发展做出了重要贡献。尽管验证成本较高，但其发现实际错误的价值和提供的方法论指导使其成为该领域的重要工作。