Открылась ИИ-система, которая решает задачи Международной математической олимпиады

Стартап Harmonic отменил лист ожидания для своей системы Aristotle. И теперь любой может зарегистрироваться и сразу получить доступ к API. Aristotle — это система автоматического доказательства теорем. Которая в июле 25 года решила 5 из 6 задач Международной математической олимпиады, показав результат на уровне золотой медали. В отличие от аналогов OpenAI и Google DeepMind, которые достигли того же уровня, но остаются закрытыми, Aristotle стал первым публично доступным ИИ такого класса с формальной верификацией.

Ключевая фишка — каждое решение формализуется в языке доказательств Lean 4, и если код проходит проверку компилятора, решение считается верифицированным. Глава Harmonic Тюдор Ачим говорит, что это гарантирует отсутствие галлюцинаций в количественных и математических задачах. Такой подход используется в авиации и медоборудовании.

Система работает через командную строку. Устанавливаете Python-библиотеку aristotlelib, получаете ключ, запускаете терминал и всё. Задачи можно писать на Lean 4 или обычном английском. Архитектура включает поисковую систему доказательств на трансформере с более 200 миллиардов параметров, модуль генерации лемм и решатель геометрии Yuclid. Harmonic основан в 23, среди сооснователей глава Robinhood Влад Тенев. На сегодня Aristotle — это единственный публично доступный искусственный интеллект уровня золотой медали IMO.

Похоже, что система Aristotle показывает что высокоуровневый математический ИИ может быть открытым в отличие от закрытых моделей гигантов. И формальная верификация делает систему надёжной без галлюцинаций.