Команда сети Ethereum опубликовала гостевую серию постов от ведущего разработчика Vyper под псевдонимом big_tech_sux, посвященную роли формальной верификации в эпоху стремительного развития искусственного интеллекта.
Автор утверждает, что прогресс LLM делает математическое доказательство корректности программ более доступным, а для смартконтрактов, которые управляют миллиардами долларов, формальная верификация постепенно становится необходимостью.
ИИ меняет подход к проверке программного обеспечения
В серии постов объясняется, что формальная верификация — это математический метод, который позволяет доказать правильность работы программы для всех возможных сценариев выполнения, а не только тех, что охвачены тестами.
В качестве примера автор привел функцию f(x) = x/2, для которой можно математически доказать, что результат никогда не превысит входное значение.
По его словам, такая методика способна находить чрезвычайно редкие ошибки, которые практически невозможно выявить обычным тестированием.
«Формальная верификация может выявить один случай из квадриллиона, который никогда не проявится во время тестирования, но именно он может привести к катастрофическому сбою», — отметил автор.
В то же время он признал, что до недавнего времени использование этого подхода требовало работы больших команд экспертов, которые создавали математические модели программ и проводили сложные доказательства.
По мнению разработчика, современные LLM существенно упрощают этот процесс по мере приближения к AGI.
Вместе с тем автор подчеркнул, что даже с помощью ИИ формальная верификация остается сложным и ресурсоемким процессом. В частности, преобразование программного кода в формальную модель может содержать неточности, которые влияют на достоверность результатов.
Развитие ИИ меняет баланс между атакой и защитой
В материале отмечается, что развитие искусственного интеллекта одновременно повышает эффективность как защитников, так и злоумышленников.
Автор напомнил о случае, когда еще не выпущенная модель OpenAI смогла найти уязвимости нулевого дня, которые позволяли обходить несколько уровней защиты.
На этом фоне формальная верификация, по словам автора, позволяет сместить преимущество в пользу защитников.
«Тогда как нападающим достаточно найти лишь одну последовательность входных данных для взлома системы, защитники могут использовать формальную верификацию, чтобы доказать ее устойчивость ко всем возможным входным данным», — подчеркнул он.
Именно поэтому для критически важного программного обеспечения, в частности смартконтрактов, которые управляют миллиардами долларов пользовательских средств, формальная верификация становится «не опцией, а необходимой предпосылкой».
Стоит отметить, что это продолжает дискуссию, которую ранее начал сооснователь Ethereum Виталик Бутерин относительно использования ИИ для формальной верификации кода.
end-content
