Исследователи из Массачусетского технологического института (MIT), Дэвид Роу и Эндрю Сазерленд, входят в число первых получателей грантов AI for Math от Renaissance Philanthropy и XTX Markets.
Кроме них, были отмечены ещё четыре выпускника MIT: Аншула Ганди, Виктор Кунчак, Гириджа Ранаде и Дамиано Теста. Они получили гранты за отдельные проекты.
Первые 29 проектов-победителей будут поддерживать математиков и исследователей в университетах и организациях, работающих над созданием систем искусственного интеллекта, которые помогают продвигать математические открытия и исследования в нескольких ключевых областях.
Роу и Сазерленд вместе с Крисом Беркбеком из Университета Восточной Англии будут использовать свой грант для развития автоматизированного доказательства теорем путём создания связей между Базой данных L-функций и модульных форм (LMFDB) и математической библиотекой Lean4 (mathlib).
«Автоматизированные системы доказательства теорем технически сложны, но их разработка недостаточно обеспечена ресурсами», — говорит Сазерленд. «Благодаря технологиям искусственного интеллекта, таким как большие языковые модели (LLM), барьер для входа в эти формальные инструменты быстро снижается, делая системы формальной верификации доступными для работающих математиков».
Mathlib — это большая математическая библиотека, управляемая сообществом, для средства проверки теорем Lean, формальной системы, которая проверяет правильность каждого шага в доказательстве. В настоящее время Mathlib содержит порядка $10^5$ математических результатов (таких как леммы, предложения и теоремы).
LMFDB — это обширный совместный онлайн-ресурс, который служит своего рода «энциклопедией» современной теории чисел и содержит более $10^9$ конкретных утверждений. Роу и Сазерленд являются управляющими редакторами LMFDB.
Грант Роу и Сазерленда будет использован для проекта, направленного на расширение возможностей обеих систем. Результаты LMFDB станут доступны в mathlib в виде утверждений, которые ещё не были формально доказаны, а также будут предоставлены точные формальные определения числовых данных, хранящихся в LMFDB.
Это позволит как людям-математикам, так и агентам искусственного интеллекта использовать единую систему для работы с математическими данными.
Исследователи отмечают, что доказательство новых теорем на переднем крае математических знаний часто включает шаги, основанные на нетривиальных вычислениях. Например, в доказательстве Великой теоремы Ферма Эндрю Уайлсом используется так называемый «трюк 3-5» в решающем месте доказательства.
«Этот трюк зависит от того, что модульная кривая X_0(15) имеет лишь конечное число рациональных точек, и ни одна из этих рациональных точек не соответствует полустабильной эллиптической кривой», — по словам Сазерленда. «Этот факт был известен задолго до работы Уайлса, и его легко проверить с помощью вычислительных инструментов, доступных в современных системах компьютерной алгебры, но это не то, что можно реалистично доказать с помощью карандаша и бумаги, и это не так просто формализовать».
Для преодоления этих препятствий исследователи будут использовать финансирование для создания инструментов доступа к LMFDB из mathlib, делая большую базу данных неформализованных математических знаний доступной для системы формальных доказательств.
«Предоставление большой базы данных неформализованных теоретико-числовых фактов в mathlib станет мощным инструментом для математических открытий, поскольку набор фактов, которые агент может рассмотреть при поиске теоремы или доказательства, экспоненциально больше, чем набор фактов, которые в конечном итоге необходимо формализовать при фактическом доказательстве теоремы», — говорит Роу.
Исследователи отмечают, что подключение формальных систем доказательства к системам компьютерной алгебры для более эффективной проверки позволяет использовать вычислительные результаты из существующих математических баз данных.
Использование сохранённых результатов позволяет использовать тысячи человеко-лет вычислительного времени, уже потраченного на создание LMFDB, экономя средства, которые потребовались бы для повторного выполнения этих вычислений. Наличие предварительно вычисленной информации также делает возможным поиск примеров или контрпримеров без предварительного определения широты поиска.
«Тот факт, что теоретики чисел подчеркнули роль проводника в базах данных эллиптических кривых, уже сыграл решающую роль в одном примечательном математическом открытии, сделанном с помощью инструментов машинного обучения», — говорит Сазерленд.
«Наши следующие шаги — создать команду, взаимодействовать с сообществами LMFDB и mathlib, начать формализовать определения, лежащие в основе разделов эллиптических кривых, числовых полей и модульных форм в LMFDB, и сделать возможным запуск поиска в LMFDB из mathlib», — говорит Роу. «Если вы студент MIT и хотите принять участие, не стесняйтесь обращаться!»
1. Какие цели и задачи стоят перед исследователями, получившими гранты AI for Math?
Исследователи, получившие гранты AI for Math, стремятся ускорить математические открытия и исследования в ключевых областях. Они планируют использовать финансирование для создания инструментов доступа к LMFDB из mathlib, делая большую базу данных неформализованных математических знаний доступной для системы формальных доказательств.
2. Какие технологии и инструменты будут использоваться для достижения целей проекта?
Для достижения целей проекта будут использоваться технологии искусственного интеллекта, такие как большие языковые модели (LLM), а также системы формальной верификации, например, математическая библиотека Lean4 (mathlib). Исследователи также планируют использовать системы компьютерной алгебры для более эффективной проверки математических утверждений.
3. Какие преимущества даёт использование AI для математических исследований?
Использование AI для математических исследований позволяет преодолеть технические сложности при разработке автоматизированных систем доказательства теорем. Технологии искусственного интеллекта снижают барьер для входа в формальные инструменты, делая их доступными для работающих математиков. Кроме того, использование сохранённых результатов позволяет экономить средства и время, которые потребовались бы для повторного выполнения вычислений.
4. Какие конкретные шаги планируют предпринять исследователи в рамках проекта?
Исследователи планируют создать команду, взаимодействовать с сообществами LMFDB и mathlib, начать формализовать определения, лежащие в основе разделов эллиптических кривых, числовых полей и модульных форм в LMFDB, и сделать возможным запуск поиска в LMFDB из mathlib.
5. Как гранты AI for Math могут повлиять на будущее математических открытий?
Гранты AI for Math могут значительно ускорить математические открытия, предоставляя исследователям мощные инструменты и ресурсы для работы. Создание единой системы для работы с математическими данными позволит как людям-математикам, так и агентам искусственного интеллекта более эффективно исследовать и доказывать математические теоремы.