- Стартап Harmonic привлек $120 млн инвестиций и оценен в $1,45 млрд, получив статус «единорога».
- Разрабатываемый ими искусственный интеллект Aristotle представляет собой математический суперразум с формальной проверкой решений для минимизации ошибок.
- Aristotle уже продемонстрировал высокие результаты на Международной математической олимпиаде и специализированных наборах задач, соревнуясь с ведущими ИИ-системами.
Стартап Harmonic, основанный Владом Теневым (одним из основателей Robinhood) и Тюдором Ахимом, завершил новый раунд финансирования, привлекая $120 млн и достигая оценки примерно в $1,45 млрд, что вывело компанию в статус «единорога». Основное стремление Harmonic — создать уникальный искусственный интеллект под названием Aristotle, который отличается от традиционных языковых моделей. В отличие от универсальных чат-ботов, склонных к генерации неточных данных и «галлюцинаций», Aristotle позиционируется как математический суперразум, способный решать сложнейшие задачи с использованием строгих доказательств.
Ключевой особенностью этой системы является сочетание нейросети и формальной системы доказательств на языке Lean4. Языковая модель помогает сгенерировать идеи и шаги решения, однако каждое решение должно быть формально описано и затем проверено ядром системы. Если доказательство не соответствует формальным критериям, оно отвергается, что кардинально снижает вероятность появления ошибок. Таким образом, Harmonic обещает практически полное исключение галлюцинаций в областях, где задачи можно формализовать — это математика, логика и смежные области.
На данный момент Aristotle уже существует в виде действующей модели. Она показала высокое качество выполнения задач на международной математической олимпиаде, разделив «золото» с такими продвинутыми ИИ, как Google Gemini 2.5 DeepThink и экспериментальными системами OpenAI. Ранее Aristotle также продемонстрировал эффективность на специализированных наборах MiniF2F, содержащих комплексные формализованные задачи из учебников и конкурсов.
Привлечённые средства в $120 млн Harmonic намерена направить на улучшение возможностей Aristotle и расширение сферы его применения за пределы строго математических задач. В планах — использование системы для проверки финансовых моделей и деривативов, автоматического поиска ошибок в программном обеспечении, анализа инженерных расчётов и поддержки научных исследований, где необходимы точные и формально проверяемые доказательства. Авторы проекта подчёркивают, что в таких критичных сферах традиционные «болтливые» языковые модели слишком ненадежны, а интеграция нейросети с системой Lean4 может стать оптимальным решением.
Примечательно, что идея контроля и проверки выводов ИИ не уникальна для Harmonic — подобный подход используется, в частности, при обучении GPT-5 в OpenAI, где отдельная нейросеть отсеивает ошибки и недостоверные ответы.
