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

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

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

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

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

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

Несофические группы

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

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

Википедия уже обновлена:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Что пока не решено

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

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

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

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

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

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

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

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

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

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

Итоги

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

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