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