Harmonic привлекла $120 млн на создание математического суперразума Aristotle

Стартап Harmonic, основанный Владом Теневым (Robinhood) и Тюдором Ахимом, закрыл новый раунд финансирования на 120 млн долларов и получил оценку около $1,45 млрд – статус "единорога". Компания делает ставку не на очередного универсального чат-бота, а на специализированный "математический суперразум" Aristotle, который должен решать сложные задачи со строгими доказательствами и минимумом галлюцинаций.

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

Aristotle уже существует в виде рабочей модели, которая добилась золота Международной математической олимпиады наравне с Google Gemini 2.5 DeepThink и экспериментальным ИИ от OpenAI. Ранее Aristotle ghjдемонстрировал высокие результаты на наборах наподобие MiniF2F, где собраны формализованные задачи из учебник��в и соревнований.

$120 млн инвестиций Harmonic планирует вложить в расширение возможностей Aristotle и выход за пределы чистой математики. Логика компании проста: если ИИ умеет надежно работать с формальными объектами, его можно использовать там, где цена ошибки особенно высока. Речь идет о проверке финансовых моделей и деривативов, автоматическом поиске ошибок в программном обеспечении, анализе инженерных расчетов, а со временем – и о помощи в научных исследованиях, где важны строгие доказательства и аккуратная работа с формулами. Для таких сценариев обычный "болтливый" ИИ слишком ненадежен, а связка "нейросеть + Lean4" выглядит более естественным кандидатом.

Стоит отметить, что подход с "проверяющим" не является ноу-хау Harmonic. Например, OpenAI при тренировке GPT-5 применили специальную нейросеть, которая проверяла ответы модели — если в них были галлюцинации, то ответ не засчитывался.

P.S. Поддержать меня можно подпиской на канал "сбежавшая нейросеть", где я рассказываю про ИИ с творческой стороны.