AI-агент доказал, что ваш код работает. Но можно ли ему верить?Борис Черный
рассказал в Xвиттере, как проверял Claude Agent SDK с помощью Lean. Всего несколько промптов привели к 16 PR с исправлениями багов. Риторический вопрос Бориса в посте: формальная проверка — будущее разработки? Но я бы сформулировал вопрос по-другому: можно ли верить формальной проверке, которую провел агент?
Для начала разберёмся, что именно проверяется и какВо-первых, Lean. Это язык программирования и помощник для доказательств, который моделирует что-либо, чтобы проверить утверждения о логике программы. Например: "Рассчитанная выплата никогда не превышает доступный остаток". Агент записывает функцию и доказательство на Lean, а движок Lean проверяет его
для всех допустимых входов, а не для нескольких примеров из тестов.
Во-вторых, Борис также упоминает TLA+ — он проверяет поведение системы во времени. Например, два воркера (проще говоря — параллельно работающих процесса) одновременно забирают задачу в работу. Агент описывает на TLA+ их возможные шаги, а движок (TLC)
перебирает порядки событий. И может так найти проблемы, как например, что будет, если оба прочитали статус до того, как один из них записал новый?
Звучит как мечта: попросил агента "докажи, что все ок" — и спишь спокойно ☕️ Но есть нюанс...
После получения "магического промпта" процесс под капотом выглядит так: агент интерпретирует программу, свою интерпретацию логики программы он пишет в виде модели на Lean или TLA+, а движки уже далее проверяют
эту модель (а не исходный код!). И если при переводе агент забыл или неправильно считал условие, неверно понял транзакцию или поведение внешнего API, можно получить безупречное доказательство просто не той программы 🤡.
И вся беда в том, что откровенно говоря, процесс перевода автоматически полностью валидировать никак нельзя. Вот и получается, что процесс, который призван проверять ошибки за глючащими LLM — сам подвержен этим самым глюкам.
Получается Lean и TLA+ — фигня?Нет. Как любил говорить мой преподаватель в универе — в математике важна "жесткость конструкции". Для проверки жесткости нужно довести написанные программы до предела, растянуть их сразу во все стороны, найти все edge-кейсы. И по задумке вообще-то это должны делать хорошие юнит-тесты. Но мы все знаем, как LLM пишет тесты: 100500 тестов, из которых 2 реально полезных, 100496 ничего не тестирующая мешура и 2 теста агент решил пропустить, потому что они не работали 😁
Поэтому Lean и TLA+ — это те самые инструменты, которые позволяют писать реально качественные тесты.
Но что делать с бедой, что LLM может просто потерять или неправильно перевести часть программы на языки Lean и TLA+ для проверок?
Хоть 100% гарантии нет, все-таки можно существенно увеличить шансы корректного перевода из кода в модель. Для этого нужно явно тянуть "красные нити" через всю разработку.
Допустим, в BRD есть бизнес-требование: "Одна заявка не должна приводить к двум выплатам". Это наша красная нить. Дальше мы начинаем ее тянуть. Сначала в TRD — там она обрастает сценариями: что делать, если два воркера, поведение при повторном запросе и тд. Далее тянем ее в архитектуру программы — архитектор выбирает механизмы реализации и защиты написанного в TRD. И наконец на последнем этапе все это реализуется в коде программы. То есть вся разработка строится вокруг красной нити, тянущейся из самого начала — из бизнес-требований.
И если разработка выстроена вдоль этих требований — то жесткий каркас вашей программы становится однозначным и детальным.
Дальше дело техники из двух частейПервая. Эти же "красные нити" становятся опорой для агента для перевода программы в модели Lean и TLA+. На нашем примере TLA+ проверяет, возможны ли две выплаты при разных порядках событий; Lean проверяет отдельные правила расчёта; тесты воспроизводят найденные сценарии на реальном коде. У каждого шага есть ссылка на исходное требование. В таком сеттинге агенту крайне сложно потерять какое-то важное условие, тк это станет видно на каждом этапе анализа проекта.
Вторая. Отдельно нужен набор проверок того, насколько построенная в Lean и TLA+ модель реально отражает проверяемый код. Иначе это останется слепой зоной, где вы теряете весь контроль над всеми остальными тестами. В этих проверках сравниваются результаты работы кода программы и построенной модели программы на одинаковых входных данных.
Отвечаем ЧерномуТак что ответ на риторический вопрос Бориса Черного — конечно, да, формальная проверка станет частью агентной разработки, потому что она круто укрепляет слабое место современной агентной разработки — тестирование.
Но, чтобы реально доверять "зеленой галочке" об успешно прохождение Lean и TLA+ тестов, необходимо выстраивать прослеживаемую цепочку через всю разработку:
|→ BRD (задается людьми)
|→ TRD (валидируется людьми)
|→ Архитектура (верхнеуровнево валидируется людьми)
|→ Реализация в коде (выполняется агентами и как раз нуждается в проверке)
|→ Lean / TLA+ модели (пишется агентами)
|——> Проверка на соответствие логики модели закладываемым требованиям (осуществляется агентами)
|——> Проверка на соответствие логики модели логике проверяемого кода (осуществляется агентами)
|→ воспроизведение ошибок, найденных во время тестирования модели, на реальном коде (осуществляется агентами)
Может звучит сложно, но это новый образ качественной разработки. Ведь в условиях, когда писать код руками нам с вами уже не нужно — проработка каждого из этих этапов — и есть наша основная работа.
#ИИученьесвет
Заместители
