Формальная верификация преобразования разреженных матриц из формата COO в CSR (Приглашённая статья)

Основная информация

• ID статьи: 2510.13412
• Название: Formal Verification of COO to CSR Sparse Matrix Conversion (Invited Paper)
• Автор: Andrew W. Appel (Принстонский университет)
• Классификация: math.NA cs.LO cs.NA
• Время публикации/конференция: VSS 2025 (Международный семинар по верификации научного программного обеспечения), EPTCS 432, 2025
• Ссылка на статью: https://arxiv.org/abs/2510.13412

Аннотация

В данной статье описывается машинно-проверяемое доказательство корректности для верификации программы на языке C, которая преобразует разреженные матрицы из координатного формата (COO) в формат сжатых разреженных строк (CSR). Классический алгоритм (сортировка записей 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, представляющее частичное состояние CSR при обработке i-й записи COO и r-й строки.

3. Систематическое выведение инвариантов цикла

Путём анализа ключевых точек переходов состояния в программе систематически выводятся требуемые свойства инвариантов:

• partial_CSR_0: начальное состояние
• partial_CSR_duplicate: обработка повторяющихся записей
• partial_CSR_newcol: новая запись столбца
• partial_CSR_newrow: новая запись строки
• partial_CSR_skiprow: пропуск пустых строк

Экспериментальная установка

Инструментарий верификации

• Помощник по доказательствам Coq: Используется для формальной спецификации и доказательств
• Verifiable Software Toolchain (VST): Используется для верификации программ на C с использованием логики Хоара
• Verifiable C: Логика программ в VST, встроенная в Coq

Масштаб верификации

• Определения и леммы: 1571 строка кода Coq для определений и свойств coo_csr и partial_CSR
• Доказательство VST: 412 строк для основного доказательства логики Хоара
• Основание доверия: Основная спецификация составляет примерно 39 строк, требующих ручной проверки ключевых частей

Методология верификации

1. Многоуровневая верификация: Сначала доказывается, что программа на C реализует низкоуровневую спецификацию, затем доказывается математическая корректность низкоуровневой спецификации
2. Модульное проектирование: Разделение рассуждений о структурах данных и рассуждений об приближениях с плавающей точкой
3. Восходящее выведение: Обратный вывод инвариантов цикла из требований доказательства логики Хоара программы

Результаты экспериментов

Основные достижения

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. Более крупные системы: Интеграция этого модуля в верификацию полного решателя уравнений в частных производных
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 — библиотека формального доказательства для программ линейной алгебры

Резюме: Данная статья демонстрирует осуществимость полной формальной верификации сложных численных алгоритмов, предлагает практическую методологию верификации и вносит важный вклад в развитие надёжного научного вычислительного программного обеспечения. Несмотря на высокие затраты на верификацию, её ценность в обнаружении практических ошибок и предоставленное методологическое руководство делают её важной работой в данной области.