Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
SpecGuard научили до запуска агента разработки находить задачи, где описание и тесты требуют несовместимого поведения. В препринте Param Biyani и Krishnamurthy Dvijotham, который не прошёл рецензирование и содержит замеры самих авторов, инструмент обнаружил до 72,8% конфликтов в SWE-bench и подтвердил 51,1% формальным доказательством. Такую проверку можно поставить перед выдачей задачи агенту, чтобы противоречивый тест не подтолкнул его править саму проверку или вшивать ожидаемый ответ.
SpecGuard разделяет интерпретацию требований и тестов. Первый агент получает описание и кодовую базу, но не видит тесты, и переводит ожидаемое поведение в исполняемую спецификацию Lean 4. Второй независимо формализует тестовые сценарии, а третий связывает обе записи; затем ядро Lean проверяет, может ли какая-либо реализация удовлетворить им одновременно.
Если требования несовместимы, система выпускает сертификат, который можно перепроверить без доверия к создавшей его модели. Когда доказательство собрать не удаётся, SpecGuard либо показывает расхождение при исполнении спецификации, либо возвращает неопределённый результат — он не считается разрешением запускать агента.
С GPT-5.6 Sol доля пропущенных конфликтов составила 8,1% против 39,8% у модели-оценщика, которая читала задачу и тесты и выносила вердикт без проверяемого артефакта. На естественных конфликтах из GitHub SpecGuard выдал девять вердиктов для 22 задач, восемь из них подкрепил сертификатами Lean.
Основной замер проводили на искусственно испорченных задачах SWE-bench; дополнительный — на LiveCodeBench и конфликтах из реальных репозиториев. Метод рассчитан на требования, которые можно выразить через входные и выходные значения. Доказательство подтверждает несовместимость формальных записей, но не гарантирует, что они точно передают исходный текст: ручная проверка признала верными 52 из 60 изученных сертификатов.
Источники
Иллюстрация: рисунок из статьи «SpecGuard: Proving a Task Is Broken Before the Agent Cheats», Param Biyani, Krishnamurthy Dvijotham, CC BY 4.0
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
