Разработчики программного обеспечения всё чаще используют искусственный интеллект для формальной верификации кода — математической проверки того, соответствует ли программа заданным требованиям. Такой подход уже применяют в проектах с открытым исходным кодом, а некоторые компании рассматривают возможность покупать у крупных лабораторий искусственного интеллекта проверенный код, созданный нейросетями. Об этом сообщает Wired.
В начале года специалисты по безопасности Apple заявили, что формальная проверка выявила в библиотеке шифрования corecrypto проблемы, которые, вероятно, невозможно было обнаружить другим способом. При этом компания вынуждена осторожно добавлять в библиотеку новые фрагменты кода, чтобы успевать проводить их проверку. Два руководителя подразделений кибербезопасности крупных компаний, пока не использующих формальную верификацию, признались, что ещё не уверены в экономической целесообразности автоматизации.
Интерес к технологии растёт и среди создателей открытого программного обеспечения. Некоммерческий Beneficial AI Foundation при поддержке гранта Anthropic в этом году проверил тот же код шифрования, который ранее изучал Стэнфордский университет. Майкл Розенберг, сопровождающий библиотеку curve25519-dalek, рассчитывает на появление устойчивого финансирования таких работ, однако не видит понятной модели его организации. «Я понятия не имею, как это произойдет, и мы определенно не должны полагаться на добрую волю компаний, занимающихся ИИ», — сказал он.
Стартапы, развивающие инструменты верификации, пока выбирают между прямыми продажами клиентам и сотрудничеством с посредниками, включая Anthropic. Их общий замысел заключается в том, чтобы поручить искусственному интеллекту значительную часть подготовки описания поведения программы. Например, спецификация таблицы может требовать, чтобы после сортировки в ней сохранялись те же элементы, хотя их порядок менялся.
Затем специальные средства, не обязательно основанные на искусственном интеллекте, переводят такое описание в формат, пригодный для математических систем Lean, Rocq и Isabelle. Эти инструменты проверяют, выполняет ли программа заявленные требования. Одним из новых участников рынка стал Мадан Мусуватхи, более 20 лет работавший в Microsoft Research, а затем основавший компанию Truidic.
После инцидентов, включая взлом Hugging Face, Мусуватхи решил ускорить коммерческое применение своих исследований. «ИИ в руках злоумышленников может быть чрезвычайно мощным», — заявил он, добавив, что верификация способна «сделать ИИ безопасным и защищенным для всех и везде». Компания Proofcraft, давно занимающаяся традиционной проверкой программ, сообщает о резком росте числа обращений, однако её руководители Джун Андроник и Гервайн Кляйн считают, что спрос уже превышает возможности самой компании и её конкурентов.
Специалисты Proofcraft одновременно опасаются, что автоматически созданные спецификации могут привести к «неоправданному доверию» к результатам проверки. При этом они хотят сохранить творческую сторону своей профессии: Кляйн сравнивает её с увлекательной головоломкой и говорит, что такая работа «довольно addictive, как игра-головоломка».