Бог из машины (буквально). Модель «Аристотель» показала проблески нечеловеческой логики на тестах по математике.
Harmonic тренирует искусственный интеллект на синтетических доказательствах и заставляет его говорить языком кода, чтобы потом доверить ему самолеты и деньги.
Стартап Harmonic, который развивает системы искусственного интеллекта и был основан при участии CEO Robinhood Влада Тенева, привлек 120 млн долларов инвестиций. После нового раунда компания оценивается в 1,45 млрд долларов и обещает решать одну из главных проблем современных моделей ИИ - так называемые "галлюцинации", то есть неправильные или бессмысленные ответы, за счет более продвинутых механизмов рассуждения.
Раунд серии C возглавил фонд Ribbit Capital, к нему присоединились действующие инвесторы Sequoia и Kleiner Perkins. Новым участником стала инвестиционная компания Emerson Collective Лорин Пауэлл Джобс. Для Harmonic это уже третье крупное привлечение средств за последние 14 месяцев, а общий объем инвестиций достиг 295 млн долларов. Такой интерес показывает, что инвесторы готовы делать крупные ставки на команды, которые пытаются сделать ИИ более надежным и точным, даже если у стартапа пока нет коммерческих продуктов и выручки.
Harmonic разрабатывает то, что называет "математическим сверхинтеллектом" (Mathematical Superintelligence, MSI) - разновидность ИИ, сфокусированную на сложном формальном мышлении. В компании заявляют, что их подход позволяет избавиться от галлюцинаций и фактических ошибок, которые часто встречаются в генеративных моделях, работающих с естественным языком.
Флагманская модель Harmonic называется Aristotle. Ее обучали на синтетических математических доказательствах - это автоматически сгенерированные примеры, которые используются для отработки навыков решения задач и построения строгих рассуждений. По словам компании, Aristotle в июле показала результат уровня призеров на Международной математической олимпиаде, выступив в одном ряду с решениями от Google и OpenAI. Генеральный директор Harmonic Тюдор Аким отмечает, что именно этот успех заметно усилил интерес инвесторов.
Стартап был основан в 2023 году и делает ставку на формальные методы. В Harmonic требуют от модели не просто выдать ответ в виде текста, а расписать ход рассуждений в виде компьютерного кода на языке Lean4. Такой код затем можно автоматически проверить на корректность. Основная часть свежепривлеченных средств, как говорит Аким, пойдет на оплату колоссальных вычислительных мощностей, необходимых для обучения подобных систем.
Ставка на формальное, проверяемое мышление должна помочь завоевать доверие в отраслях, где ошибки особенно опасны, например в авиационно космической сфере, автопроме или финансах. "Устранение галлюцинаций напрямую следует из того, что мы заставляем систему выдавать рассуждения в виде кода, а не в виде английского текста" - объясняет Аким.
Сейчас Harmonic предоставляет доступ к модели Aristotle через бесплатный API. Разработчики, математики и исследователи уже используют его для проверки сложных доказательств и ускорения работы над новыми идеями. Коммерциализацию своих технологий компания пока только планирует. По словам Акима, наибольший интерес к таким системам проявляют те области разработки, где безопасность и надежность играют ключевую роль, а также заказчики из критически важных отраслей вроде автопрома и аэрокосмической промышленности.