Исследователь из Стэнфорда Чую Сунь и группа ученых разработали ИИ-инструмент, который завершил инженерный проект менее чем за полдня при затратах ниже $500. Для сравнения, аналогичная ручная работа трех высококвалифицированных экспертов заняла пять месяцев. Этот рост эффективности находится на стыке растущих коммерческих инвестиций и повышенного спроса индустрии на безошибочное программное обеспечение.
Десятилетиями разработчики пытались применять математические методы для доказательства отсутствия багов в ПО, однако этот процесс оставался долгим и трудоемким. Компании регулярно проводят сложные тесты для поиска уязвимостей, но формальная верификация — математический подход, способный выявлять аномальное поведение, — внедряется редко из-за высоких издержек и операционных сложностей.
Фундаментальная рыночная тенденция заключается в том, что ИИ способен взять на себя трудоемкие задачи формальной верификации, переводя ее из разряда академической роскоши в базовую корпоративную защиту. На кону стоит способность организаций избегать скрытых дефектов, порождаемых быстрыми циклами разработки с помощью ИИ, без раздувания бюджетов на инженерию. Вопрос в том, смогут ли математические доказательства надежно заменить традиционное тестирование методом проб и ошибок в коммерческих софтверных пайплайнах.
Коммерческий натиск и рыночная оценка
Волна стартапов капитализирует этот технологический сдвиг, привлекая масштабные раунды финансирования для внедрения автоматических математических доказательств в массовое программирование. Среди них — компания &Truth, к которой Чую Сунь присоединилась в августе и которая официально запустилась в четверг. Стартап привлек $70 млн от инвесторов и планирует верифицировать любой язык программирования. Исследования компании продемонстрировали потенциал технологии: ИИ использовался для верификации части кода, отвечающего за шифрование сообщений в мессенджере Signal. Илья Сергей, директор по науке &Truth, указал на общий пробел в индустрии, отметив, что мосты и здания не рушатся, потому что перед строительством инженеры выполняли математические расчеты, и задался вопросом, почему индустрия не поступает так же с кодом.
Мосты и здания не рушатся, потому что перед строительством люди делали математические расчеты. Почему мы не делаем то же самое для кода? Технология для математического анализа существовала всегда, ее просто было сложно масштабировать.
Этот тезис разделяют конкуренты, поддерживаемые венчурным капиталом. Стартап Harmonic, сооснователем которого выступил генеральный директор Robinhood Влад Тенев и который получил $295 млн финансирования, объявил на этой неделе, что его ориентированный на математику ИИ-агент Aristotle поддерживает верификацию ПО на языке C и аппаратных проектов на Verilog.
Реалии корпоративной интеграции
Хотя высококлассная технологическая инфраструктура уже опирается на эти методы — самолеты Boeing, серверы Amazon и более 2,5 млрд активных устройств Apple содержат хотя бы часть формально верифицированного ПО, — массовое коммерческое внедрение сталкивается с серьезными препятствиями. Байрон Кук, видный ученый и вице-президент Amazon Web Services, отмечает, что формальная верификация снизила опасения клиентов по поводу облачной безопасности и помогла внутренним командам двигаться быстрее за счет раннего устранения крупных багов. Ранее в этом году команда безопасности Apple заявила, что некоторые уязвимости в их библиотеке corecrypto, используемой для шифрования, невозможно было обнаружить иным способом. Тем не менее, несколько средних технологических компаний сообщили изданию WIRED, что обычно верифицируют лишь одну ключевую функцию своих продуктов, ссылаясь на дефицит инженеров по верификации, непомерные затраты и опасения, что ожидание результатов проверки кода на протяжении недель затормозит продуктовые инновации.
Скептики утверждают, что лежащая в основе математика фундаментально ограничена непредсказуемостью человека и оборудования. Формальная верификация опирается на допущения о том, как компьютеры и люди взаимодействуют с программным обеспечением, что заставляет некоторых экспертов сомневаться в ее способности находить баги, возникающие из-за пользовательских ошибок и сбоев железа. Как отметил Виталик Бутерин в своем блоге ранее в этом году, формальная верификация не является панацеей, даже оставаясь необходимой защитой от автоматизированных кибератак. Способен ли этот подход избежать участи ловушки, не заменяющей исчерпывающее тестирование, и станут ли клиенты платить за него — остается открытым вопросом для бюджетов на разработку.
Пересмотрите внутренние кодовые базы на этой неделе, чтобы выделить критические зоны шифрования и библиотеки безопасности, где ручные аудиты создают узкие места в графиках релизов, и оцените возможность интеграции пилотного доступа к новым инструментам верификации в текущие среды развертывания.
Как это выглядит рядом
Где именно математические доказательства для кода перестают быть штучным товаром для гигантов? Эксперимент Чую Сунь показал, что софт можно строго проверить за половину дня вместо пяти месяцев ручной работы, срезав траты до символических сумм. Но пока венчурные миллионы текут в стартапы вроде &Truth и Harmonic, обычный средний бизнес все так же застревает на проверке всего одной ключевой фичи из-за нехватки редких экспертов. Венчурные фонды охотно вливают сотни миллионов в автоматизацию доказательств, но средние команды пока с трудом могут позволить себе математическую верификацию хотя бы одной функции продукта.