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