Российские математики вместе с коллегами из Вьетнама создали систему, с помощью которой ИИ-агенты формулируют задачи математической оптимизации, находят способы их решения и строго доказывают полученные результаты. Как передает ТАСС со ссылкой на пресс-службу Института искусственного интеллекта AIRI, несколько разных агентов доказали более 30 новых теорем.
Разработка совместима с большим числом ИИ-агентов и автоматически проверяет каждое доказательство. Система составляет алгоритмы на языке программирования Lean, который применяется в математике для формальной проверки доказательств, после чего контролирует корректность их выполнения.
Такой механизм предназначен для устранения одной из проблем использования искусственного интеллекта в математике. Модель может сформировать внешне убедительное доказательство, которое содержит ошибку либо относится к иной постановке задачи, а автоматическая проверка позволяет выявлять подобные случаи.
Система работает с задачами математической оптимизации. Методы этой области используются при обучении нейросетей, а также в логистике, создании конструкционных материалов и физических и биологических исследованиях.
К настоящему времени ученые проработали около 100 теорем. Для половины из них удалось улучшить гарантии, известные по более ранним работам, а 35 результатов исследователи намерены оформить как отдельные научные работы для международных публикаций.
На доказательство одной теоремы ИИ-агент расходует в среднем от 3 до 7 часов. Руководитель научной группы AIRI «Методы оптимизации в машинном обучении» Александр Тюрин сообщил, что исследователи продолжат доказывать новые теоремы, повышать сложность задач, систематизировать их и работать над практической эффективностью найденных алгоритмов.