Математика, которая может спасти вайб-кодинг от самого себя, хоть и требует возни

Десятилетиями разработчики пытались с помощью математики доказывать, что в программном обеспечении нет ошибок. Это долгий и трудоёмкий процесс: инженерам нужно точно описать, как программа должна работать, а затем представить её код в виде формул, пригодных для проверки. Компании уже проводят сложные тесты, чтобы найти как можно больше дефектов, но редко тратятся на формальную верификацию, которая способна выявить и более необычное поведение.

Теперь несколько стартапов надеются, что генеративный ИИ превратит формальную проверку программ в практичный и необходимый инструмент. Среди них — &Truth: Сун присоединилась к компании в августе, а публично её запустили в четверг. В своей работе исследовательница показала возможности технологии, применив ИИ для проверки части кода, которая шифрует переписку в мессенджере Signal.

Главный научный сотрудник &Truth Илья Сергей сравнил проверку кода с расчётами при строительстве мостов и зданий. По его словам, математические методы для анализа программ существовали давно, но их было трудно масштабировать.

&Truth привлекла от инвесторов 70 миллионов долларов и рассчитывает со временем проверять программы на любом языке. Её конкурент Harmonic, основанный в том числе генеральным директором Robinhood Владом Теневым, получил 295 миллионов долларов. На этой неделе компания сообщила, что её ориентированный на математику ИИ-агент Aristotle умеет проверять программы на C и аппаратные проекты на Verilog. Harmonic испытывает технологию с потенциальными клиентами, среди которых производители чипов Tensordyne и Nvidia. Венчурное подразделение Nvidia также вложилось в стартап.

Неделей ранее Anthropic и стартап Theorem объявили, что с помощью ИИ нашли ошибки в программном обеспечении с открытым исходным кодом, которые не выявили триллионы тестов. Они также представили дополнение для Claude, призванное помогать другим разработчикам с верификацией. Стоимость первоначального проекта не раскрыли.

Формальная верификация обещает сделать программы надёжнее и снизить риски для безопасности. Но пока неясно, сможет ли ИИ вывести её за пределы наиболее критичных систем — например, в организациях вроде NASA и Apple — и сделать повсеместной.

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

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

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

Проверка критически важного кода

По данным компаний, формально проверенное программное обеспечение есть в самолётах Boeing, серверах Amazon и более чем 2,5 миллиарда активных устройств Apple. Обычно речь идёт о коде, связанном с безопасностью: его уязвимости при эксплуатации могут привести к серьёзному ущербу.

Байрон Кук, заслуженный научный сотрудник и вице-президент Amazon Web Services, говорит, что формальная верификация помогла снять опасения клиентов по поводу безопасности облачных сервисов. Она также ускорила работу внутренних команд: серьёзные ошибки удаётся устранять на ранних этапах.

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

Ранее в этом году команда безопасности Apple сообщила, что некоторые проблемы, найденные формальной верификацией в библиотеке шифрования «corecrypto», нельзя было обнаружить другими способами. При этом компания добавила, что должна осторожно добавлять в библиотеку новый код, чтобы успевать его проверять.

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

Разработчики проектов с открытым исходным кодом, на котором основана работа многих приложений, всё чаще пробуют проверять программы с помощью ИИ. Некоммерческий фонд Beneficial AI Foundation получил грант от Anthropic и в этом году проверил тот же код шифрования, который исследовала Сун в Стэнфорде. Майкл Розенберг, сопровождающий библиотеку curve25519-dalek, надеется, что появится устойчивое финансирование таких проверок. При этом, по его словам, он не знает, как этого добиться, и полагаться на добрую волю ИИ-компаний не стоит.

Некоторые стартапы, которые хотят расширить применение верификации, пока не решили, предлагать ли свои инструменты напрямую клиентам или работать через посредников, например Anthropic. Их общий план — поручить ИИ автоматизацию значительной части работы по описанию того, как должна вести себя программа. Так, спецификация таблицы данных может требовать, чтобы до и после сортировки в ней оставались те же элементы, менялся только их порядок. Затем код нужно преобразовать в формат, с которым умеют работать математические инструменты Lean, Rocq и Isabelle. Эта часть автоматизации может обходиться без ИИ.

Ещё один новый участник в области формальной верификации — Мадан Мусувати. После более чем 20 лет в Microsoft Research он ушёл оттуда и основал стартап Truidic. По его словам, после таких инцидентов, как взлом Hugging Face, совершённый OpenAI, он почувствовал острую необходимость вывести свои исследования на рынок. Мусувати считает, что ИИ в руках злоумышленников может быть чрезвычайно мощным, а верификация способна сделать его безопаснее для всех и повсюду.

Proofcraft — одна из немногих компаний, которые давно предлагают традиционную формальную верификацию. Там говорят, что растущий интерес к этому процессу привёл к наплыву запросов от потенциальных клиентов. Гендиректор Джун Андроник и главный научный сотрудник Гервин Кляйн отмечают, что спрос заметно превышает возможности их компании и конкурентов.

При этом Андроник и Кляйн опасаются, что спецификации, созданные ИИ, могут вызвать необоснованное доверие к результатам проверки. Специалисты по верификации также хотят сохранить удовольствие от своей работы: Кляйн сравнивает её с затягивающей игрой-головоломкой. Если всё пойдёт хорошо, решать такие задачи ему придётся ещё чаще.