Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
SWE-Proof выявляет неверные исправления реальных ошибок, которые обычный набор тестов принимает за правильные. George Ma с соавторами обнаружили контрпримеры для каждого четвёртого — каждого второго прошедшего тесты патча, хотя препринт не рецензирован и все числа получили сами авторы. Значит, рейтинг агента по SWE-bench ещё не показывает, насколько безопасно доверять ему изменение репозитория.
Как патч превращают в проверяемое утверждение
Обычный тест подтверждает поведение программы только на выбранных входных данных. Формальная верификация проверяет другое: выполняет ли реализация точную спецификацию на всей области входов, которую эта спецификация описывает.
SWE-Proof построен из всех 500 задач SWE-bench Verified. Для каждой задачи Benchproofer создаёт формальную спецификацию исправленного поведения, реализацию на языке системы проверки и доказательство её соответствия спецификации. Предыдущая, ошибочная реализация при этом должна проверку провалить.
Большой репозиторий нельзя целиком перенести в средство доказательства. Поэтому Benchproofer моделирует только новый или изменённый код, а вызовы неизменённых функций заменяет аксиомами — допущениями об их поведении. Доказательство действует при условии, что эти допущения верны.
Аксиомы проверяют на сгенерированных входах и пытаются опровергнуть контрпримерами. Отдельные проверки ищут слишком слабую спецификацию, при которой проходит неверная реализация, и слишком строгую, которой не соответствует правильный код. Также система сверяет модель исправления с настоящим патчем в репозитории.
В наборе используются три системы: Nagini для Python с контрактами, Velvet для доказательств через Lean и непосредственно Lean. В последнем случае агент пишет доказательство, а ядро Lean проверяет его; в остальных случаях обязательства в основном решает автоматический доказатель.
Правильная спецификация помогает, автоматически написанная — нет
Если Claude Opus 4.8 получал готовую формальную спецификацию, доля решённых задач росла с 85% до 95%. Для GPT-5.5 результат увеличивался с 81% до 95%. Спецификация давала агенту одновременно точный критерий правильности и дополнительную информацию о том, какое поведение требуется изменить.
Когда модель должна была сама сформулировать спецификацию, преимущества исчезали: итог не становился лучше работы без формальной проверки. Аудит выдержали лишь 62% созданных моделями спецификаций.
Главная ошибка — неполное соответствие исходной задаче. Такая спецификация точно ограничивает одну часть поведения, но оставляет другую свободной. Агент после этого может доказать корректность патча относительно собственного, урезанного утверждения, хотя ошибка в репозитории остаётся.
Структурированные требования на естественном языке проблему тоже не закрыли. Они делают задачу понятнее, но не позволяют механически проверить все допустимые входы. Формат документа здесь менее важен, чем полнота зафиксированного поведения.
Это меняет смысл результата агента. Прошедший тесты патч означает, что известные примеры не нашли ошибку. Патч с проверенным доказательством означает больше, но только если спецификация верно передаёт задачу, аксиомы соответствуют вызываемым функциям, а проверяемая реализация эквивалентна изменению в репозитории.
Что менять в планах разработки
Работа меняет прежде всего план оценки агентов. Скрытые тесты стоит считать первым фильтром, а не окончательным вердиктом: поверх них нужен независимый поиск контрпримеров или проверка по явному контракту. Иначе команда сравнивает способность агентов пройти конкретный набор примеров, а не исправить класс ошибочных состояний.
Переводить весь продукт на Lean из этого результата не следует. Узкое место находится раньше доказательства: кто-то должен точно выразить требуемое поведение. Если агент пишет спецификацию сам и затем сам по ней проверяет код, общий источник ошибки сохраняется.
Практический сценарий лучше выглядит для критичных функций, где контракт уже существует или его стоимость оправданна: расчётов, преобразований данных, правил доступа и переходов между состояниями. Формальная проверка тогда может стать дополнительным барьером после тестов. Для расплывчатой продуктовой задачи сначала потребуется отдельный контур подготовки и аудита спецификации.
Границы вывода задаёт сама оценка: Claude Opus 4.8 и GPT-5.5 решали задачи из Python-репозиториев SWE-bench Verified, а доказательства строились с известным правильным патчем при подготовке эталона. Benchproofer также применили к Python-части SWE-bench Pro, но приведённые основные результаты относятся к SWE-bench Verified. Это проверка подхода к оценке агентов, а не готовая замена испытаниям и ревью в произвольном стеке.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
