ИИ не отменит верификацию: почему «почти правильный» код опаснее, чем кажется

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

Авторы статьи анализируют инциденты, связанные с ИИ, и напоминают: «почти корректные» компоненты в сумме дают ненадёжные системы. Они провели эксперимент — создали формально верифицированную систему управления конференциями с помощью ИИ-ассистента и среды AutoProof для языка Eiffel.

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