Harmonic, стартап зі сфери штучного інтелекту, співзаснований CEO Robinhood Владом Тенєвим, випустив бета-версію свого чат-бота для iOS та Android з вбудованою моделлю Aristotle — ШІ, розробленим спеціально для математичних розв’язків без галюцинацій.
Компанія, яка нещодавно залучила $100 мільйонів інвестицій у раунді B при оцінці $875 мільйонів, відрізняється від основних моделей ШІ акцентом на математичному суперінтелекті (MSI). На відміну від традиційних великих мовних моделей, які часто помиляються у складних обчисленнях, Aristotle створювався з нуля для гарантії точності у кількісних задачах.
«Aristotle — це перший продукт, доступний людям, який виконує логічні розв’язки та формально перевіряє результати», — зазначає CEO та співзасновник Harmonic Тудор Акім. «У тих сферах, які підтримує Aristotle, а саме у кількісному мисленні, ми дійсно гарантуємо відсутність галюцинацій».
Система досягає такої точності завдяки двоетапному процесу. Спочатку Aristotle перекладає математичні задачі з природної мови на відкриту мову програмування Lean 4 — асистент доказів, що дозволяє перевіряти математичні визначення та теореми на коректність. Далі, перед тим як надати відповідь користувачу, модель додатково перевіряє розв’язки за допомогою алгоритмічної верифікації, яка не використовує ШІ — подібно до методів перевірки у критично важливих сферах, як-от медичне обладнання чи авіація.
Harmonic стверджує, що Aristotle досяг рівня «золотої медалі» на Міжнародній математичній олімпіаді (IMO) 2025 року під час формального тестування, коли задачі переводилися у машинозчитуваний формат. Це досягнення відбулося у рік, коли моделі від Google DeepMind та OpenAI також досягли «золотих медалей» на IMO, але під час неформальних тестів у природній мові.
Амбіції компанії виходять за межі математики. У Harmonic вважають, що MSI допоможе користувачам у всіх сферах, що залежать від математичного мислення, включаючи фізику, статистику та інформатику. Згодом компанія планує випустити API для корпоративного доступу та вебдодаток для споживачів, що потенційно може змінити підхід індустрій до задач, які вимагають точної кількісної аргументації.