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