ИИ-генерация кода не решает проблем верификации: эксперимент с AutoProof показал важность строгого процесса

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

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

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

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