ИИ OpenAI решил 10 математических задач, некоторые оставались открытыми 60 лет

OpenAI представила десять новых результатов в математике и теоретической информатике, полученных внутренней версией модели Astra. Некоторые из затронутых задач оставались открытыми несколько десятилетий. Компания опубликовала сами доказательства, их формальные версии для машинной проверки и отдельный документ, объясняющий, как модель пришла к ключевым идеям. Об этом говорится в публикации OpenAI от 1 августа.

Речь идет не о решении сложных примеров или олимпиадных задач. Astra работала с вопросами, на которые не было известных ответов у профессиональных математиков. OpenAI отобрала задачи, по которым основной результат не продвигался как минимум десять лет, а в некоторых случаях более полувека.

В опубликованной работе представлены результаты по теории групп, геометрии, теории кодирования, квантовым вычислениям, криптографии и теории графов. Полный документ занимает 249 страниц.

Самый громкий результат связан с несофическими группами

Одним из центральных результатов стала конструкция первой известной несофической группы. Чтобы понять значение этого результата, сначала нужно разобраться, что математики называют группой.

В математике группа представляет собой набор объектов и правил, по которым их можно комбинировать. Такие структуры помогают описывать симметрии, повороты, перестановки и множество других процессов.

Софическую группу можно представить как очень сложную или даже бесконечную систему правил, отдельные фрагменты которой удается достаточно точно воспроизвести с помощью конечного набора перестановок.

Математики долго не знали, существуют ли группы, которые принципиально невозможно приблизить таким способом. Свойство софичности появилось в работе Михаила Громова в 1999 году, а вскоре был сформулирован вопрос о существовании несофических групп.

Astra построила конкретный пример такой группы. Если доказательство выдержит независимую проверку, это даст отрицательный ответ на вопрос, который оставался открытым около 25 лет.

Какие еще задачи решила модель

• Упаковка сфер в пространствах большой размерности. Представить такую задачу можно как попытку как можно плотнее заполнить пространство одинаковыми шарами. В обычном мире это похоже на укладку апельсинов в коробку, но Astra работала с пространствами, где измерений намного больше трех. Модель получила новую общую границу плотности. Авторы называют ее первым улучшением соответствующего показателя с 1978 года.
• Двоичные и сферические коды. Такие коды помогают передавать и хранить информацию так, чтобы ошибки можно было обнаруживать или исправлять. Модель улучшила известные границы, определяющие, сколько кодовых комбинаций можно разместить на заданном расстоянии друг от друга.
• Гипотеза жесткости Конна. У математической группы может быть своеобразная алгебраическая тень, называемая алгеброй фон Неймана. Предполагалось, что для определенного класса групп по этой тени можно однозначно восстановить исходную группу. Astra построила бесконечно много разных групп с одинаковой алгеброй, тем самым опровергнув гипотезу.
• Сложность арифметических вычислений. Модель получила новые нижние границы для вычисления перманента матрицы. Простыми словами, результат показывает, насколько большой должна быть вычислительная схема, чтобы выполнить определенный тип сложного расчета.
• Повторение квантовых игр. В теоретической информатике игры между участниками используют для изучения вычислений и проверки доказательств. Astra доказала общий результат, согласно которому вероятность успешной стратегии быстро уменьшается при многократном повторении квантовой игры.
• Задача о ближайшем векторе. Необходимо найти точку математической решетки, расположенную ближе всего к заданной цели. Подобные задачи связаны с решетчатой криптографией, которую рассматривают как одно из направлений защиты информации от будущих квантовых компьютеров. Модель получила новый результат о сложности приближенного решения этой задачи.
• Гипотеза Эрхарта об объеме. Представим многомерную фигуру, расположенную на сетке из целых точек. Ее центр является единственной точкой сетки внутри фигуры. Еще в 1964 году Эжен Эрхарт спросил, насколько большой может быть такая фигура. Astra доказала предполагаемую максимальную границу для любого числа измерений.
• Многоцветные числа Рамсея. Если соединить каждую пару точек линией и раскрасить линии несколькими цветами, при достаточно большом количестве точек обязательно появится треугольник одного цвета. Модель показала, насколько быстро увеличивается необходимое число точек при добавлении новых цветов, и решила задачу Эрдеша №183.
• Две гипотезы в теории графов. Astra построила специальные графы, которые опровергают гипотезы о компактности и вырожденности. Эти результаты также закрывают задачи Эрдеша №146 и №180.

Зачем доказательства перевели в Lean

Обычное математическое доказательство пишется для людей. Автор может пропустить очевидный для специалиста шаг, сослаться на известный результат или использовать сложное рассуждение, которое другой ученый должен проверить вручную.

Lean позволяет записать доказательство в строгой формальной форме. Каждый объект, условие и логический переход описывается так, чтобы компьютер мог проверить, действительно ли вывод следует из предыдущих шагов.

Это не означает, что программа сама оценивает научную значимость открытия. Lean проверяет логическую конструкцию в рамках заданных определений и предпосылок. Специалистам все равно предстоит оценить корректность постановки задач, новизну методов и связь результатов с предыдущими исследованиями.

OpenAI разместила формальные сертификаты в открытом репозитории. Там находятся отдельные файлы Lean для упаковки сфер, несофических групп, гипотезы Конна, задачи Эрхарта, чисел Рамсея и остальных результатов.

Опубликован не исходный ход мыслей, а его реконструкция

Вместе с доказательствами OpenAI выпустила 62-страничный документ о процессе поиска решений. Его не следует считать дословной выгрузкой всех внутренних рассуждений Astra.

Как объясняет компания, другая модель изучила первоначальные цепочки рассуждений, итоговые статьи и математические записи, после чего подготовила понятную реконструкцию. В ней показано, какие подходы сначала казались перспективными, где возникали препятствия и какие изменения направления привели к окончательному доказательству.

Что означает сумма в 2000 долларов

OpenAI оценила стоимость токенов, использованных для поиска всех десяти решений, примерно в 2000 долларов по тарифам Sol API.

Эта цифра не является полной стоимостью проекта. В нее не входят обучение Astra, разработка инфраструктуры, работа сотрудников, подготовка статей и последующая формализация. Она показывает лишь примерную стоимость непосредственных запросов к уже существующей модели.

Можно ли считать задачи окончательно закрытыми

Публикация доказательства является только началом научной проверки. Другие математики должны внимательно разобрать аргументы, сопоставить их с известными работами и убедиться, что в постановках и используемых предпосылках нет скрытых проблем.

Формализация в Lean значительно усиливает результат, поскольку компьютер проверяет логические переходы. Однако окончательное признание открытий зависит и от независимой оценки научного сообщества. Сама OpenAI призвала математиков изучить опубликованные материалы, проверить их и развить предложенные идеи.

Если результаты подтвердятся, работа Astra станет одним из наиболее заметных примеров того, как искусственный интеллект может не только пересказывать известную науку, но и предлагать новые доказательства для задач исследовательского уровня.