При аудите полноты спецификации задача не просто найти программу, которая проходит проверку. Нужно обнаружить программу, допустимую по записанному контракту, но нарушающую предполагаемое поведение. В препринте Adarsh Agrawal сравниваются три политики такого поиска: Direct, IntentShield и Phase. На 12 задачах Verus/Rust автор сообщает о большем выходе сертифицированных свидетелей у подхода без корректирующей обратной связи, но эффект не следует переносить на другие языки и среды. Источник: препринт на arXiv.
Что именно сравнивается: аудит полноты, а не обычная проверка корректности
Свидетель неполноты — не просто неудачная реализация и не сообщение об ошибке компилятора. По критериям статьи кандидат должен пройти ослабленный контракт, в котором удалено значимое постусловие; после возвращения постусловия проверка должна провалиться. Кроме того, программа должна компилироваться и исполняться, а её поведение — расходиться хотя бы с одним официальным тестом. Такой набор условий связывает подозрение на пропущенное требование с проверяемым примером.
Различие между аудитом и обычной починкой важно для выбора стратегии: обратная связь, полезная для устранения ошибки, может направить поиск к программе, которая удовлетворяет текущему контракту, но перестаёт показывать, чего в нём не хватает.
Критерии сравнения трёх стратегий
Сравнивать политики стоит по трём вопросам: как организованы попытки, какие сигналы получает модель во время поиска и что происходит после обнаружения кандидатов. В таблице приведены только свойства и числа, сообщённые в препринте; это не независимый тест редакции.
| Критерий | Direct | IntentShield | Phase |
|---|---|---|---|
| Поиск кандидатов | Независимые попытки | Итеративный цикл | Отдельный этап поиска, затем передача результатов |
| Корректирующая обратная связь при поиске | Нет | Да: результаты компиляции, верификатора и видимых тестов | Не используется между фазами |
| Переиспользование ответов между этапами | Не описано как отдельная фаза | Ответы включены в итеративный цикл | Нет, согласно аннотации |
| Результат обнаружения | Относится к no-feedback discovery в целом | 27,1% сертифицированных свидетелей | Совокупный выход сопоставим с no-feedback discovery; отдельное число в доступном описании не приведено |
| Подходящий сценарий по логике метода | Независимое исследование кандидатов | Поиск с использованием сигналов об ошибках | Разделение обнаружения и последующей проверки или исправления |
Значения 59,0% и 27,1% — доли сертифицированных свидетелей в описанных авторами сравнениях, а не доли задач, решённых успешно. Первое значение относится к no-feedback discovery в целом, поэтому его нельзя приписывать исключительно Direct как отдельному замеру. Авторы сообщают, что при равном бюджете вызовов no-feedback discovery дал примерно в 2,18 раза больший выход свидетелей, чем цикл IntentShield.
Условия эксперимента и измеренный разрыв
Описанное сравнение охватывает 12 задач Verus/Rust и четыре семейства моделей; авторы указывают на сопоставимые бюджеты вызовов. Контроль с итеративными вызовами и форматированием, согласованным с IntentShield, должен был отделить эффект корректирующей информации от эффекта независимых перезапусков. По сообщению авторов, большая часть разрыва связана с содержанием обратной связи, а не только с независимостью попыток.
Это делает результат аргументом против автоматического включения обратной связи именно в фазу поиска свидетелей, а не доказательством того, что обратная связь всегда вредна. Для проверки или исправления уже найденного кандидата задачи иные: там сигналы верификатора могут быть полезны, но исследование рассматривает их раздельно от первичного обнаружения.
Различия между Direct, IntentShield и Phase
Direct подходит как простая политика поиска, если важна независимость попыток от результатов предыдущих. В изложении статьи он относится к no-feedback discovery. Однако доступные числа не дают отдельного процента Direct рядом с IntentShield, поэтому выбирать Direct как численного победителя по этим данным нельзя.
IntentShield передаёт модели результаты компиляции, верификатора и видимых тестов. Это наиболее прямой вариант для цикла, где следующая попытка корректируется по предыдущим ошибкам. Но в поставленной задаче такое направление может подавлять примеры, которые проходят неполный контракт и тем самым обнаруживают пропущенное требование.
Phase разделяет обнаружение и дальнейшую работу: сначала выполняется поиск по протоколу Direct, затем результаты передаются на сертификацию и исправление. Авторы сообщают, что отдельное выполнение Phase достигло совокупного выхода no-feedback discovery без повторного использования ответов. Поэтому в описанном Verus/Rust-процессе это наиболее подходящая из трёх политик, когда нужно сохранить свидетель до перехода к починке контракта; это не универсальный рейтинг для других языков и сред.
Что даёт сохранение свидетелей при исправлении спецификации
Практический смысл раздельных фаз проверяется не только числом найденных кандидатов. В downstream-оценке авторы сообщают об успешной реализации в 81,3% случаев для Phase-Revised против 62,5% для IS-Revised. Это показатели успеха реализации на исправленных спецификациях, а не доли обнаруженных свидетелей. Direct-Revised, по аннотации, оказался близок к Phase-Revised, но точное значение в доступном описании не приводится.
Для процесса аудита отсюда следует конкретное правило: до исправления спецификации сохранять и сертифицировать кандидата, который показывает её слабое место. Если сразу использовать его только как очередную ошибку для исправления, можно потерять сам пример, указывающий на пропущенное требование.
Выбор по ситуации
- Выбирайте Phase, если нужен полный контур: сначала независимый поиск, затем отдельная сертификация и работа над контрактом. В описанной постановке эта схема сочетает сопоставимый с no-feedback discovery выход свидетелей и более высокий приведённый результат исправления относительно IS-Revised.
- Выбирайте Direct, если нужен этап самостоятельных попыток без корректирующих подсказок и вы готовы организовать последующую проверку отдельно. Не трактуйте 59,0% как опубликованную отдельную оценку Direct: показатель относится к no-feedback discovery в целом.
- Выбирайте IntentShield, если основная цель — итеративно использовать сообщения компилятора, верификатора и видимых тестов для поиска следующего решения, а не максимизировать обнаружение свидетелей неполноты в описанной постановке.
Итак, для аудита полноты в изученном Verus/Rust-процессе наиболее обоснованный выбор — Phase: он отделяет обнаружение от исправления и сохраняет кандидатов для сертификации. Direct уместен как отдельная политика поиска, IntentShield — когда важнее корректирующий цикл. Это выбор по цели процесса и данным одного исследования, а не универсальный рейтинг инструментов.
Ограничения результата и границы применимости
Результаты представлены в одном препринте, принятом, согласно его тексту, на воркшоп NeurIPS 2026. В доступном описании фигурируют 12 задач Verus/Rust и четыре семейства моделей; независимая промышленная валидация не приведена. Авторы также указывают, что эффект не воспроизвёлся в доступных оценках Dafny и Lean. Поэтому проценты и рекомендация относятся к изученной постановке и не подтверждают преимущество той же схемы в любом языке, проекте или наборе тестов.
