Разработка математиков из России помогла ИИ доказать свыше 30 новых теорем

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

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

К настоящему времени российские математики проработали около сотни теорем. Примерно для 50 из них удалось получить более сильные гарантии, чем в прежних работах. Ученые собираются оформить 35 результатов как отдельные научные работы, достойные международных публикаций.

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

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

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

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

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