Израильский стартап бросил вызов гигантам ИИ-индустрии в решении математических задач

Компания doubleAI, основанная Амноном Шашуа, предложила альтернативный путь развития ИИ-математики. Стартап всего за $2000 продвинулся в решении задачи, поставленной почти 40 лет назад.

ИИ-гиганты, в первую очередь OpenAI, при решении математических задач действуют масштабом: вкладывают миллионы долларов и огромные мощности суперкомпьютеров в решение сотен задач сразу. Но израильский стартап doubleAI выбрал принципиально иной путь. Стартап основан профессором Амноном Шашуа (CEO Mobileye). doubleAI фокусируется не на универсальном интеллекте (AGI), а на концепции "искусственного экспертного интеллекта" (Artificial Expert Intelligence, AEI).

Гонка "математических доказательств", которую подстегивает OpenAI, быстро показала проблемы массового подхода к математике. Стремясь решить сотни математических проблем за раз, языковые модели общего назначения нередко выдают громоздкие тексты, которые крайне трудно прочитать и понять человеку. Более того, математическое сообщество указывает на проблему семантического расхождения: код доказательства на языке Lean, генерируемый ИИ для машины, не всегда совпадает по смыслу с текстом в стандартной нотации, который тоже генерирует ИИ, но он предназначен для чтения человеком. Из-за этого проверка "ИИ-открытий" становится трудной, а результат неоднозначным.

Ответом doubleAI стала демонстрация работы системы Double Agent. Алгоритм улучшил коэффициент обхвата для регулярных графов с 4/3 до 8/5, сделав важный шаг в проблеме, остававшейся без продвижения с 1988 года. Система сгенерировала новое алгебраическое построение, проверила его через Lean, сформировала строгое доказательство и потратила на все только $2000.

Секрет эффективности doubleAI – в отказе от масштабного охвата в пользу поиска в узком пространстве идей. Система не тратит ресурсы на лишние знания, а погружается в конкретную математическую дисциплину. Double Agent работает по принципу, который использовался в шахматной программе AlphaZero: агент генерирует гипотезы, мгновенно проверяет их и учится на собственных успешных формальных выкладках. Человек-ученый задает вектор поиска и проверяет условия, а ИИ берет на себя глубинный перебор.

Оценка doubleAI уже превысила $1 миллиард. Cтартап доказывает, что глубинный узкий поиск в сочетании со строгой верификацией может быть эффективнее метода "грубой силы", который используют гиганты ИИ-индустрии.