С помощью разработки агенты ставят новые задачи математической оптимизации и придумывают, как их решить. Полученные результаты они могут строго доказать. При этом система поддерживает работу с разными ИИ-агентами и автоматически контролирует каждое доказательство.

Механизм проверки использует Lean. На этом языке программирования система составляет алгоритмы, а затем оценивает корректность их исполнения. Математики применяют Lean для проверки теорем.

Как объяснили исследователи, убедительность ответа ИИ сама по себе не означает его правильности. Модель может допустить ошибку в рассуждении или доказать результат для задачи с другими условиями. Автоматическая проверка позволяет справиться с этой проблемой.

Российская команда уже разобрала около 100 теорем, причем в половине случаев улучшила ранее известные гарантии. Ученые намерены посвятить 35 результатам отдельные научные работы, достойные международных публикаций. В среднем агент затрачивает на одно доказательство от трех до семи часов.

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

Тюрин рассказал, что исследователи продолжат доказывать теоремы, займутся более сложными задачами и их структурированием. Кроме того, команда намерена добиваться эффективной работы найденных алгоритмов в практических условиях.

Оптимизация необходима для обучения нейросетей любых типов. Ее методы также играют важную роль в логистике и разработке новых конструкционных материалов, используются во многих физических и биологических исследованиях.

Источник: ТАСС