ИИ-агент из AIRI доказывает теоремы за часы: 35 результатов уйдут в журналы

Российские исследователи из Института AIRI совместно с вьетнамским студентом Куок Вьетом представили платформу LongTails. Она сама формулирует задачи математической оптимизации, подбирает методы решения и формально доказывает итоги. На одну теорему у агента уходит от трех до семи часов — это в разы быстрее, чем у профессионалов. Данную информацию сообщает портал Известия.

Система уже отработала около 100 теорем. В 50 случаях ИИ показал, что алгоритмы могут работать быстрее и точнее, чем считалось ранее. Еще 35 результатов настолько уникальны, что авторы готовят по ним отдельные статьи для крупных международных журналов.

Руководитель научной группы «Методы оптимизации в машинном обучении» AIRI Александр Тюрин признался: фреймворк за пару дней доказал больше, чем он за всю карьеру. Он отметил, что сложно определиться с отношением к этому, но это очень интересно. Планы — повышать сложность задач и добиваться практической эффективности алгоритмов.

Ключевая особенность LongTails — формальная проверка результатов через язык Lean 4. Обычная языковая модель может выдать убедительное на вид доказательство с ошибкой или не по той постановке. Платформа сверяет соответствие формальным условиям и цели.

Эксперты видят главный риск в том, что система может дать корректный ответ на некорректно поставленную задачу. Как отметила советник практики интеллектуальной собственности ЮК «ЭБР» Ольга Яшина, если постановку сформулировал агент, ошибка может быть заложена уже на этом этапе. Тогда безупречное доказательство подтверждает неверный результат, и ответственность остается на исследователе.

Основатель финтех-платформы SharesPro Денис Астафьев обратил внимание на различие между формальной корректностью и научным пониманием. Доказательство может быть безупречным математически, но недоступным для человеческого понимания. Для развития науки этого мало: нужно понимать, почему метод работает и как применять его в других задачах.

Ведущий разработчик MWS AI Cowork Егор Старовойтов считает перспективными системы, которые объясняют ход рассуждений. Иначе машина решает конкретную задачу, но не дает человеку нового понимания. Заведующий кафедрой РУС «ГЦОЛИФК» Михаил Новоселов полагает, что ИИ возьмет на себя вычисления и технический поиск, а специалисту останутся постановка задач и оценка значимости.

Доцент Финансового университета при правительстве РФ Артур Вафин предупредил об образовательном риске: если постоянно передавать ИИ сложные этапы рассуждений, молодые исследователи получат меньше практики. Обучение должно сочетать работу с ИИ и самостоятельное решение задач.

Массового неприятия технологий среди математиков нет. Заместитель руководителя направления «Искусственный интеллект» ИТ-холдинга Т1 Евгений Григорьев отметил, что ИИ берет на себя рутину — поиск и проверку доказательств, перебор подходов. Это освобождает время для сложных задач.

Профессия математика изменится, но не исчезнет. Даже если агент сам формулирует задачи, определять их важность будет человек. Ситуация напоминает появление калькуляторов: ручная работа ушла, профессия осталась. Теперь нужно уметь ставить задачи перед ИИ и проверять результаты.

Политолог Елена Штульман подчеркнула: технологический прогресс повышает требования к человеку, а не отменяет его роль. Исследователь должен определять научную ценность задач и контролировать применение результатов. Руководитель команды ИИ-тренеров модели Alice AI по высшей математике Ашот Маргарян добавил: ИИ — хороший ассистент для проверки гипотез и рутинных вычислений, но создание концептуального подхода и подлинная научная новизна невозможны без ученого.

Материал подготовлен по информации «Известий».