Скорость, с которой искусственный интеллект совершенствует свои математические способности, многих удивила. Он переосмысливает само понятие математика.
Неужели эпоха рукописных математических вычислений подходит к концу? Лаборант / Алами
В марте 2025 года математик Даниэль Литт заключил пари. Несмотря на стремительный прогресс искусственного интеллекта во многих областях, он считал свою тему безопасной, поспорив с коллегой, что вероятность того, что к 2030 году ИИ сможет написать математическую статью на уровне лучших математиков-людей, составляет всего 25 процентов. Всего год спустя он считает, что ошибся. «Теперь я ожидаю проиграть это пари», — заявил он в своем блоге.
Математики были поражены скоростью улучшения способности ИИ решать задачи и создавать доказательства. «Пару лет назад они были практически бесполезны даже для решения школьных математических задач, а теперь иногда могут решать задачи, которые действительно встречаются в научной работе математика», — говорит Литт из Университета Торонто.
Этот прогресс опережает многие прогнозы, и математики предупреждают, что их профессия переживает одну из самых быстрых эволюций за всю историю. «Нам больше негде спрятаться», — написал Джереми Авигад из Университета Карнеги-Меллона в Пенсильвании в недавнем эссе. «Мы должны смириться с тем фактом, что искусственный интеллект вскоре сможет доказывать теоремы лучше, чем мы».
Реакцию вызывает не какое-то одно событие, а устойчивый прогресс в математике, демонстрируемый искусственным интеллектом. В прошлом году такие компании, как OpenAI и Google DeepMind, завоевали золотые медали на Международной математической олимпиаде — элитном соревновании для старшеклассников, которое многие эксперты ранее считали неподвластным инструментам ИИ. В январе математики начали использовать аналогичные инструменты для решения давних задач, поставленных венгерским математиком Полом Эрдошем.
В настоящее время, в рамках двух отдельных этапов развития, искусственный интеллект начал брать на себя более сложные математические задачи, решая реальные исследовательские проблемы и помогая автоматически проверять передовые доказательства, что традиционно требовало огромных усилий от групп математиков.
В феврале Никхил Шривастава из Калифорнийского университета в Беркли и его коллеги запустили проект First Proof, пытаясь найти более реалистичный критерий для проверки математических способностей ИИ. Первый этап проекта состоял из 10 задач, которые исследователям необходимо было решить в рамках своей работы, из совершенно разных математических областей.
«Это были проблемы, которые естественным образом возникали в ходе наших повседневных исследований, — говорит Шривастава. — Они взяты из типичного распределения сложности. Они не были сверхсложными, но и не были рутинными. Диапазон действительно был очень широк».
Доказательство прогресса
После того, как проблемы стали достоянием общественности, начали появляться решения. Исследователи из технологических компаний, включая OpenAI и Google DeepMind, были среди тех, кто пытался решить задачи из серии «Первое доказательство» с помощью собственных моделей ИИ. OpenAI утверждает, что, согласно «отзывам экспертов», она правильно решила половину задач, в то время как Google DeepMind набрала 6 баллов из 10, по словам математиков, с которыми она консультировалась по каждой задаче.
«Все изменилось так быстро, — говорит Тханг Луонг из Google DeepMind. — Для нас сейчас ИИ действительно стал серьезным партнером, будь то для проведения серьезных исследовательских работ или, как в случае с First Proof, он может самостоятельно предложить решение».
Инструмент Google для решения математических задач на основе искусственного интеллекта, называемый Aletheia, использует ресурсоемкую версию своего чат-бота Gemini AI в сочетании с алгоритмом проверки для поиска недостатков в возможных решениях. Затем он может итеративно улучшать свои решения самостоятельно, пока не найдет правильный ответ. Google не раскрыл публично, сколько итераций потребовалось Aletheia для решения этих задач, что затрудняет оценку его эффективности, но математики все равно впечатлены.
Не все проблемы были единогласно признаны решенными. Например, в случае с проблемой № 8, которая относится к узкоспециализированной области геометрии, только пять из семи экспертов, опрошенных Google, согласились с тем, что предложенное решение является правильным. Иван Смит из Кембриджского университета, не участвовавший в проекте Google, говорит, что ИИ, похоже, подходит к этой проблеме разумно и демонстрирует хороший прогресс. «Если бы это был аспирант, который поделился бы своими мыслями, это было бы обнадеживающе и укрепило бы уверенность в том, что результат действительно верен», — говорит Смит.
Это подчеркивает проблему с доказательствами, созданными ИИ, — их проверка требует больших усилий. Легко может возникнуть ситуация, когда ИИ сможет создавать доказательства быстрее, чем люди смогут их проверить. Если теорема доказана ИИ, но рядом нет никого, кто мог бы ее проверить, доказана ли она? ИИ может помочь и здесь.
Технология быстро совершенствуется в преобразовании рукописных доказательств на естественном языке, таких как задачи, поставленные в «Первом доказательстве», в формат, который может быть проверен компьютером; этот процесс называется формализацией.
Компания Math, Inc., занимающаяся разработкой искусственного интеллекта, недавно удивила математиков, объявив, что ее инструмент на основе ИИ, Gauss, формализовал удостоенное наград доказательство и подтвердил его правильность. Доказательство касалось того, сколько сфер можно упаковать в пространство, и стало предметом награждения Марины Вязовской Филдсовской премии 2022 года, которую часто называют Нобелевской премией по математике.
Работа по формализации трудов Вязовской началась в конце 2024 года с небольшой группы математиков, работавших независимо от Math. Inc. под руководством Сидхарта Харихарана из Университета Карнеги-Меллона, которые надеялись вручную перевести задачу в компьютерный код. Сначала они рассмотрели решение Вязовской задачи об упаковке сфер в восьми измерениях. Пока они неуклонно продвигались вперед, компания Math. Inc., которая позже оказала помощь исследователям, объявила, что у нее уже есть полное доказательство, а затем и более общая версия результата для 24 измерений.
Харихаран и его коллеги первоначально набросали план формализации работы, а также сформулировали важные математические определения. Без этого ИИ не смог бы завершить свои доказательства, говорит Бхавик Мехта из Имперского колледжа Лондона, который работал над формализацией вместе с Харихараном.
«Мы изготовили все детали, но не написали инструкцию по их сборке», — говорит Крис Биркбек из Университета Восточной Англии (Великобритания), также входящий в команду.
Математик нового стиля
Окончательное доказательство заняло около 200 000 строк кода, что составляет примерно 10 процентов от всей существующей формализованной математики. Хотя этот код, вероятно, примерно в 10 раз длиннее, чем тот, который человек написал бы для выполнения той же задачи, это все равно огромное достижение, говорит Йохан Коммелин из Утрехтского университета в Нидерландах. «Это очень важно. Это работа, удостоенная Филдсовской премии, и она автоматически формализуется».
По словам Коммелина, подобные усилия теперь должны быть возможны и в большом количестве других областей, что может изменить практику математики. «В будущем мы все будем думать о инструментах, которые будут автоматически формализовывать новые исследования и математические статьи и отмечать наличие ошибок», — говорит Коммелин. «Это будет иметь огромное значение, например, для работы с экспертами и рецензированием».
В условиях будущего, в котором все большая доля математических вычислений будет выполняться искусственным интеллектом, некоторые математики, такие как Авигад, бьют тревогу по поводу пагубных последствий, которые это может иметь для нашей способности практиковать и создавать новые математические модели.
Использование машин для решения задач, подобных тем, что рассматриваются в книге «Первое доказательство», может привести к получению конкретных доказательств, говорит Анна Мария Боманн из Университета Вандербильта в Теннесси, но при этом мы теряем «возможность обучения», добавляет она. «Борьба за создание и формулирование новых идей и решение новых проблем — один из главных способов, с помощью которого как студенты, так и специалисты в области математики закрепляют свои знания».
Тони Фенг, один из членов команды Aletheia в Google DeepMind, придерживается аналогичного мнения и с осторожностью относится к использованию этого инструмента самостоятельно. «Часто мне кажется, что я должен сам изучать этот вопрос и развивать свою интуицию».
Даже формализация доказательств может дать важные результаты, говорит Мехта, и теперь ему и его коллегам предстоит разобраться с доказательством, состоящим из 200 000 строк кода ИИ, чтобы понять, что может быть полезно для других проектов.
Однако математики по-прежнему надеются, что им найдется место в будущем, где все большее значение приобретают машины. Обращаясь к истории, Коммелин говорит, что когда-то ручные вычисления составляли значительную часть работы математика, но теперь они выполняются автоматически. «Я думаю, что здесь произойдут похожие вещи: мы радикально изменим то, чем занимаемся, но через 10 или 20 лет мы все равно будем считать, что делаем математику, только в новом стиле».
Статья изменена 11 марта 2026 года.
Мы уточнили, кто принимал участие в формализации упаковки сфер.
Источник: www.newscientist.com
