Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Формально проверенный код от LLM может пройти верификатор и всё равно не быть связанным с требованиями задачи. Это показал препринт Verified but Vacuous, который не прошёл рецензирование, а все числа получили сами авторы: на HumanEval верификатор принял 99,1% решений, но только 1,9% сертификатов ссылались на заданную спецификацию. Командам, которые строят генерацию доказуемого кода, придётся разделить одну метрику «verified» на несколько последовательных проверок.
Что именно доказывает верификатор
Авторы делят проверку на три этапа. Первый отвечает только на технический вопрос: принял ли формальный верификатор программу и доказательство. Он находит ошибки типов, незавершённые доказательства и невыполненные обязательства, но не гарантирует, что эти обязательства описывают нужное поведение.
В Dafny метод может пройти проверку без функционального постусловия ensures. В таком случае система докажет корректность тех обязательств, которые действительно присутствуют: например, завершение метода и согласованность типов. Но она не докажет, что функция возвращает максимум массива или правильно рассчитывает платёж, если это требование не записано в постусловии.
Второй этап проверяет синтаксическую связь со спецификацией. Предложенный авторами фильтр разбирает дерево программы и требует, чтобы хотя бы одно постусловие ссылалось на предикат или функцию из отдельного файла спецификации. Так он отсеивает сертификаты без постусловий и доказательства, не связанные с внешним контрактом.
Этот фильтр не оценивает смысл контракта. Содержательное постусловие, записанное прямо в реализации, может не пройти его, а именованный предикат, который всегда возвращает истину, — пройти. Поэтому нужен третий этап: проверка того, что формальная спецификация действительно передаёт исходное требование.
Для этого постусловие можно превратить в исполняемый предикат и проверить на положительных и отрицательных примерах. Если контракт принимает результат, который тестовый эталон считает неправильным, спецификация описывает задачу неполно. Обычные тесты здесь проверяют не только реализацию, но и границы самого формального требования.
Где распадается цепочка проверок
Первый разрыв авторы измерили на Li@Opus — воспроизведении существующего конвейера с Claude Opus 4.7. Модель генерировала Dafny как промежуточное представление, после чего код переводили в Python. Проверку провели на HumanEval, LeetCodeDataset и LiveCodeBench v6: доля принятых верификатором решений оставалась высокой, а доля сертификатов со ссылкой на спецификацию — низкой на всех наборах.
Причина видна в структуре подсказки. Примеры предлагают метод без постусловия и запускают проверки через expect. Dafny исполняет такие проверки во время работы программы, но не доказывает общий функциональный контракт. Это не делает полученный код автоматически неправильным, однако показатель принятия верификатором нельзя трактовать как доказательство соответствия задаче.
Второй разрыв проверили на собственном конвейере VCG, где все выпущенные компоненты уже обязаны ссылаться на спецификацию. Код генерировали для Rust и затем запускали на скрытых тестах. Среди структурно проверенных решений тесты не прошли 11,48% примеров на MBPP-Rust и 14,82% на части VeriContest LC.
Значит, обязательная ссылка на контракт закрывает только синтаксический разрыв. Реализация может полностью соответствовать формуле, но сама формула — разрешать неверные результаты. На VeriContest LC весь путь от условия до кода, доказательства и проверки постусловия прошли 7,79% попыток.
Работа охватывает один модельный бэкенд, два целевых языка и пять наборов задач. Li@Opus и VCG используют разные подсказки, архитектуру и циклы исправления, поэтому результаты показывают классы отказов, а не преимущество одного конвейера над другим.
Как это меняет планы продуктовых команд
Если система уже выпускает формальные сертификаты, менять нужно прежде всего критерий готовности. Успешный ответ Dafny или другого верификатора следует хранить как отдельную техническую метрику, а не как итоговую долю корректного кода.
После верификатора стоит добавить статический фильтр, который проверяет наличие постусловия и его связь с выделенной спецификацией. Такой этап легко встроить в цикл генерации и исправления: решение без связанного контракта возвращается модели до компиляции и тестирования.
Следующий шлюз должен проверять смысл спецификации. Практический вариант — запускать постусловие на примерах с правильными и заведомо неправильными ответами, а реализацию отдельно проверять скрытыми тестами. В отчёте полезно показывать, сколько решений прошло верификатор, сколько связало доказательство с контрактом и сколько подтвердило поведение.
Работа не требует отказываться от Dafny или генерации через промежуточное представление. Она меняет значение слова «проверенный»: сертификат подтверждает только явно сформулированное утверждение. Для платёжной логики, медицинских расчётов и разборщиков недоверенных данных этого недостаточно, пока команда не проверила происхождение и полноту самой спецификации.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
