РоссияНовостьМодели
В РФ создали ИИ-агента для решения сложных математических задач
Ученые AIRI создали LongTails: платформа автоматизирует математические исследования, доказывает теоремы через Lean 4 и уже отработала около 100 теорем
В РФ создали ИИ-агента для решения сложных математических задач
30 октября 2026, 10:10
0
Фото: ИЗВЕСТИЯ/Эдуард Корниенко
Озвучить текст
Выделить главное
Вкл
Выкл
Ученые Института AIRI разработали LongTails — программную платформу, автоматизирующую значительную часть математических исследований. Система формулирует задачи математической оптимизации, ищет способы их решения и формально доказывает результаты. На одну теорему агенту требуется в среднем от трех до семи часов, что позволяет решать задачи этого класса в разы быстрее математиков.
С помощью LongTails уже отработано около 100 теорем. В 50 случаях удалось улучшить известные ранее результаты, еще по 35 результатам исследователи планируют подготовить отдельные статьи для международных научных журналов.
LongTails специализируется на математической оптимизации, методы которой применяются, в частности, при обучении нейросетей, в логистике, энергетике, инженерии, химии и физике. Ключевая особенность системы — формальная проверка доказательств с помощью Lean 4. Это позволяет выявлять ошибки, которые могут оставаться незаметными при обычной проверке текста, сгенерированного ИИ.
«При этом автоматизация математических исследований не исключает человеческого контроля. Ошибка может возникнуть еще на этапе постановки задачи: если исходные условия сформулированы неверно, система способна безошибочно доказать уже некорректное утверждение», — отметила советник практики интеллектуальной собственности юрфирмы «ЭБР» Ольга Яшина.
Подробнее читайте в эксклюзивном материале «Известий»:
Скор на разгадку: новый ИИ-агент докажет теоремы в разы быстрее математиков
Комментарии
Обсуждайте статью, отвечайте и оценивайте комментарии. Вход — через ваш Яндекс ID.
Загружаем обсуждение…