Долгое время зависимо-типизированные языки вроде Coq (недавно переименованного в Rocq) и Lean выглядели как мечта: можно записать инварианты прямо в типах, и машина проверит их. Но цена — громадные усилия на доказательства. Проект seL4, например, потратил в 10 раз больше времени на доказательства, чем на написание кода, а строк доказательств оказалось в 20 раз больше, чем C-кода. Попытки автоматизировать это с помощью SMT-солверов (F*) часто упирались в то, что солвер уходит в астрал на часы, и программисту приходилось развивать чутьё на то, какие формулировки ему понравятся.
Появление LLM всё меняет. Поскольку в теории важно лишь существование доказательства, а не его конкретное содержимое, языковые модели обещают стать крайне эффективной автоматизацией. Чтобы проверить идею, автор написал декомпрессор Zstandard на Lean, в основном доверив доказательства LLM.
Zstandard использует продвинутый энтропийный кодировщик FSE — конечный автомат с несколькими состояниями на символ. За счёт того, что для частых символов часть состояний читает один бит, а часть — два, в среднем кодируется дробное число бит, чего нельзя добиться в классических деревьях Huffman. Таблица состояний строится на лету по переданным вероятностям, без явной передачи. Декодировать приходится с конца блока, двигаясь по битовому потоку назад.
На Lean автор доказал универсальные свойства алгоритма построения таблицы FSE: что размер таблицы корректен для заданной точности, количество состояний каждого символа соответствует вероятности, и для любого символа с ненулевой вероятностью существует ровно одно подходящее состояние, которое может достичь любой целевой номер. Это именно те нетривиальные допущения, на которых держится оптимизированный внутренний цикл декодера, и в языках без зависимых типов они максимум живут в комментариях. Все доказательства LLM сгенерировали примерно за 20 минут, потратив лишь небольшую долю квоты подписки за $20/мес. Чтобы облегчить работу прувера, пришлось переписать часть кода, заменив императивные куски в Id.run.
Экспериментальный декомпрессор получился в 10 раз медленнее эталонного zstd, а сильные типы могут болезненно усиливать вносимые изменения. Но факт остаётся: автоматизация доказательств уже здесь, и у нас практически появился новый класс языков, доступных для повседневной разработки. Автор также заглянул в сторону верифицированного ассемблера: семантика AArch64, которую сделала AWS в проекте LNSym, теоретически позволяет доказывать эквивалентность оптимизированного кода и эталонной реализации на Lean. Однако даже небольшой пример popcount требовал больше памяти, чем есть на машине, а доказать что-то крупнее крошечных функций не удалось — пока это не масштабируется.