Открылась ИИ-система, которая решает задачи Международной математической олимпиады
Стартап 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 показывает что высокоуровневый математический ИИ может быть открытым в отличие от закрытых моделей гигантов. И формальная верификация делает систему надёжной без галлюцинаций.
AIvengo >
Новости ИИ >
Открылась ИИ-система, которая решает задачи Международной математической олимпиады
Почитать из последнего
Вайб-кодинг убивает Open Source - и это проблема для всех
Исследователи из Центрально-Европейского университета в Вене обнаружили жёсткую закономерность. Вайб-кодеры только потребляют ресурсы, но ничего не отдают обратно. Откуда нейросеть может взять знания? А берет она их из Open Source. Из тех самых бесплатных библиотек и фреймворков, которые энтузиасты создавали 10летиями.
Как уболтали ИИ-бота на скидку 80%
Владелец небольшого бизнеса в Англии поставил на сайт чат-бота на ИИ, чтобы он отвечал на вопросы клиентов по ночам. Полгода всё работало идеально — бот консультировал и помогал оформлять заказы, даже продажи росли. А потом нашёлся 1 хитрец, который за час беседы выманил у искусственного интеллекта скидку 80% на заказ в £8000.
Как DeepSeek обманул Anthropic и что из этого вышло
Представьте: вы годами строите уникальную технологию, вкладываете миллиарды, а кто-то просто скачивает её через прокси. Именно это произошло с Anthropic. Компания раскрыла промышленный шпионаж 3 китайских лабораторий. DeepSeek, Moonshot и MiniMax.
Учёные сломали защиту ИИ обычным вопросом
Исследователи из Microsoft наткнулись на дыру размером с ворота. Оказалось, что всю защиту ИИ можно обойти на этапе обучения 1 безобидным запросом. И дальше модель превращается в послушную машину по производству любой гадости.
США обвинили Nvidia в помощи китайским военным через DeepSeek
Глава комитета Конгресса по Китаю Джон Муленаар направил письмо министру торговли Говарду Латнику с серьёзными обвинениями. По его словам, документы Nvidia свидетельствуют, что инженеры компании помогали китайскому стартапу DeepSeek оптимизировать обучение их моделей. Теперь эти модели развёрнуты в подразделениях планирования мобилизации Народно-освободительной армии Китая.
