Стартап &Truth привлёк $70 млн на ИИ-проверку кода математикой

Wired рассказывает, как малоизвестная область на стыке программирования и математики, формальная верификация, получает второе дыхание благодаря генеративному ИИ. Исследовательница Стэнфорда Чуюэ Сунь (Chuyue Sun) с коллегами разработала ИИ-инструмент, который выполнил инженерный проект меньше чем за полдня и меньше чем за $500. Трём высококвалифицированным специалистам на ту же работу вручную потребовалось пять месяцев. Об этом результате Сунь сообщила в недавней статье.

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

Теперь, по словам издания, волна стартапов ставит на то, что генеративный ИИ сделает такую проверку и практичной, и необходимой. Один из них, &Truth: Сунь присоединилась к нему в августе, а публично компания запустилась в четверг. Исследование Сунь показало потенциал технологии: ИИ проверил часть кода, который шифрует переписку в мессенджере Signal. Главный научный директор (chief science officer) &Truth Илья Сергей (Ilya Sergey) объясняет идею так: мосты и здания не рушатся, потому что люди посчитали математику до постройки, почему бы не сделать то же для кода? По его словам, технологии для математических рассуждений были давно, но их было трудно масштабировать.

&Truth привлекла $70 млн и хочет со временем верифицировать любой язык программирования. Конкурент Harmonic, сооснованный главой Robinhood Владом Тенёвым (Vlad Tenev) и получивший $295 млн финансирования, на этой неделе объявил, что его математический ИИ-агент Aristotle теперь поддерживает верификацию ПО на C и аппаратных схем на Verilog. Harmonic оценивает технологию с потенциальными пользователями, среди которых производители чипов Tensordyne и Nvidia; венчурное подразделение Nvidia, один из инвесторов стартапа. А на прошлой неделе Anthropic и стартап Theorem совместно объявили, что с помощью ИИ нашли ошибки в открытом ПО, которые не обнаружили триллионы тестов. Они же представили дополнение к Claude, помогающее другим разработчикам с верификацией. Затраты на первоначальный проект не раскрыты.

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

Главный вопрос, выйдет ли формальная верификация за пределы самых критичных систем (по примеру NASA и Apple) в массовое использование. Технология пока на стадии прототипов, спрос высок, но неясно, сколько клиенты готовы платить и как им удобнее её внедрять. Верификация опирается на допущения о взаимодействии компьютеров и людей с ПО, и часть экспертов сомневается, что она поймает ошибки из-за действий пользователя и сбоев оборудования.

Вилл Уилсон (Will Wilson), глава ИИ-стартапа Antithesis, который ищет ошибки в ПО, называет формальную верификацию «ловушкой» для математических фанатов вроде него самого. Antithesis потратил миллионы долларов на формальную проверку части своей киберзащиты, и Уилсон называет это занятием, которое «достаёт» (в оригинале грубее: «pain in the ass»). При этом компания всё равно нашла дополнительные ошибки своим инструментом, а также ошибки в ПО нескольких клиентов, уже прошедшем формальную верификацию. Уилсон: верификация даёт некоторую уверенность, но подтвердить её может только надёжное исчерпывающее тестирование. Виталик Бутерин в блоге написал, что формальная верификация, «не панацея», но он и другие сторонники по-прежнему считают её важной защитой от кибератак ИИ-систем.

Сегодня формально верифицированное ПО, по раскрытиям компаний, есть в самолётах Boeing, серверах Amazon и более чем в 2,5 млрд активных устройств Apple. Обычно это код, связанный с безопасностью. Байрон Кук (Byron Cook), заслуженный учёный и вице-президент Amazon Web Services, говорит, что верификация сняла опасения клиентов насчёт облачной безопасности и помогла внутренним командам двигаться быстрее за счёт раннего устранения крупных ошибок. Но несколько компаний среднего размера рассказали Wired, что проверяли формально обычно лишь одну ключевую функцию продукта, а то и ни одной: не хватает инженеров-верификаторов, затраты перевешивают риски, а ожидание проверки неделями может тормозить разработку. Служба безопасности Apple ранее заявила, что часть проблем в библиотеке corecrypto (для шифрования) нельзя было найти иначе, но компания должна быть «консервативной» при добавлении кода в неё, чтобы успевать его проверять. Двое руководителей по кибербезопасности в крупных компаниях, не верифицировавших код, не уверены, что автоматизация сделает это оправданным, но могли бы платить крупным ИИ-лабораториям за «верифицированный» ИИ-код.

Разработчики открытого ПО всё активнее пробуют верификацию с помощью ИИ: некоммерческий Beneficial AI Foundation на грант Anthropic в этом году проверил тот же код шифрования, что и Сунь. Майкл Розенберг (Michael Rosenberg), мейнтейнер библиотеки curve25519-dalek, надеется на устойчивое финансирование, но не знает, откуда оно возьмётся, и считает, что полагаться на добрую волю ИИ-компаний не стоит. Мадан Мусувати (Madan Musuvathi), ушедший из Microsoft Research после более чем 20 лет работы, основал стартап Truidic: после инцидентов вроде взлома Hugging Face, связанного с OpenAI, он решил, что исследования пора срочно коммерциализировать. Компания Proofcraft, давно предлагающая традиционную верификацию, сообщает о потоке запросов; её CEO Джун Андроник (June Andronick) и главный учёный Гервин Кляйн (Gerwin Klein) говорят, что интерес превышает возможности их и конкурентов. Оба опасаются, что сгенерированные ИИ спецификации породят «неоправданное доверие» к результатам. Кляйн называет работу верификатора «очень затягивающей, как головоломка», и, если всё получится, решать их придётся больше, чем когда-либо.

Ключевые факты

ИИ-инструмент исследователей Стэнфорда во главе с Чуюэ Сунь выполнил инженерный проект меньше чем за полдня и менее чем за $500; трое экспертов делали ту же работу вручную пять месяцев.
&Truth публично запустилась в четверг и привлекла $70 млн; Harmonic (получила $295 млн) расширила ИИ-агента Aristotle на верификацию ПО на C и схем на Verilog.
Anthropic и Theorem с помощью ИИ нашли ошибки в открытом ПО, которые не поймали триллионы тестов, и представили дополнение к Claude для верификации.
Технология на стадии прототипов: неясно, сколько клиенты готовы платить; глава Antithesis Уилсон скептичен, а Proofcraft опасается «неоправданного доверия» к сгенерированным ИИ спецификациям.
Формально верифицированный код уже есть в самолётах Boeing, серверах Amazon и более чем в 2,5 млрд активных устройств Apple, но в основном это код, связанный с безопасностью.

Почему это важно

Формальная верификация, единственный способ математически доказать, что код ведёт себя как задумано, а не просто не сломался на тестах. До сих пор её сдерживали долгая трудоёмкая работа и нехватка специалистов. Если результат Стэнфорда (полдня и менее $500 вместо пяти месяцев у трёх экспертов) подтвердится на других задачах, экономика этого подхода изменится. Вокруг этого уже выросла волна стартапов с крупным финансированием: &Truth с $70 млн, Harmonic с $295 млн, плюс Theorem и Truidic. Сторонники видят в верификации важную защиту от кибератак, которые запускают ИИ-системы.

Кому это важно

Разработчикам и командам безопасности критичного ПО: шифрование, облачная инфраструктура, аппаратные схемы. Мейнтейнерам открытых библиотек, которым нужно устойчивое финансирование проверок. Компаниям среднего размера, которые из-за нехватки верификаторов и стоимости проверяли формально лишь одну ключевую функцию продукта или вовсе ничего. Инвесторам и ИИ-лабораториям: двое руководителей по кибербезопасности допускают, что могли бы платить за «верифицированный» ИИ-код.

Как это применить

Готового продукта для массового внедрения пока нет: технология на стадии прототипов, и цены в материале не называются. Из конкретного: Aristotle от Harmonic поддерживает верификацию ПО на C и схем на Verilog и оценивается потенциальными пользователями; Anthropic и Theorem представили дополнение к Claude, помогающее с верификацией. Общая схема стартапов такая: ИИ автоматизирует описание того, как программа должна себя вести (например, что после сортировки в таблице те же элементы), затем код переводится в формат для инструментов Lean, Rocq и Isabelle, которые проверяют соответствие. Компании среднего размера, по их словам, проверяли формально обычно лишь одну ключевую функцию продукта, а то и ни одной: им не хватает инженеров-верификаторов, а затраты перевешивают риски.

Можно ли доверять

Материал, журналистский обзор Wired; ключевые результаты опираются на статью Сунь, которая в тексте не названа и не приведена по ссылке. Данные о Boeing, Amazon и Apple, по раскрытиям самих компаний. Результат со временем и стоимостью касается одного инженерного проекта, который в тексте не описан подробнее. Затраты на проект Anthropic и Theorem не раскрыты. Заявления стартапов о перспективах, слова заинтересованных сторон, а часть источников (руководители по кибербезопасности, представители компаний среднего размера) не названа по имени.

Риски и подводные камни

Верификация опирается на допущения о взаимодействии компьютеров и людей с ПО, поэтому часть экспертов сомневается, что она ловит ошибки из-за действий пользователя и сбоев оборудования. Глава Antithesis Уилсон потратил миллионы долларов на проверку части своей киберзащиты, всё равно нашёл потом ошибки собственным инструментом, а также ошибки в ПО клиентов, уже прошедшем формальную проверку; по его мнению, подтвердить уверенность может лишь исчерпывающее тестирование. Бутерин напоминает, что это «не панацея». Андроник и Кляйн из Proofcraft опасаются, что сгенерированные ИИ спецификации породят «неоправданное доверие». Неясно, сколько клиенты заплатят и как предпочтут внедрять технологию, а ожидание проверки неделями может тормозить разработку. Мейнтейнер Розенберг предупреждает, что нельзя полагаться на добрую волю ИИ-компаний в вопросе финансирования.

«Мосты, здания не рушатся, потому что люди делали математические расчёты, прежде чем их строить.»

— Илья Сергей, главный научный директор (chief science officer) &Truth