Lean и LLM: как автоматизировать доказательства при реализации Zstandard
Автор эссе экспериментирует с Lean, языком с зависимыми типами, в котором можно записывать инварианты программы в типах и затем машинно проверять их. Такой подход позволяет формализовать тонкие требования, которые в обычных языках часто остаются лишь в комментариях и теряются по мере роста команды. Но практическое применение тормозит стоимость доказательств: в ретроспективе проекта seL4 на доказательства ушло примерно в десять раз больше времени, чем на проектирование и реализацию, а строк кода доказательств оказалось более чем в двадцать раз больше, чем строк C-кода.
Предыдущая автоматизация, например в F*, может поручать обязательства SMT-решателю, однако автор отмечает, что на более сложных случаях решатель способен работать часами. Появление LLM меняет ситуацию: если формулировка утверждения верна, для проверки важен сам факт существования доказательства, а не его содержание. По ограниченным тестам автора, LLM могут строить доказательства и при этом избегать такого усложнения, которое заставляет проверку типов расходовать огромный объём памяти. Это может сделать зависимые типы заметно практичнее, хотя остаются задачи по поддержанию доказательств после изменений кода и контролю сложности проверки.
Для опыта автор написал на Lean распаковщик Zstandard. В материале он также объясняет устройство формата: Zstandard, компрессор семейства LZ77 с быстрым распаковыванием; помимо деревьев Хаффмана он использует энтропийный кодировщик FSE. FSE представляет кодирование как таблицу состояний: более вероятным символам достаётся больше состояний, а комбинация состояний, читающих разное число битов, позволяет в среднем тратить на символ дробное число бит. Сжатые данные кодируются с конца последовательности, поэтому распаковщик читает биты блока в обратном направлении. В Zstandard FSE главным образом применяется для эффективного кодирования смещений и длин ссылок на уже распакованные данные.
Ключевые факты
- В Lean типы могут выражать инварианты программы; машина затем проверяет их соблюдение.
- По ретроспективе seL4, доказательства потребовали примерно в 10 раз больше времени, чем проектирование и реализация, и дали более чем в 20 раз больше строк, чем C-код.
- Автор считает, что LLM вместе с принципом несущественности доказательства могут автоматизировать значительную часть работы над формальными доказательствами.
- Эксперимент автора, распаковщик Zstandard на Lean; в ограниченных тестах LLM не вызывали чрезмерного роста потребления памяти проверкой типов.
- Zstandard использует FSE для кодирования смещений и длин обратных ссылок; таблица состояний позволяет приблизиться к дробному числу бит на символ.
Почему это важно
Формальные доказательства помогают закреплять важные инварианты в коде, но их ручное написание слишком дорого для массового применения. Если LLM действительно снимают значительную часть этой нагрузки, зависимые типы могут стать практичнее за пределами узкой области формальной верификации.
Кому это важно
Разработчикам системного ПО, пользователям Lean и других языков с зависимыми типами, а также командам, которым нужно машинно проверять свойства реализации. Материал особенно полезен тем, кто интересуется реализацией форматов сжатия и формальной верификацией.
Как это применить
Подход автора, взять реальную реализацию, сформулировать её инварианты в Lean и использовать LLM как помощника при построении доказательств. При этом следует отдельно следить за тем, чтобы изменения кода не ломали структуру доказательств и чтобы проверка типов не становилась чрезмерно ресурсоёмкой.
Можно ли доверять
Это личный технический опыт автора, а не сравнительное исследование: он прямо оговаривает, что его тесты ограничены. Числа о трудоёмкости взяты из упомянутой им ретроспективы проекта seL4; описание FSE дано как объяснение механизма Zstandard.
Риски и подводные камни
Автоматизация не отменяет необходимости правильно сформулировать утверждение: доказательство ложной цели получить нельзя. Даже корректные доказательства могут быть хрупкими при изменениях программы, а сложные конструкции способны перегружать проверку типов по времени и памяти.