Theorem приввлекает $6 млн для верификации кода с помощью ИИ

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

Theorem, базирующаяся в Сан-Франциско компания, вышедшая из инкубатора Y Combinator (весенний набор 2025 года), объявила во вторник о привлечении 6 миллионов долларов в рамках посевного раунда финансирования. Средства пойдут на создание автоматизированных инструментов для проверки правильности ПО, сгенерированного ИИ. Лид-инвестором раунда выступила венчурная компания Khosla Ventures при участии Y Combinator, e14, SAIF, Halcyon, а также бизнес-ангелов, включая Блейка Боргессона (сооснователя Recursion Pharmaceuticals) и Артура Брейтмана (сооснователя блокчейн-платформы Tezos).

Инвестиции поступают в ключевой момент. ИИ-помощники для программирования от таких компаний, как GitHub, Amazon и Google, теперь ежегодно генерируют миллиарды строк кода. Внедрение таких решений в корпоративном секторе ускоряется. Однако способность проверять, действительно ли написанный ИИ софт работает так, как задумано, за этим не поспевает. Это создает то, что основатели Theorem называют растущим «разрывом в контроле», который угрожает критической инфраструктуре — от финансовых систем до электросетей.

«Мы уже находимся в этой точке, — отметил Джейсон Гросс, сооснователь Theorem, отвечая на вопрос о том, опережает ли сгенерированный ИИ код возможности человеческой проверки. — Если бы вы попросили меня проверить 60 000 строк кода, я бы не знал, как это сделать».

Почему ИИ пишет код быстрее, чем люди успевают его проверять

Ключевая технология Theorem объединяет формальную верификацию — математический метод доказательства того, что программное обеспечение ведет себя строго в соответствии со спецификацией — с моделями ИИ, обученными автоматически генерировать и проверять доказательства. Такой подход превращает процесс, который исторически требовал многих лет работы инженеров с докторской степенью (PhD), в задачу, занимающую, по утверждению компании, недели или даже дни.

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

Гросс знает об этом не понаслышке. До основания Theorem он защитил докторскую диссертацию в Массачусетском технологическом институте (MIT), работая над верифицированным криптографическим кодом, который сегодня лежит в основе протокола безопасности HTTPS, защищающего триллионы интернет-соединений ежедневно. По его оценке, этот проект потребовал пятнадцати человеко-лет работы.

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

Как формальная верификация находит ошибки, ускользающие от традиционного тестирования

Система Theorem работает на основе принципа, который Гросс называет «дробным разложением доказательств». Вместо исчерпывающего тестирования каждого возможного поведения программы (что вычислительно невыполнимо для сложного софта), технология распределяет ресурсы верификации пропорционально важности каждого компонента кода.

Недавно этот подход позволил обнаружить баг, который прошел незамеченным при тестировании в компании Anthropic — создателе чат-бота Claude. По словам Гросса, эта техника помогает разработчикам «находить баги уже сейчас без затрат огромных вычислительных мощностей».

В ходе недавней технической демонстрации под названием SFBench специалисты Theorem использовали ИИ для перевода 1276 задач из Rocq (помощника по формальным доказательствам) в Lean (другой язык верификации), после чего автоматически доказали эквивалентность каждого перевода оригиналу. По оценкам компании, команде людей на выполнение той же работы потребовалось бы около 2,7 человеко-лет.

«Каждый может запускать агенты параллельно, но мы также способны запускать их последовательно», — пояснил Гросс, отметив, что архитектура Theorem справляется со взаимозависимым кодом (где решения надстраиваются друг над другом в десятках файлов), на котором спотыкаются обычные ИИ-агенты для кодинга, ограниченные размером контекстного окна.

Как одна компания превратила 1,500-страничную спецификацию в 16,000 строк надежного кода

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

Клиент обратился в Theorem, имея на руках PDF-спецификацию объемом 1500 страниц и устаревшую реализацию софта, страдающую от утечек памяти, сбоев и других трудноуловимых ошибок. Их самой острой задачей было повышение производительности с 10 мегабит в секунду до 1 гигабита в секунду — то есть в 100 раз — без внесения дополнительных ошибок.

Система Theorem сгенерировала 16 000 строк промышленного кода, который клиент развернул в продакшене без какого-либо ручного ревью. Уверенность обеспечила компактная исполняемая спецификация — всего несколько сотен строк, обобщающих огромный PDF-документ, — в сочетании с инструментом проверки эквивалентности, который подтвердил, что новая реализация полностью соответствует задуманному поведению.

«Теперь у них есть парсер промышленного уровня, работающий на скорости 1 Гбит/с, который они могут развернуть с уверенностью в том, что при синтаксическом анализе не теряется ни байта информации», — заявил Гросс.

Риски безопасности, скрытые в созданном ИИ софте для критической инфраструктуры

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

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

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

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

Чем Theorem отличается от других стартапов по верификации кода ИИ

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

«Наши инструменты полезны командам системных инженеров, работающим «близко к «железу», которым необходимы гарантии корректности перед слиянием изменений», — сказал он.

Команда основателей отражает эту техническую направленность. Гросс обладает глубокой экспертизой в теории языков программирования и опытом масштабного внедрения верифицированного кода в продакшн. Сооснователь Раджашри Агравал (Rajashree Agrawal), инженер-исследователь в области машинного обучения, сосредоточена на обучении ИИ-моделей, которые приводят в действие конвейер верификации.

«Мы работаем над формальными рассуждениями программ, чтобы каждый мог контролировать работу не просто ИИ уровня среднего программиста, а по-настоящему задействовать возможности искусственного интеллекта уровня Линуса Торвальдса», — заявила Агравал, упомянув легендарного создателя Linux.

Гонка за верификацией ИИ-кода до того, как он начнет управлять всем

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

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

Гросс формулирует ставки предельно жестко. Системы ИИ совершенствуются по экспоненте. Если эта траектория сохранится, он считает сверхчеловеческую разработку программного обеспечения неизбежной — она будет способна проектировать системы, более сложные, чем все, что когда-либо создавал человек.

«И без принципиально иной экономики контроля, — подчеркнул он, — мы в конечном итоге развернем системы, которыми не управляем».

Машины пишут код. Теперь кому-то нужно проверить их работу.