Стартап Axiom Math объявил о принятии пяти научных статей с доказательствами, выполненными системой искусственного интеллекта AxiomProver, в рецензируемых математических журналах. Это первый случай, когда работы, полностью подготовленные ИИ, прошли экспертную оценку в академической литературе.
Стартап Axiom Math, разрабатывающий инструменты для автоматизации математических доказательств, достиг значимого рубежа: пять статей, подготовленных системой AxiomProver, были приняты к публикации в рецензируемых математических журналах. Как сообщила компания в своём аккаунте в X (Twitter), с февраля текущего года на платформе arXiv появилось восемь работ по алгебраической геометрии, теории представлений, теории чисел и комбинаторике, выполненных с помощью AxiomProver. Признание пяти из них академическим сообществом стало первым случаем в истории, когда формальные доказательства, сгенерированные ИИ, прошли независимую экспертизу.
AxiomProver — это система, способная не только предлагать гипотезы, но и строго доказывать математические утверждения. В отличие от предыдущих попыток применения ИИ в математике, где модели использовались для поиска закономерностей или генерации идей, AxiomProver самостоятельно строит полные формальные доказательства, которые затем проверяются рецензентами. Как отметил в комментарии для Axios сооснователь Axiom Math Лун Ван (Lun Wang), ключевым фактором успеха стала способность системы работать с символьными выражениями и логическими цепочками на уровне, сопоставимом с человеческим.
Реакция математического сообщества на новость была преимущественно положительной. Профессор Университета Висконсина Димитрис Папайлиопулос (Dimitris Papailiopoulos) назвал это «невероятным прогрессом в области математики и ИИ», подчеркнув, что автоматизация рутинных доказательств освобождает исследователей для более творческой работы. Аналогичные оценки прозвучали от сотрудников Google DeepMind и других компаний, занимающихся разработкой ИИ для научных приложений. В частности, Пейдж Бейли (Paige Bailey), ведущий менеджер по продуктам в Google DeepMind, провела параллель с ростом производительности разработчиков программного обеспечения, отметив, что аналогичный эффект наблюдается и в исследовательской деятельности.
При этом в сообщении Axiom Math подчёркивается, что система не заменяет математиков, а выступает в роли инструмента, позволяющего ускорить проверку гипотез и снизить количество ошибок в доказательствах. Компания также опубликовала подробный технический отчёт о принципах работы AxiomProver, доступный на своём сайте.