Насколько хорошо агенты используют методы тестирования и верификации?

Введение

Ранее отмечалось, что хотя проще чем когда-либо добиться определённого уровня качества благодаря тому, что агенты умеют использовать эффективные методы тестирования, качество ПО, похоже, становится хуже. Это указывает на то, что используемые разработчиками по умолчанию подходы, вероятно, не очень эффективны. Здесь мы проверяем, улучшают ли простые инструкции агентам о применении конкретных техник или библиотек правильность реализации — своего рода тест того, насколько эффективны агенты при наведении кем-то без экспертизы в тестировании, кто, может быть, слышал, что следует применять определённые методы или использовать определённые библиотеки.

Мы переиспользуем оценку реализации Zstd, обсуждавшуюся в этом сравнении эффективности agentic-программирования на разных языках, и вместо этого сравниваем различные техники тестирования и библиотеки тестирования, когда агентам даётся подсказка реализовать Zstd с различными добавлениями, такими как «Используй разработку, управляемую тестами», «Используй Lean 4», «Используй QuickCheck», «Используй property-based-тестирование» и так далее. Я также запустил несколько других оценок, например на RFC IMAP, которые вкратце обсуждаются.

Методология

Все реализации были на Rust. Тестировалось 26 условий подсказки: ACL2, Alloy, «Audit and fuzz risky areas», «Audit first», Creusot, Default (без дополнительных инструкций), Differential testing, Fuzzing, Hegel, Insta, Judgement (агенты просили использовать лучшую технику), Kani, Lean 4, «Make no mistakes», Metamorphic testing, Mutation testing, Property-based testing, Proptest, QuickCheck, rstest, встроенный фреймворк тестирования Rust, SMT-решатели (с Z3, cvc5 и Yices, все доступные), Spin, TDD, TLA+ и Verus. Дополнительно тестировались 4 навыка: Hegel с официальным навыком Hegel, навык Rust test от ECC (ECC — это сборка навыков с 250k звёзд на GitHub и 38k форков), навык property-based-тестирования от Trail of Bits, и навык для тестирования, который я написал сам (я реакционер, который использует подсказки вместо навыков и не чувствую, как писать хороший навык). Кроме моего навыка, навыки были выбраны потому, что это были главные результаты, когда я просил найти релевантные навыки.

Предварительные прогнозы

Заранее зарегистрировано несколько предположений о том, как будут показывать себя условия:

• TDD будет показывать худшие результаты (55% уверенности)
  • TDD была добавлена специально потому, что я думал, что она покажет худшие результаты
  • Уверенность невысока, так как неизвестно, что будут делать агенты, когда им дана инструкция использовать TDD
• Формальные методы не будут показывать лучшие результаты (52% уверенности)
  • Предположение в том, что формальные методы эффективны и полезны, хорошие методы тестирования тоже эффективны и полезны, а на простых задачах формальные методы не должны превосходить при использовании на одном уровне компетентности
• «Make no mistakes» не будет показывать лучшие результаты, чем без инструкций (95% уверенности)
  • Это шутка, которую многие пробовали. Если бы это работало, люди бы, конечно, заметили?
• Навык ECC (с 250k звёзд и 38k форков) не будет показывать лучшие результаты (65% уверенности)
• Навык Hegel не будет показывать лучшие результаты (65% уверенности)
• Навык Trail of Bits не будет показывать лучшие результаты (55% уверенности)

Общие результаты

Ниже приведен очень беспорядочный график, показывающий результаты для протестированных условий (Codex с GPT-5.6 Sol, с средним и высоким уровнями усилий). На оси X — стоимость, на оси Y — доля запусков, которые прошли 100% тестов, среднее по 80 запускам из каждого условия и уровня усилий.

Одно, что можно видеть — ничего не показывает существенно лучших результатов. Однако Default (без дополнительных инструкций) показал выше среднего. На высоком уровне усилий в среднем fuzzing и связанные с property-based-тестированием условия показали немного лучше, чем формальные методы, ситуация была намного более смешанной на среднем уровне. Рекомендованные codex навыки для тестирования показали худшие результаты, хотя наш быстрый пользовательский навык показал хорошо. TDD не показал хороших результатов, как и предсказывалось.

Если действительно посмотреть, что делали агенты, быстро становится очевидно, что в целом агенты не знают, как хорошо использовать эти инструменты или техники. Как мы отметили здесь, и как отметил каждый, с кем я разговаривал, агенты действительно плохо тестируют и, похоже, не понимают, как разумно тестировать «по умолчанию». Например, вот комментарий Gary Bernhardt:

Подход AI-агентов к тестированию, более или менее:

1. Взять патологические случаи, придуманные кем-то, возражавшим против мокирования 15 лет назад, без когда-либо реального использования мокирования. Наивные мечты об чрезмерном мокировании.
2. Сделать эти патологии основой вашей стратегии тестирования.

Оказывается, если попросить агентов использовать конкретную технику тестирования или библиотеку для тестирования, такой подход не меняется столько, сколько хотелось бы. Агенты либо просто пишут тесты, которые они обычно писали бы, но внутри фреймворка для другого типа техники тестирования, либо используют технику поверхностно, но не делают вещи, которые дают ценность этой технике.

Verus

Verus использует SMT-решатель и различные типы рассуждений для доказательства того, что код соответствует спецификациям.

Хотя Verus может доказать, что код соответствует спецификациям, агенты этого не делали. Вместо этого они делали доказательства о различных абстрактных свойствах, связанных с Zstd. Сам я с таким инструментом не работал, поэтому не могу говорить о том, что обычно делает эксперт или даже новичок, но из прочтения туториала мне кажется немного странным, что агенты не пытались использовать Verus для верификации какого-либо реального кода и использовали его только для абстрактных рассуждений.

Когда агент полагается на Verus, результаты совпадают со средними, но средние по себе не особенно хороши.

Alloy

Alloy часто называют model checker'ом bounded. Может быть, это не совсем правильно для Alloy 6, так как он вводит некоторые дополнительные функции, но это далеко вне моей области экспертизы. Мое понимание в том, что обычно с Alloy вы доказываете свойства вашей модели (в отличие от доказывания того, что ваш код работает).

Alloy получил второй худший балл правильности и, необычно, показал низкие результаты как на среднем, так и на высоком уровне. Как и в случае с Verus, агенты, используя Alloy, полагались на стандартный Rust тест и в основном возились с Alloy. Использование формального инструмента плохо не помогло с правильностью.

Дифференциальное тестирование

Дифференциальное тестирование — это техника, где вы даёте одни и те же входные данные нескольким реализациям и затем сравниваете результаты для поиска проблем. В принципе, это кажется разумным для попытки с LLM'ами, так как мы часто получаем разные результаты от разных случайных попыток.

Но это дало нам третьи худшие результаты. Ни один из агентов не создал две полные реализации для сравнения. Из 160 запусков 135 сделали что-то, что можно было бы назвать дифференциальным тестированием, но, как и в других условиях, которые мы видели, они были в основном тривиальны и фактически бесполезны.

Lean 4

Lean 4 может быть описан как интерактивный theorem prover.

Как и в других формальных условиях, агенты, используя Lean, полагались тяжело на стандартные тесты Rust. Как и в других формальных условиях, доказательство нескольких вещей, которые не имеют значения, не помогло с правильностью.

QuickCheck

QuickCheck — это библиотека для property-based-тестирования, вероятно, самая известная такая библиотека в течение долгого времени, хотя Hypothesis может сейчас занимать эту корону.

К сожалению, агенты были примерно столь же эффективны при использовании property-based-тестирования, как и при использовании формальных инструментов, которые мы видели до сих пор. Используя QuickCheck, агенты писали в основном очень простые «smoke tests», которые не много проверяли. Они также использовали случайные входные данные, которые, когда полностью случайны, довольно плохие для тестирования чего-то вроде Zstd.

TDD

TDD показала худшие результаты здесь, а также в оценке IMAP RFC.

Подсказка TDD, казалось, вызвала большие изменения в поведении агента. Агенты создали в два раза больше тестов и работали в гораздо более итеративном рабочем процессе test-code-test-code и так далее, хотя сторонник TDD, вероятно, сказал бы, что агенты на самом деле не использовали TDD. Были только несколько примеров агентов, делающих какой-то fine-grained итеративный TDD.

В целом, агенты писали больше тестов в начале; например, агенты имели один или более неудачных тестов в 67 из 160 случаев перед существенной реализацией, в сравнении с 0 из 160 для условия Default.

Spin

Spin — это model checker.

Теперь мы входим в диапазон, где результаты были близки к средним. Spin показал умеренно хуже чем средний на обоих уровнях усилий, при ниже средней стоимости. Как и в других формальных инструментах, использование Spin было в основном неэффективным.

Hegel

Hegel — это библиотека для property-based-тестирования на основе Hypothesis.

Как можно ожидать на данный момент, агенты не использовали Hegel эффективно. В той мере, в которой они её использовали, они использовали её поверхностно, и они в целом использовали её после того, как тяжело полагались на обычное тестирование.

Fuzzing

Fuzzing включает случайное варьирование тестовых входных данных каким-либо образом.

Агенты полагались на отправку случайных байтов, что в основном приводило к прохождению одних и тех же кодовых путей (недействительные входные данные). На редких случаях, когда агенты генерировали случайные структурированные входные данные (10 из 160 случаев), это находило настоящие баги половину времени, некоторые из которых были нетривиальными случаями. Использование fuzzing немного эффективно в 5 из 160 случаев — это не совсем хорошо, но это было одним из более эффективных использований техники, которое мы видели до сих пор.

Snapshot-тестирование (Insta)

Insta — это библиотека для snapshot-тестирования (иногда называемого golden-тестированием), где вы сравниваете результаты с «снимком» или «золотым файлом» правильных результатов.

Как вы можете ожидать, snapshot-тестирование едва использовалось и агенты в основном полагались на традиционные тесты.

SMT-решатели

Агентам была дана инструкция использовать SMT-решатель, с установленными Z3, cvc5 и Yices.

Агенты в основном использовали SMT-решатель как своего рода черновик для вычисления вещей, таких как диапазоны состояний FSE, арифметика заголовков и так далее. Даже когда агенты моделировали что-то, они в целом не моделировали правильную вещь, чтобы избежать частой ошибки.

TLA+

TLA+ — это язык и инструмент для моделирования поведений.

Мы входим в набор выше средних результатов (но всё ещё хуже, чем Default), но, как отмечалось выше, я не буду делать сильные выводы из фактического упорядочивания. Хотя это не обязательно значительно, TLA+ показала немного выше среднего на среднем уровне и более выше среднего на высоком уровне.

Метаморфное тестирование

При метаморфном тестировании мы проверяем, что связанные входные данные производят выходные данные с ожидаемым соотношением. Например, вы можете проверить, что для функции сортировки изменение порядка неравных входных данных не меняет порядок выходных данных.

Как мы видели для других условий, метаморфное тестирование не выполнялось очень полезно в отношении правильности. Некоторые действительно разумные свойства были проверены, но они не попали в области, в которых агенты часто ошибались, поэтому проверка этих свойств не помогла.

Kani

Kani — это библиотека для model checking на Rust.

С точки зрения «действительного использования формального метода на коде, который будет выполняться», Kani имела лучшее покрытие в том, что Kani действительно использовалась на коде Zstd. Однако это происходило только иногда, и большинство использования было поверхностным.

Был один случай, когда реальное использование Kani поймало нетривиальный баг, который привел к изменению кода Rust. 1 из 160 — это не впечатляет, но это указывает на то, что агенты могут иногда наткнуться на разумное использование Kani (что, как я предполагаю, означает, что, если используется в окружении RL, модели могли бы научиться использовать Kani более эффективно).

ACL2

ACL2 — это theorem prover. Одна вещь, на которую следует обратить внимание в результате здесь — в многих случаях ACL2 испытала OOM (лимит 192 GiB). Результаты OOM не были подсчитаны, что смещает результаты в некотором неясном способе.

Хотя ACL2 показала выше Default, было бы удивительно, если бы это было каузально и значительно. Как мы видели почти со всеми другими формальными методами, ACL2 в основном использовалась для доказывания вещей, которые не значительно повлияли на правильность.

Proptest

Proptest — это библиотека для property-based-тестирования.

Так же, как и в случае с другим рандомизированным тестированием, большинство тестов не были очень интересны, и чрезмерная зависимость от случайности вызвала плохое покрытие.

Несмотря на в целом плохое использование property-based-тестирования, shrinking'и proptest'а (нахождение более простого входа, который вызывает отказ теста) иногда давали некоторое значение, что лучше, чем мало или никакой ценности, которую мы видели в большинстве других случаев.

Default (без инструкций)

Default дал агенту никаких инструкций по тестированию или верификации.

Учитывая то, что мы видели до сих пор, неудивительно, что Default показал выше среднего. Агенты в целом делали вещи, которые не были полезны, когда их просили использовать конкретные библиотеки или конкретные техники тестирования. Разумно, что не говорить агентам делать вещи, которые заставят их делать бесполезную работу, лучше, чем говорить им делать вещи, которые заставят их делать бесполезную работу.

Аудит кода

Audit просила агентов аудировать код после реализации. 152/160 агентов действительно сделали это и 151 агент заявили найти проблему и затем сделали изменение в результате аудита. Агенты в целом выбирали разумные области для аудита, но обычно не делали независимого аудита с свежим контекстом.

42 использовали независимого агента, но эти запуски в действительности показали худшие результаты. Аудит закончился с лучшей правильностью на высоком уровне, но ниже средней правильностью на среднем уровне, и все этот аудит существенно увеличил стоимость.

Аудит и фаззинг рискованных областей

Для Zstd, когда эта инструкция была следована, это заставило агентов сосредоточиться тяжело на FSE, Huffman, bit readers и состояниях. Это были области, где в целом агенты часто пропускали проблемы, поэтому агенты были правы в мысли, что эти области были рискованны. Области, которые были нацелены на фаззинг, были лучшим выбором, чем простое условие Fuzzing.

Make no mistakes

Хотя это технически показало выше Default, поведение, похоже, не было существенно отличным и баллы очень близки; я предполагаю, что это из-за случайного варьирования.

Пользовательский навык для тестирования

Здесь Skill относится к навыку, который я написал для тестирования простого навыка (в отличие от больших/сложных навыков, которые были тем, что я нашел, когда я просил агента найти релевантные навыки для тестирования).

Может быть, я должен использовать навыки, но я обычно не использую и вместо этого полагаюсь на подсказки. Результат был лучшей правильностью, но не функционировал так, как предполагалось. Агенты часто не делали то, что требовалось (например, fresh context), хотя они иногда писали более значимые тесты, чем при других условиях.

Общие замечания

Как мы отметили выше, я не пытался разбить данные в красивый, простой для просмотра способ. Я не сделал это потому, что, когда мы посмотрели, что агенты действительно делали, кажется, что они были в основном не очень эффективны, и я не думаю, что это особенно интересно видеть, как хорошо «агенты, используя Verus плохо» делают в сравнении с «агенты, используя QuickCheck плохо».

Одна вещь, которую я нахожу немного интересной — когда просили идентифицировать области, которые являются рискованными или подвержены тонким багам, агенты смогли это сделать. Но в целом, независимо от предложенной библиотеки или техники, агенты не смогли использовать технику. Как ранее обсуждалось, просто просить агентов «тестировать» или повторно просить их тестировать больше результатов в плохом тестировании. Оказывается, что просить их использовать техники тестирования (некоторые из которых я лично нашел быть высокоэффективными) также результатов в плохом тестировании.

Как заставить агентов писать хорошие тесты?

Мой опыт был, если вы направляете агентов установить разумную структуру тестирования и триажа, получить агентов добавить к этому эффективно без огромного количества надзора работает ok-ish. Из-за моего фона (смещение), тип тестирования, которое я стремлюсь использовать, это какая-то форма случайного тестирования / фаззинга / property-based-тестирования.

Я разговаривал с Jamie Brandon об этом, и он нашел то же самое с snapshot-тестированием. Он упомянул, что на одном проекте, когда он просил агентов (используя различные модели) делать snapshot-тестирование, они говорили, что они это делают и затем просто не делали это (они писали unit-тест и затем говорили, что написали snapshot-тест).

Точность предсказания

• TDD underperforms (55% confidence) — True
• Formal methods do not outperform (52% confidence) — True, но не по причине, которую я ожидал. Агенты не смогли использовать их эффективно вообще, поэтому конечно они не могли превосходить
• Make no mistakes doesn't outperform no instructions (95% confidence) — True; превзошла большинство условий потому, что no-op лучше, чем заставить агентов делать неэффективные вещи
• ECC skill will not outperform — True
• Hegel skill will not outperform — True
• ToB skill will not outperform — True

О навыках

Я не знаю достаточно о навыках, чтобы говорить, как писать хороший навык, но со всеми навыками, которые мы посмотрели в этом посте (кроме того, что я написал за минуту или две), навыки казались написанными как человеческие инструкции туториала. Мое наивное предположение как человека, который написал ровно один навык, в том, что я предполагаю, что это не оптимально при работе с моделью, которая уже должна иметь какое-то знание темы.

Модель уже будет иметь какое-то распределение поведения по умолчанию, поэтому я чувствую, что более естественная вещь — это дать утверждения, которые будут изменять это поведение, не писать инструкции, которые позволяли бы человеку или неведающему агенту делать поведение вообще.

Поскольку у нас получаются различные поведения по умолчанию от различных harnesses, моделей и уровней усилий, просто бросание большого количества текста в подсказку или навык не на самом деле изменяет это; это просто более долгий способ отталкивать агента от его по умолчанию, с большим количеством текста, который может делать какой-то непреднамеренный отталкивание.

Заключение

Кажется, что ключ к тому, чтобы заставить агентов писать хорошие тесты, — это не просто назвать технику или библиотеку, которую использовать, и предположить, что агенты знают, как её использовать. Вместо этого требуется установить разумную структуру тестирования, направить агентов к конкретным областям и итеративно уточнять результаты.

На данный момент, без направления эксперта по тестированию, агенты плохо используют даже хорошо известные техники и библиотеки. Это указывает на то, что либо агентам нужна лучшая подготовка по тестированию во время обучения, либо нам нужны лучшие способы направления их во время выполнения кода.