ИИ может сделать математическую проверку программ практичной
Стартапы рассчитывают, что генеративный ИИ сделает формальную верификацию — математическое доказательство отсутствия ошибок в коде — дешевле и доступнее. Эксперты расходятся во мнениях, выйдет ли метод за пределы самых критичных систем.
Исследовательница Стэнфордского университета Чуюэ Сунь и её коллеги-информатики создали инструмент на основе ИИ, который выполнил инженерный проект меньше чем за полдня и менее чем за 500 долларов. Трое высококвалифицированных специалистов делали ту же работу вручную пять месяцев. Эти ранние результаты привлекли внимание к формальной верификации — узкой области программирования и математики, где с помощью математики доказывают, что программа работает как задумано.
Традиционно процесс долгий и трудоёмкий: инженеры должны точно сформулировать цели программы и преобразовать код в формулы, поддающиеся проверке. Компании проводят сложные тесты, но редко платят за формальную верификацию, хотя она способна выявить ещё более нестабильное поведение.
Гонка стартапов
Теперь ряд стартапов надеется, что генеративный ИИ сделает её практичной. Сунь присоединилась к &Truth в августе; компания в четверг публично начала работу и привлекла 70 миллионов долларов. В её исследовании с помощью ИИ проверена часть кода, шифрующего переписку в мессенджере Signal. Конкурент Harmonic, сооснованный главой Robinhood Владом Тенёвым и получивший 295 миллионов долларов, сообщил, что его ИИ-агент Aristotle поддерживает проверку программ на языке C и аппаратных проектов на Verilog. Потенциальные пользователи, включая Nvidia и Tensordyne, оценивают технологию. На прошлой неделе Anthropic и стартап Theorem объявили, что с помощью ИИ нашли ошибки в открытом программном обеспечении, которые не обнаружили триллионы тестов.
Сомнения и ограничения
Технология пока на стадии прототипов, и неясно, сколько клиенты готовы платить. Некоторые эксперты сомневаются, что она выявит ошибки, вызванные действиями пользователей или сбоями оборудования. Уилл Уилсон, глава Antithesis, называет формальную верификацию «ловушкой» и считает, что уверенность подтверждает только исчерпывающее тестирование. Виталик Бутерин также писал, что она не панацея.
Формально проверенное ПО уже есть в самолётах Boeing, серверах Amazon и устройствах Apple. Компании среднего размера обычно проверяют лишь одну ключевую функцию из-за нехватки специалистов, затрат и риска замедлить разработку. Руководители Proofcraft предупреждают, что составленные ИИ спецификации могут вызвать «неоправданное доверие» к результатам.
