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

Для проверки она составляет алгоритмы на Lean — языке программирования, который математики используют для контроля доказательств теорем. Затем система проверяет, правильно ли исполняются эти алгоритмы. Исследователи пояснили, что такой подход помогает справиться с одной из основных проблем ИИ в математике. Модель способна предложить внешне убедительное доказательство, в котором скрыта ошибка или которое на самом деле решает иначе поставленную задачу.

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

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

«Наша система за пару дней доказала больше результатов, чем я сам за всю свою карьеру. Сложно определиться, как я к этому отношусь, но это очень интересно», — заявил Тюрин.

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

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

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