Верификация программ в эпоху ИИ: почему галлюцинации делают проверку кода важнее

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

Почему ИИ не решает главного Программная инженерия — это не только написание кода.

Опросы индустрии показывают: разработчики тратят на непосредственное кодирование от 20 до 30% рабочего времени. Остальное уходит на сбор требований, проектирование архитектуры, ревью, тестирование и исправление ошибок. ИИ-ассистенты умеют генерировать функции и объяснять незнакомый код, но не умеют доказывать корректность системы в целом — это принципиально иная задача. Главная проблема — галлюцинации. ИИ уверенно предлагает код, который выглядит правдоподобно, компилируется и проходит базовые тесты, но содержит тонкую логическую ошибку. «Почти корректные» компоненты, сложенные вместе, формируют ненадёжную систему. Авторы собрали задокументированные инциденты с ИИ-сгенерированным кодом в production: от неверных юридических цитат в чат-ботах до ошибок в медицинских рекомендательных алгоритмах. Паттерн один: система работала корректно в большинстве случаев — пока не встретила граничный.

Эксперимент с

AutoProof и Eiffel Исследователи не ограничились теорией и провели конкретный эксперимент. Система управления конференциями была создана с помощью ИИ-ассистента в связке с AutoProof — формальным верификатором для языка Eiffel. Принципиальное отличие от тестирования: формальная верификация доказывает корректность для всех возможных входных данных, а не только для набора подобранных примеров.

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

Федерация агентов как новая парадигма

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

«Галлюцинация как вид отказа делает гарантии корректности более, а не менее важными», — утверждают авторы.

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

Что это значит Вывод авторов осторожно оптимистичен.

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