Команда выпускников Цинхуа добилась впечатляющих математических прорывов с помощью искусственного интеллекта! Разработанный ими LeanAgent, ИИ-помощник с возможностью обучения на протяжении всей жизни, успешно доказал 162 ранее нерешенные математические теоремы и даже решил формальную проблему полиномиальной гипотезы Фреймана-Рузы, предложенную Теренсом Тао. Это не только демонстрирует огромный потенциал ИИ в фундаментальных научных исследованиях, но и знаменует собой инновацию в математических методах исследования. Редакторы даункодов дадут вам более глубокое понимание этой захватывающей разработки и технологических инноваций, лежащих в основе LeanAgent.
Из последних сенсационных новостей в мире математики группа выпускников Университета Цинхуа использовала возможности искусственного интеллекта, чтобы успешно доказать 162 математические теоремы, которые до этого никому не удавалось решить. Еще более удивительно то, что этот агент по имени LeanAgent фактически преодолел проблему формализации полиномиальной гипотезы Фреймана-Рузы Теренса Теро. Это заставляет нас сожалеть о том, что методы исследования фундаментальной науки были полностью преобразованы ИИ.
Как мы все знаем, хотя нынешние языковые модели (LLM) хороши, большинство из них все еще статичны и не могут усваивать новые знания онлайн. Еще труднее доказывать сложные математические теоремы. Однако LeanAgent, совместно разработанный исследовательскими группами из Калифорнийского технологического института, Стэнфордского университета и Вашингтонского университета, представляет собой помощника искусственного интеллекта с возможностью обучения на протяжении всей жизни, который может постоянно изучать и доказывать теоремы.
LeanAgent реагирует на различные математические трудности посредством тщательно разработанных путей обучения и использует динамическую базу данных для управления непрерывным потоком математических знаний, чтобы гарантировать, что он не забывает уже приобретенные навыки при изучении новых знаний. Эксперименты показывают, что он успешно доказал 162 математические теоремы, которые до этого никому не удавалось решить, с помощью 23 различных библиотек Lean-кодов, а его производительность в 11 раз выше, чем у традиционных больших моделей. Это действительно потрясающе!
Эти теоремы охватывают многие области высшей математики, включая такие сложные проблемы, как абстрактная алгебра и алгебраическая топология. LeanAgent не только может начинать с простых концепций и постепенно решать сложные темы, но и демонстрирует отличную производительность с точки зрения стабильности и обратной миграции.
Однако задача Теренса Тао по-прежнему заставляет ИИ чувствовать себя беспомощным. Хотя интерактивные средства доказательства теорем (ITP), такие как Lean, играют важную роль в формализации и проверке математических доказательств, процесс построения таких доказательств часто бывает сложным и трудоемким, требующим тщательных шагов и обширных библиотек математического кода. Продвинутые большие модели, такие как o1 и Claude, также склонны к ошибкам при столкновении с неформальными доказательствами, что подчеркивает недостатки LLM в точности и надежности математических доказательств.
В предыдущих исследованиях пытались использовать LLM для создания полных этапов доказательства, например LeanDojo, который представляет собой средство доказательства теорем, созданное путем обучения большой модели на конкретном наборе данных. Однако данных для формальных доказательств теорем крайне мало, что ограничивает широкое применение этого подхода. Другой проект, ReProver, представляет собой модель, оптимизированную для библиотеки кода доказательства теорем бережливого производства mathlib4. Хотя он охватывает более 100 000 формальных математических теорем и определений, он ограничен рамками студенческой математики, поэтому он не очень эффективен при работе с более сложными задачами. проблемы. хорошо.
Стоит отметить, что динамичный характер математических исследований ставит перед ИИ более сложные задачи. Математики обычно работают над несколькими проектами одновременно или поочередно. Например, Теренс Тао одновременно продвигает несколько областей исследований, включая гипотезу PFR и симметричное среднее действительных чисел. Эти примеры показывают ключевой недостаток нынешних методов доказательства теорем ИИ: отсутствие системы ИИ, которая могла бы адаптивно обучаться и совершенствоваться в различных математических областях, особенно когда данные бережливого производства ограничены.
Вот почему команда LeanDojo создала LeanAgent, новую систему непрерывного обучения, призванную решить вышеуказанные проблемы. Рабочий процесс LeanAgent включает в себя вычисление сложности теорем для формулирования учебных курсов, балансирование стабильности и гибкости процесса обучения посредством постепенного обучения, а также использование поиска по дереву наилучших результатов для поиска еще не доказанных теорем.
LeanAgent работает с любой крупной моделью, улучшая ее возможности обобщения посредством «извлечения». Его инновация заключается в использовании специальной динамической базы данных для управления постоянно расширяющимися математическими знаниями, а также стратегии обучения курса, основанной на бережливой структуре доказательства, которая помогает изучать более сложный математический контент.
Чтобы справиться с катастрофической проблемой забывания ИИ, исследователи применили прогрессивный метод обучения, позволяющий LeanAgent постоянно адаптироваться к новым математическим знаниям, не забывая предыдущие знания. Этот процесс включает в себя постепенное обучение на каждом новом наборе данных, обеспечивая оптимальный баланс стабильности и гибкости.
Благодаря такому прогрессивному обучению LeanAgent демонстрирует отличные результаты в доказательстве теорем, успешно решая 162 сложные задачи, которые не были решены людьми, особенно в сложных теоремах абстрактной алгебры и алгебраической топологии. Его способность доказывать новые теоремы в 11 раз выше, чем у статического ReProver, сохраняя при этом способность доказывать известные теоремы.
LeanAgent демонстрирует характеристики прогрессивного обучения в процессе доказательства теорем, постепенно переходя от простых теорем к более сложным, доказывая свою глубину усвоения математических знаний. Например, он демонстрирует глубокое понимание математики, доказывая фундаментальные теоремы алгебраической структуры, связанные с теорией групп и теорией колец. В целом, LeanAgent открывает перед математическим сообществом захватывающие перспективы благодаря своим мощным возможностям непрерывного обучения и совершенствования!
Адрес статьи: https://arxiv.org/pdf/2410.06209.
Появление LeanAgent указывает на то, что ИИ будет играть все более важную роль в области математических исследований, и в будущем может появиться больше случаев использования возможностей ИИ для решения сложных математических задач. Это, несомненно, открывает новое направление математических исследований, а также дает новые идеи и методы исследований в других научных областях. Ждем еще более потрясающих результатов в будущем!