Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Формальную проверку функций PETSc удалось частично автоматизировать, не поручая LLM писать проверяющую программу. Работа Argonne National Laboratory и University of Delaware нашла в MatAYPX ошибку, которая жила в коде с 1997 года; это нерецензированный препринт, и приведённые числа получены самими авторами. Для команд результат предлагает безопасную границу: модель формулирует проверяемое требование, а исполняемую часть строят обычные инструменты.
LLM пишет только то, что можно быстро проверить вручную
Обычный подход с LLM выглядел бы так: модель получает документацию функции и сразу генерирует проверяющую программу. Но такая программа сама становится источником ошибок. В ней нужно правильно создать символические входы, настроить MPI, разделить варианты исполнения и сравнить результат с ожидаемым поведением.
Предложенный конвейер оставляет модели более узкую задачу. Она читает документацию и прототип функции, а затем составляет короткий контракт на ограниченном подмножестве ACSL — языка для описания требований к программам на C. Контракт задаёт допустимые входы, ожидаемый результат и части объекта, которые функция может изменить.
Модель не получает доступ к репозиторию PETSc. Это снижает риск, что контракт повторит ошибочное поведение реализации вместо требований документации. В опыте использовали Claude Opus 4.8 с отключёнными инструментами и сохранением сессии.
Затем специалист по PETSc сверяет контракт с документацией, семантикой API и при необходимости с реализацией. Неясные случаи он решает явно. Например, если документация не запрещает передавать одну матрицу в двух аргументах, проверяющий должен определить, допустимо ли такое совмещение, а не позволять модели угадать ответ.
После ручного подтверждения acsl2civl разбирает контракт и детерминированно создаёт проверяющую программу для CIVL. Неподдерживаемую конструкцию инструмент отклоняет, а не заменяет приближением. CIVL символически перебирает состояния и проверяет, что реализация выполняет контракт во всех вариантах внутри заданных границ.
Совпавшие аргументы превратили правильную формулу в ошибочную
Конвейер применили к MatAXPY, MatAYPX и режиму MatFilter без сжатия матрицы. Для MatAXPY уже существовала отдельно написанная эталонная модель, поэтому CIVL сравнивал реализацию и с ней, и с контрактом. Для двух других функций единственным описанием правильного результата служил подтверждённый человеком контракт.
Ошибка проявилась в MatAYPX, которая должна вычислять Y = aY + X. Контракт допускал, что X и Y указывают на одну матрицу: документация не вводит запрета, а реализация предусматривает такой вызов.
MatAYPX сначала умножает Y на a, а затем прибавляет X. Если оба аргумента совпадают, на втором шаге X уже тоже содержит масштабированную матрицу. Функция возвращает 2aY вместо документированного (1+a)Y. Именно сгенерированный отдельный случай для совпадающих аргументов вывел CIVL на нарушение контракта.
MatFilter показал другую сторону подхода: контракт может описывать условное изменение каждого элемента. Значение с модулем не больше заданного порога заменяется нулём, остальные значения сохраняются. Чтобы выразить это правило, разработчики расширили поддерживаемый язык вещественными параметрами, сравнением, модулем и условными выражениями.
Проверка охватывала до двух процессов MPI и матрицы со сторонами до трёх элементов. CIVL работал с плотным логическим представлением матриц; оно скрывает распределённое хранение и не подтверждает свойства разреженных структур. Перенос проверяемой функции в совместимый с CIVL код, модель PETSc, acsl2civl и сам CIVL остаются доверенными частями контура.
Планы меняет не генерация, а граница доверия
Работа не превращает формальную проверку большой библиотеки в полностью автоматический процесс. Для каждой новой группы операций по-прежнему нужны специалист, точная модель среды и совместимый перенос реализации. Сборка распределённых матриц, разреженное хранение и операции вроде сумм и норм пока требуют дальнейшего расширения инструментов.
Практический шаблон можно применять шире PETSc. LLM стоит поручать небольшой декларативный артефакт, который специалист способен прочитать целиком: контракт API, инвариант состояния или набор постусловий. Всё, что создаёт входы, запускает систему и принимает решение о корректности, лучше генерировать детерминированно из уже проверенного описания.
Такой дизайн особенно уместен, если команда уже планирует формальную проверку критической библиотеки или вычислительного ядра. Он сокращает область ручной проверки с полной проверяющей программы до контракта и сохраняет воспроизводимость последующих шагов. При этом эксперт не исчезает из процесса: именно он отвечает за соответствие контракта документации и решает неоднозначные случаи.
Для обычной автоматизации тестов работа даёт скорее архитектурный принцип, чем готовый инструмент. Полезная часть результата — не выбор конкретной модели, а разделение ролей: LLM переводит текст в строгую форму, человек подтверждает смысл, а проверенный компилятор превращает её в исполняемую проверку.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
