Починка формальных доказательств сборщика мусора CertiGC с Codex
Автор статьи на arXiv чинил с помощью Codex доказательства на Rocq для верифицированного сборщика мусора CertiGC. Локальный ремонт агенту удался, но проверять, что его инварианты сохраняют спецификацию, пришлось человеку.
Что сделали
Codex получил доступ к репозиторию, правил файлы доказательств на Rocq, запускал выборочную сборку через make и смотрел состояния доказательств через сервер rocq-mcp. Сначала он починил доказательства на VST, потом теорему об изоморфизме графов. Инвариант recorded-backward-edge предложил сам Codex, а автор его проверил. Любое изменение Definition автор требовал сначала обсудить и не принимал новые предусловия VST без обоснования.
Что получилось
Ветка собралась и вошла в основной проект как PR 30. Главную теорему приняли 29 апреля, а позднейший аудит убрал устаревшую посылку no-backward-edge. Это один случай, а не контролируемое исследование.
На что обратить внимание
Будьте готовы к плотному надзору. За десять дней ушло около 59 часов активной работы Codex, 415 промптов от человека и 13 305 вызовов инструментов, а ускорение никто не измерял.
Пояснение
Rocq (бывший Coq) это система, в которой математические доказательства пишут как код и проверяют машиной. VST (Verified Software Toolchain) это набор инструментов для доказательства корректности программ на C. Сборщик мусора автоматически освобождает память, которой программа больше не пользуется.
Кому пригодится
Исследователям и инженерам, которые занимаются формальной верификацией и думают, можно ли отдать агенту ремонт доказательств.
Попробуйте сами с Codex
В моём проекте на [Coq, Lean или Isabelle] в [папка] сломалось доказательство [файл или лемма] после [ваше изменение]. Правь файлы, запускай сборку и почини доказательство минимальными локальными изменениями. Не ослабляй и не меняй спецификации и инварианты, не спросив меня. В конце дай список всех утверждений, которые ты изменил, чтобы я их проверил.
Нужна помощь с запуском? Вступайте в сообщество AI Pack ↗
Источник: arxiv.org ·