Искусственный интеллект научился математически доказывать, что код рабочий. Осталось убедить в этом компьютер
Нейросети научились писать программы быстрее, чем люди успевают искать в них ошибки, но теперь искусственный интеллект пытается взять под контроль и саму проверку. Стартап Harmonic, основанный главой Robinhood Владом Теневым и Тудором Акимом, расширил возможности модели Aristotle. Система перешла от доказательства математических теорем к проверке программного кода и электронных схем.
27 октября компания представила поддержку языка C и Verilog, на котором проектируют цифровые микросхемы. Aristotle использует формальную верификацию, то есть математически доказывает соответствие программы заданным требованиям. В отличие от обычных тестов, такой подход позволяет проверить определённые свойства для всех возможных входных данных в рамках выбранной модели.
Aristotle самостоятельно предлагает свойства для проверки, пытается доказать каждое и показывает результат вместе с принятыми допущениями. Разработчики могут сохранить проверенные условия в репозитории и повторять анализ при каждом изменении кода. Подход призван сократить число дефектов, которые пропускают при проверке программ, особенно при массовой генерации кода нейросетями.
Первые практические результаты оказались любопытными. При работе с библиотекой LibTomMath, которую используют Tcl и Dropbear SSH, Aristotle исправил три ошибки. Одновременно модель ускорила модульное возведение в степень на 31–38% по результатам внутренних тестов Harmonic. Разработчики утверждают, что ускоренная реализация математически соответствует исходным требованиям.
При проверке аппаратных схем Aristotle обнаружил в проекте компании Tensordyne ошибки, проявлявшиеся лишь спустя 110 тысяч тактов работы. Подобные дефекты особенно трудно выявлять обычным моделированием, поскольку проблемное поведение может возникать после чрезвычайно длинной последовательности операций. Однако приведённые результаты пока не прошли независимую сравнительную оценку.
Ещё один эксперимент провели в исследовательском центре термоядерного синтеза DIII-D. По представленным результатам, Aristotle за четыре часа воссоздал часть программного обеспечения на основе научной статьи и запроса длиной 254 слова. Проверка охватывала реализацию вычислений на C и вариант для аппаратного ускорения на Verilog. Авторы эксперимента сообщили о доказанной логической эквивалентности двух версий.
Технология продолжает направление, в котором машинную проверку математических доказательств применяют для оценки результатов искусственного интеллекта. Однако математическое доказательство конкретного свойства не гарантирует полной безопасности программы. Качество проверки зависит от правильности требований и допущений, а ошибки за пределами выбранной модели могут остаться незамеченными.
Aristotle уже доступна коммерческим пользователям с оплатой по объёму потребления. Для крупных заказчиков Harmonic предлагает корпоративные варианты развёртывания, включая собственную инфраструктуру и частное облако. В ноябре 2025 года стартап привлёк 120 млн долларов при оценке 1,45 млрд долларов. Среди инвесторов значатся NVentures, Sequoia и Ribbit Capital.