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