Следующая модель OpenAI, Astra, только что решила десять многолетних открытых задач по математике

1 августа OpenAI опубликовала отчёт, в котором заявила, что её следующая модель, внутреннее название Astra (пока недоступна), получила новые результаты по десяти различным открытым задачам в математике. (Нет, это не задачи тысячелетия, но они всё равно весьма значимы.)

Важно отметить: это не постепенный прогресс над задачами, а полноценные решения, проверенные в Lean. (Lean — это язык программирования и ассистент доказательств, который требует, чтобы каждый шаг математического рассуждения был расписан в машинно-читаемых деталях.) 

Материала много. В этой статье задачи упорядочены по областям; даётся обзор того, что произошло, какие выводы это может иметь для математики как дисциплины и что ещё можно понять про Astra.

Какие это десять задач?

Ниже — каждое из достижений простыми словами, с указанием соответствующей области математики или информатики.

Не- Софиковые группы

Область: теория групп

Astra построила явный пример группы, которую нельзя сколь угодно точно аппроксимировать большими конечными структурами — тем самым закрыв вопрос, открытый с 1999 года, когда был введён термин «софиковая» группа. Конструкция сопровождается доказательством того, что никакая последовательность конечных приближений не сработает, формализованным в Lean, чтобы логику можно было проверить машинно.

Статью в Wikipedia уже обновили:

Упаковка сфер

Область: многомерная геометрия

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

Бинарные и сферические коды

Область: теория кодирования

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

Гипотеза жёсткости Конна

Область: алгебры операторов

Ален Конн предположил, что определённые группы всегда можно однозначно восстановить из построенной по ним алгебраической структуры — алгебры фон Неймана. Astra опровергла это, построив две по-настоящему разные группы, которым соответствует одна и та же алгебра, показав тем самым, что восстановление не всегда взаимно-однозначно.

Сложность арифметических схем

Область: теория вычислительной сложности

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

Квантовое параллельное повторение

Область: теория квантовой сложности

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

Задача ближайшего вектора

Область: криптография на решётках

Дана периодическая сетка точек (решётка) и целевая точка; требуется найти ближайшую сеточную точку — задача, считающаяся очень сложной в высоких размерностях, поэтому она лежит в основе некоторых устойчивых к квантовым атакам схем шифрования. Astra доказала, что даже приближённое решение в пределах конкретного полиномиального фактора остаётся доказуемо трудным, что укрепляет криптографию, основанную на этой задаче.

Гипотеза Эрхарта об объёме

Область: дискретная и выпуклая геометрия

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

Многоцветные числа Рамсея

Область: теория Рамсея / комбинаторика

Если людей достаточно много, а типов отношений между ними — тоже достаточно, то рано или поздно найдутся трое, связанные между собой отношениями одного и того же типа. Astra доказала, что минимальный размер такой группы растёт быстрее любой фиксированной экспоненты по мере увеличения числа категорий, решив задачу Эрёша № 183.

Гипотезы экстремальных чисел

Область: экстремальная теория графов

Эта область спрашивает, сколько связей может иметь сеть, всё ещё избегая определённых малых, запрещённых подструктур. Astra решила две родственные гипотезы здесь, соответствующие задачам Эрёша № 146 и № 180, уточнив, насколько плотными могут быть такие сети до того, как эти подструктуры станут неизбежными.

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

Подождите, а контрпример — это «простой» вид доказательства?

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

Самое распространённое возражение: несколько из этих результатов — это контрпримеры, а не новая общая теория. Это важно, потому что контрпример отвечает на вопрос «да/нет», но сам по себе не объясняет, почему шаблон ломается, и не даёт семейство подобных объектов для дальнейшего изучения; в то время как, скажем, теорема классификации или новая техника открывают больше дверей.

В целом это возражение справедливо, но оно не тянет на огульное отрицание всего этого набора задач. Во-первых, результат о не-софиковых группах — не небольшая доработка какого-то почти-решения; это первая подобная конструкция за 27 лет, когда вообще не было ни одной, и ожидается, что использованная техника обобщится на поиск других.

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

Что остаётся нерешённым

Есть несколько моментов, за которыми стоит следить, пока сообщество будет разбирать работу в ближайшие дни, недели и месяцы:

\n
• Пока без рецензирования. Доказательства проверены в Lean и неформально просмотрены математиками, видевшими препринты, но ни одно ещё не прошло через процесс рецензирования в журнале. 
\n
• Вопрос соавторства ещё обсуждается. OpenAI заявляет, что берёт на себя ответственность за рукописи и формализации в Lean, при этом приписывая математические доводы самой модели. Независимо воспроизвести процесс (в отличие от проверки доказательств) сейчас сложно.
\n

Что это значит для математики

Самое непосредственное изменение — в том, на что математики могут реально тратить время. Если корректно поставленную открытую задачу можно передать модели и проверить в Lean, узкое место смещается с «кто-нибудь вообще сможет это решить» на «правильно ли мы задали вопрос и формализовали его». Навык формулировать хорошую задачу и понимать, за какую стоит браться, — это реальный навык, который приходит с опытом. 

Есть и вопрос финансирования и престижности. Гранты, решения по тенюру и премии исторически строились вокруг дефицита: задачи были достаточно трудными, и их решение что-то говорило о решившем. Если результаты с помощью ИИ станут обычным делом, сообществу понадобятся новые способы различать то, что по-настоящему сложно, и то, что теперь по силам за несколько тысяч долларов инференса. Конечно, средний человек не до конца понимает эти задачи. Люди с реальной подготовкой — понимают, и это не меняется. Так что математические знания ценны как никогда. 

Как люди реагируют

Реакция в соцсетях разделилась не столько по вопросу корректности доказательств, сколько по тому, о чём они свидетельствуют.

Некоторые видят в темпе событий самую важную новость: десять старых задач разом, в несвязанных областях, быстрее, чем эксперты успевают их даже просмотреть. Вопрос на будущее: «Сумеем ли мы успевать проверять всё это?»

Другие возражают, что это говорит о возможностях ИИ в целом меньше, чем кажется. Математика — редкая область, где работу модели можно проверить автоматически и полностью. Большинство реальных задач такого встроенного «ключа ответов» не имеют. С этой точки зрения достижение реально, но оно, возможно, больше говорит о том, что математика необычно хорошо подходит для ИИ.

Третья линия комментариев: корректное доказательство, которое никто ещё полностью не изучил и не осмыслил, — это пока не понимание, а лишь верификация. Открыть теорему и понять, что она значит, — в этом взгляде две разные задачи.

Итоги

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

Чего ещё не произошло — это более медленная часть: рецензирование, воспроизведение поискового процесса и дальнейшее развитие этих результатов сообществом. Это занимает больше времени, чем один пост в блоге, и именно это покажет, насколько велико было событие. Мы будем держать вас в курсе.