Теперь у нас есть автоматизация доказательств

Адам Лэнгли (Adam Langley) написал распаковщик Zstandard на Lean, чтобы проверить конкретный тезис: LLM устранили то самое препятствие, из-за которого языки с зависимыми типами не приживались в обычной разработке ПО. Его вывод точен и подкреплён делом. Доказательства нетривиальных универсальных свойств для реального кода декодера теперь обходятся дёшево. А вот верифицированный ассемблер, который он тоже попробовал реализовать, - нет.

Цена, державшая зависимые типы в нише

Главное обещание системы зависимых типов в том, что инварианты, обычно остающиеся лишь комментариями (и перестающие соблюдаться по мере роста команды), можно записать формально и проверять машиной. Платой за это всегда были усилия на доказательство. Лэнгли ссылается на ретроспективу seL4: команда потратила на доказательства примерно в десять раз больше времени, чем на проектирование и реализацию, а строк доказательств в итоге оказалось в двадцать с лишним раз больше, чем строк на C. Он добавляет к этому сценарий неудачи, который в такие соотношения не попадает: потратить часы на доказательство и обнаружить, что исходная цель была ложной.

Привычный способ упростить задачу - автоматизация через SMT-решатели, как в F*. Она справляется с простыми обязательствами, а затем внезапно буксует, причём предсказать это трудно: легко написать условие, из-за которого решатель уйдёт в работу на долгие часы, и невозможно понять, завершится ли он вообще. Люди, работающие с такими системами ежедневно, вырабатывают чутьё на то, что нравится решателю, и подгоняют структуру кода под него. Вердикт Лэнгли по этому поводу - лучшая фраза заметки: это "превращает задачу в мистицизм, заставляя служить сложному и капризному божеству".

LLM предлагают другой тип автоматизации благодаря нерелевантности доказательств (proof irrelevance). Если утверждение сформулировано верно, значение имеет сам факт наличия доказательства, а не его внутренности. На практике этому мешают две вещи. "Инженерия доказательств" (proof engineering), о которой говорили авторы seL4, - это работа по структурированию доказательств так, чтобы их можно было дёшево обновлять при изменении кода; кроме того, излишне сложные доказательства способны исчерпать всю память проверщика типов. Если доказательства генерирует заново машина по запросу, первая проблема почти исчезает. Вторая остаётся, хотя в тестах Лэнгли LLM удавалось её избегать.

Что удалось доказать

Конкретный результат получен на построении таблиц FSE. Лэнгли реализовал алгоритм из RFC 8878, превратил три тестовых вектора из RFC в модульные тесты, а затем сформулировал теорему для всех возможных входных данных:

theorem ofDistribution_wellFormed (h : ofDistribution accuracyLog probs = some t) :
    t.entries.size = 2 ^ accuracyLog ∧
    (∀ s : Fin probs.size,
      t.entries.toList.countP (fun e => e.symbol == s.val) = probCells probs[s]) ∧
    (∀ (i : Nat) (hi : i < t.entries.size) (v : Nat), v < 2 ^ (t.entries[i]'hi).nbBits →
      (t.entries[i]'hi).baseline + v < 2 ^ accuracyLog) ∧
    (∀ (s : Fin probs.size), 0 < probCells probs[s] → ∀ x < 2 ^ accuracyLog,
      ∃! i : Nat, ∃ hi : i < t.entries.size,
        (t.entries[i]'hi).symbol = s.val ∧ (t.entries[i]'hi).baseline ≤ x ∧
          x < (t.entries[i]'hi).baseline + 2 ^ (t.entries[i]'hi).nbBits) := …

Простыми словами: если конструктор вообще возвращает таблицу, то её размер строго соответствует параметру точности; каждому символу достаётся ровно столько состояний, сколько требует его вероятность; чтение nbBits бит с прибавлением базового смещения всегда даёт корректный номер состояния; и для каждого символа с ненулевой вероятностью и любого целевого состояния существует ровно одно исходное состояние этого символа, ведущее в него. Эти четыре факта - в точности те допущения, на которые опирается оптимизированный внутренний цикл декодирования и которые не способна выразить ни одна мейнстримная система типов.

Несколько LLM сгенерировали это доказательство автоматически примерно за двадцать минут, потратив малую долю лимита подписки за $20 в месяц. Лэнгли подтвердил, что проверка типов проходит без заглушек sorry. Одной оговорки он не скрывает: моделям сначала потребовалось изменить код генерации таблицы, так как автор злоупотребил Id.run для перехода в императивный стиль, с чем механизмам доказательства работать сложнее. Разработка mvcgen в Lean как раз нацелена на устранение этого разрыва.

Менее масштабный пример в заметке показывает ту же идею на бытовом уровне. Блок типа rle имеет размер данных в один байт, поэтому обращение по индексу blockBytes.val[0] безопасно - и в Lean это доказывается прямо в месте обращения, а не принимается на веру:

let b := blockBytes.val[0]'(by
  rw [blockBytes.property, blockHeader.contentSize_rle hty]; omega)

Свойство blockBytes.property берётся из типа возвращаемого значения функции readExact: IO {ba : ByteArray // ba.size = n}, где длина зафиксирована прямо в типе. C в таком месте даёт неопределённое поведение, современные языки - исключение во время выполнения или option; Lean предлагает третий путь: доказать, что подобная ситуация в принципе невозможна.

Почему FSE - интересная цель

Zstandard вытесняет gzip, потому что очень быстро распаковывает данные: график Лэнгли для 64 МиБ исходников Lean/mathlib помещает zstd и gzip в отдельную лигу по скорости распаковки (в логарифмическом масштабе), тогда как bzip2 и LZMA работают на порядки медленнее в обмен на более сильное сжатие. (Замеры проводились на машине Apple, где gzip необычайно хорошо оптимизирован.) И именно энтропийный кодер обеспечивает эту скорость.

Код Хаффмана может тратить на символ только целое число бит. Если идеальная цена символа составляет 2.3 бита, приходится округлять, и плата за это округление ложится на остальной алфавит. FSE обходит это ограничение через конечный автомат. Состояний в нём больше, чем символов, и каждый символ получает долю состояний, пропорциональную его вероятности. Каждое состояние хранит три вещи: свой символ, количество бит, которые нужно прочесть из потока, находясь в нём, и базовое смещение, прибавляемое к этим битам для перехода в следующее состояние. Сами состояния по-прежнему считывают целое число бит, но для символа с идеальной ценой в полтора бита половина состояний может читать один бит, а вторая половина - два, попадая в среднее значение. В примере из заметки с 16 состояниями символ B занимает пять состояний с вероятностью 5/16, что даёт идеальную цену в 1.68 бита; три его состояния читают по два бита, а два - по одному, так что взвешенное среднее оказывается близким к идеалу. Сама таблица по сети не передаётся: RFC задаёт алгоритм её восстановления исключительно из вероятностей, поэтому функцию построения таблицы так важно доказать.

Отсюда следуют два структурных вывода. Любой символ может идти за любым другим, поэтому из каждого символа должна быть возможность попасть в любое состояние; символу D с единственным состоянием приходится читать четыре бита, чтобы адресовать все шестнадцать, тогда как пять состояний символа B делят пространство состояний между собой так, что ровно одно B-состояние ведёт в каждую конкретную цель. Это свойство разбиения - четвёртый пункт приведённой выше теоремы. А поскольку выбор состояния переносит информацию вперёд, кодирование не может идти в прямом порядке: кодер начинает с конца последовательности и двигается назад, при этом выводя данные последовательно, из-за чего распаковщику приходится переходить в конец блока и читать биты в обратном направлении. FSE не хранит связей между символами; эта задача ложится на внешний слой LZ77, а FSE в основном кодирует смещения и длины ссылок назад, причём Хаффман всё ещё используется в других частях формата.

Lean как язык программирования

Аргументы Лэнгли в пользу Lean не ограничиваются доказательствами. Язык строгий, а не ленивый, поэтому, в отличие от Haskell, легко понимать, когда именно выполняются вычисления. Его монадическая do-нотация поддерживает for, return и break, так что код императивного вида читается как привычный императивный код. Кроме того, Lean мутирует объекты на месте, если счётчик ссылок на них равен единице, что делает обновление массивов столь же дешёвым, как в императивных языках. Последнее - опасный момент, потому что в Lean нет линейных типов, помогающих удерживать счётчик на единице: случайная лишняя ссылка на большой массив способна обрушить производительность без каких-либо предупреждений от компилятора.

Что не сработало

Вторая часть эксперимента касалась верифицированного ассемблера. Проект LNSym от AWS даёт Lean семантику и симулятор для AArch64. Это наводит на мысль о рабочем процессе, где оптимизированная ассемблерная процедура доказывается на эквивалентность её аналогу на Lean, вызывается во время выполнения через extern, а LLM получают свободу оптимизировать код без риска внести функциональные ошибки - дешёвый верифицированный ассемблер там, где сегодня он экономически оправдан только для криптографии. Масштабировать это не удалось. Собственный пример LNSym с 32-битным подсчётом единиц (popcount) использует сертифицирующий SAT-решатель bv_decide и требует больше памяти, чем есть на машине Лэнгли. Крошечные функции работают от начала до конца, включая вызов через extern. Продвинуться дальше не удалось ни автору, ни нескольким LLM.

Открытые вопросы он перечисляет честно. Затраты на доказательства в крупных системах могут расти непропорционально быстро, обгоняя возможности моделей. Очень строгие типы увеличивают радиус поражения при изменениях, ведь обновлять приходится каждый производный тип. Lean - высокоуровневый язык и подходит не для всего; собственный декодер автора работает примерно в десять раз медленнее утилиты zstd. Код он публиковать не стал, рассудив, что для столь чётко поставленной задачи LLM наверняка справится лучше него, и сослался на проект lean-zip, где зашли ещё дальше и доказали корректность сжатия с последующей распаковкой (round-tripping).

Контекст

Тезис автора строг и проверяем, именно поэтому на него стоит обратить внимание. Речь не о том, что формальная верификация решена как класс задач; речь о том, что одна конкретная статья расходов - доказательство нетривиального универсального свойства для работающего кода декодера - сократилась с дней работы эксперта до двадцати минут инференса. Это рассуждение той же структуры, что и в if-ai-writes-your-code-why-use-python по поводу выбора языка: человеческие затраты, делавшие инструмент непрактичным, сняты моделями. И здесь сохраняется та же слабость: исчезли именно измеряемые затраты, а не обязательно те, что доминируют в реальном проекте. В llm-mathematical-research рассматривается соседний случай, когда модели создают формальный или исследовательский математический контент, а не чинят доказательства для кода. Шрирам Кришнамурти (Shriram Krishnamurthi) в pl-education-in-the-age-of-ai высказывает оптимизм по поводу того же сдвига, но предупреждает о сценарии, которого данная заметка почти не коснулась: если модель не находит доказательства, человек без экспертных знаний не получает контрпримера и остаётся ни с чем.

Зависимые типы находятся на дальнем конце статической оси в type-system-axes - проверки выполняются полностью до запуска программы для сколь угодно произвольных свойств, включая простоту чисел и уникальную достижимость. Материалы базы знаний по coverage-guided-fuzzing и differential-fuzzing описывают прагматичную альтернативу ровно для таких задач: декодер формата с эталонной реализацией для сравнения - хрестоматийная цель дифференциального фаззинга, и фаззинг находит контрпримеры там, где доказательство гарантирует их отсутствие. Баланс между ними теперь оценивается совсем иначе, чем раньше.