Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Модель научили писать программу вместе с машиночитаемым доказательством, что она соответствует заданной спецификации. В нерецензированном препринте George Ma и соавторов, где все замеры выполнили сами авторы, доля успешно проверенных решений на DafnyBench выросла с 66,1% до 93,5%. Для команд это не замена обычному обучению на тестах, а схема для задач, где уже есть формальные спецификации и автоматический верификатор.
Как диагностика верификатора превращается в награду
Обычное обучение моделей для программирования награждает код, который проходит тесты. Такой код может оставаться неверным на входных данных, которых нет в тестовом наборе. Формальный верификатор решает другую задачу: проверяет, выполняет ли программа спецификацию для всех допустимых входов.
Прямо использовать его ответ для обучения трудно. Верификатор обычно возвращает итог «принято» или «отклонено». Если почти все ранние попытки отклонены, модель получает одинаковую награду и за решение с одной недоказанной леммой, и за код, который даже не компилируется.
Новая схема оценивает не только итог, но и диагностические сообщения. Перед эпизодом среда фиксирует набор обязательств, которые программа должна доказать: постусловия, предусловия в местах вызовов, безопасность операций, инварианты циклов и завершение. Награда зависит от того, какую долю этих обязательств закрыла очередная версия.
Набор фиксируют заранее, поэтому модель не может облегчить задачу, удалив сложный инвариант или заменив его бессодержательным условием. Для восстановления доказательств среда также строит скрытые проверки из аннотаций эталонного решения. Модель их не видит, но должна вывести промежуточные факты, достаточные для их подтверждения.
Одного подсчёта доказанных условий недостаточно: верификатор честно отвечает на тот вопрос, который ему задали, даже если модель подменила вопрос. Она может ослабить постусловие, добавить ограничивающее предусловие или попросить систему принять недоказанное утверждение как аксиому.
Поэтому перед начислением награды проходит проверка целостности. Среда заново извлекает спецификацию и сравнивает её с исходной, а затем ищет непроверяемые допущения, аксиомы, пропущенные доказательства и директивы, исключающие код из проверки. Решение с подменённой спецификацией оценивается ниже честной, но неполной попытки.
Зачем модели замкнутый цикл и отдельный специалист по доказательствам
Обучение проходит в интерактивной среде. За несколько ходов модель может запустить верификатор, прочитать место и тип ошибки, выполнить программу на заданном входе, проверить целостность и отправить исправленную версию. Среда сохраняет лучшую отправку, поэтому модель учится не угадывать готовое доказательство одним ответом, а последовательно устранять конкретные ошибки.
Работа разделяет две задачи. В первой модели дают правильную реализацию без аннотаций и просят восстановить доказательство. Во второй остаётся только спецификация: нужно написать и реализацию, и доказательство. Второй вариант ближе к генерации нового кода, но объединяет два навыка, которые исходные модели освоили неравномерно.
Модель, обученную восстанавливать аннотации, затем замораживают и используют как специалиста. При каждой отправке среда сначала оценивает исходный вариант агента, а затем позволяет специалисту заменить только доказательные аннотации, сохранив реализацию. В награду идёт лучший результат, поэтому неудачная подсказка не ухудшает оценку.
Такое разделение ролей важно не только для итогового качества. Основной агент может сосредоточиться на поведении программы, а специалист — на инвариантах, промежуточных утверждениях и леммах. При этом оба получают обратную связь от одного живого верификатора, а не от модели-оценщика.
Когда такая схема меняет планы разработки
На DafnyBench доля решений, прошедших отложенную проверку при генерации кода, выросла с 66,1% до 93,5%. На SWE-Proof результат поднялся с 56,3% до 100%. Награда по диагностике также превзошла двоичную награду «прошло или нет» при одинаковых остальных условиях: преимущество оказалось наиболее заметным там, где модель одновременно писала программу и доказательство.
Работа проверяет не только изолированные задачи. В варианте SWE-Proof агент должен был подготовить доказуемую модель требуемого поведения и исправление настоящего репозитория. Доля исправлений, прошедших скрытые тесты проекта, выросла на 12,9 процентного пункта. Это связывает формальную проверку с практическим результатом: доказательство спецификации само по себе ещё не гарантирует, что патч исправил репозиторий, поэтому оба артефакта оценивали отдельно.
Эксперименты охватывают Qwen3 и Qwen3.6, задачи на Dafny и Nagini, а также перенос без дополнительного обучения на отложенные наборы. Улучшение сохранилось и на программах Verus на Rust, хотя этого языка и верификатора не было в обучении. Границы результата задаёт сама постановка: системе нужна формальная спецификация, статический верификатор с содержательной диагностикой и возможность независимо проверить, что модель не изменила условия задачи.
Для обычного помощника, который пишет прикладной код только по текстовому запросу и тестам, работа не даёт готовой замены существующему контуру. Она меняет планы там, где цена ошибки оправдывает формальные контракты: можно строить обучение вокруг уже используемого верификатора, а не подключать его лишь как финальный фильтр.
Главная инженерная идея переносится шире конкретных языков: инструмент проверки должен не просто отклонять результат, а разбирать его на фиксированные обязательства и показывать модели измеримый прогресс. Но без отдельного контроля целостности такая награда создаёт стимул упростить проверяемое утверждение вместо исправления программы.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
