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