Команда сети Ethereum опубликовала гостевую серию постов от ведущего разработчика языка Vyper под псевдонимом big_tech_sux. Автор подробно рассмотрел критически важную роль формальной верификации в эпоху стремительного развития технологий искусственного интеллекта. Прогресс больших языковых моделей делает математическое доказательство корректности программ значительно более доступным для широкого круга специалистов. Для смарт-контрактов, управляющих миллиардами долларов пользовательских средств, формальная верификация постепенно становится абсолютной необходимостью. Данный математический метод позволяет доказать правильность работы программы для всех возможных сценариев выполнения. Это выгодно отличает подход от традиционного тестирования, охватывающего лишь заранее подготовленные случаи. Автор привел показательный пример с простой функцией деления на два, для которой математически доказывается невозможность превышения входного значения.

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

Разработчик напомнил о случае обнаружения уязвимостей нулевого дня еще не выпущенной моделью компании OpenAI. Найденные уязвимости позволяли успешно обходить сразу несколько уровней защиты сложных систем. Формальная верификация позволяет заметно сместить текущее преимущество в пользу защитников инфраструктуры. Нападающим достаточно найти лишь одну последовательность входных данных для успешного взлома системы. Защитники же могут использовать математические доказательства для подтверждения устойчивости ко всем возможным входным данным. Именно поэтому для критически важного программного обеспечения формальная верификация становится необходимой предпосылкой. Данная публикация продолжает важную дискуссию, начатую ранее сооснователем Ethereum Виталиком Бутериным. Основатель сети активно обсуждает перспективы использования искусственного интеллекта для формальной верификации кода.