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