OpenAI: модель Astra решила или продвинула десять открытых математических задач

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

Публикация связана с инициативой «ChatGPT для научных сотрудников» (ChatGPT for Academic Researchers), в рамках которой OpenAI ранее объявила о бесплатном доступе к своим лучшим моделям ChatGPT для 100 000 учёных и математиков; компания говорит, что заодно продолжает проверять свои модели на открытых исследовательских задачах в ходе разработки.

По оценке OpenAI, весь объём токенов, который потребовался модели, чтобы найти решения всех десяти задач, обошёлся бы примерно в $2000 по тарифам Sol API. Найденные моделью аргументы затем оформили в рукописи люди, вместе с той же моделью. После этого модель формализовала каждое доказательство в виде Lean-сертификата (машинно проверяемого формального доказательства). Для каждого решения OpenAI также публикует пересказ модели о ходе её собственных рассуждений.

Список задач охватывает высокоразмерную геометрию, теорию кодирования, сложность арифметических схем, теорию групп, операторные алгебры, квантовую теорию сложности, решёточную криптографию и экстремальную комбинаторику:

Упаковка сфер в высоких размерностях: новые верхние оценки плотности упаковки, доведённые до порога Кона, Элкиса.
Двоичные и сферические коды: экспоненциально улучшенные оценки максимального размера двоичных кодов при заданном минимальном расстоянии и аналогичные результаты для сферических кодов в высоких размерностях.
Несофические группы: построение, доказывающее существование несофических групп, центральный открытый вопрос теории групп.
Гипотеза жёсткости Коннеса: опровержение давней гипотезы о том, что некоторые группы однозначно определяются своими алгебрами фон Неймана.
Сложность арифметических схем: новые нижние оценки для вычисления перманента арифметическими схемами и формулами, включая оценку снизу порядка n⁴/log n для арифметических формул.
Квантовое параллельное повторение: экспоненциальная теорема параллельного повторения для общих двухигровых квантовых игр, распространение фундаментального принципа классической теории сложности на квантовый случай.
Задача о ближайшем векторе: доказательство твёрдости приближения с полиномиальным фактором для задачи о ближайшем векторе, основополагающего вопроса решёточной криптографии, связанного с постквантовой криптографией.
Гипотеза Эрхарта об объёме: определён, в каждой размерности, максимально возможный объём выпуклого тела, у которого центроид, единственная внутренняя точка решётки.
Мультицветные числа Рамсея: сверхэкспоненциальная нижняя оценка для мультицветных треугольных чисел Рамсея, решение 183-й задачи Эрдёша.
Экстремальные числа: результаты по гипотезам компактности и вырожденности в экстремальной теории графов, решение 146-й и 180-й задач Эрдёша.

Это продолжение более раннего результата: в мае OpenAI уже показывала ИИ-опровержение гипотезы Эрдёша о единичных расстояниях, найденное при тестировании ещё не выпущенной модели; с тех пор оно уже вдохновило несколько независимых математических работ.

OpenAI отдельно проговаривает вопрос авторства: компания подчёркивает, что приписывать доказательство, полностью сгенерированное ИИ-системой, человеку, значит исказить и вклад системы, и природу подлинного человеческого интеллектуального труда. По словам компании, она помогла подготовить рукописи и формализовать доказательства в Lean и берёт на себя ответственность за их корректность, тогда как сами математические аргументы сгенерировала система. При этом ни имена конкретных исследователей, ни точная дата выхода Astra в посте не названы.

Ключевые факты

Внутренняя, ещё не выпущенная версия Astra, будущей ключевой модели OpenAI, представила десять результатов: каждый либо решает, либо существенно продвигает старую открытую задачу по математике и теоретической информатике.
Среди результатов, опровержение гипотезы жёсткости Коннеса, определение максимального объёма выпуклого тела по гипотезе Эрхарта, новые оценки для упаковки сфер, двоичных кодов и задачи о ближайшем векторе (важна для постквантовой криптографии).
Решены три конкретные проблемы Эрдёша из его списка открытых вопросов: №183 (мультицветные числа Рамсея) и №146 с №180 (экстремальные числа).
По оценке OpenAI, весь объём токенов на решение всех десяти задач обошёлся бы примерно в $2000 по тарифам Sol API; найденные аргументы затем оформили в рукописи люди вместе с моделью, а модель сама формализовала каждое доказательство в виде Lean-сертификата.
OpenAI явно отказывается приписывать результат человеку: компания берёт на себя ответственность за корректность рукописей и формализаций, но подчёркивает, что сами математические аргументы сгенерировала система.

Почему это важно

Это заявка на новый уровень возможностей ИИ в фундаментальной науке: не подсказки или черновики, а формально проверяемые (Lean) доказательства и оценки по десяти разным задачам сразу, от геометрии упаковки сфер до постквантовой криптографии. OpenAI прямо связывает публикацию с майским ИИ-опровержением гипотезы Эрдёша о единичных расстояниях, которое уже породило несколько независимых математических работ, то есть речь не о разовом трюке, а о продолжающейся серии результатов.

Кому это важно

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

Как это применить

Практический канал доступа, инициатива ChatGPT for Academic Researchers: 100 000 учёных и математиков получили бесплатный доступ к лучшим моделям ChatGPT. Сама Astra в посте не датирована и подана как «наша следующая ключевая модель», то есть ещё не выпущена публично. Оценка OpenAI в $2000 токенов на все десять задач, ориентир по порядку вычислительных затрат, но не готовый прайс для стороннего пользователя.

Можно ли доверять

Источник, собственный блог OpenAI, независимой проверки в тексте нет; в посте не названы ни конкретные исследователи-соавторы рукописей, ни точная дата релиза Astra. Доказательства формализованы в Lean, это машинная проверка корректности логического вывода, которая снижает риск ошибки в самой математике, но не заменяет независимую экспертную оценку значимости и новизны результатов сообществом. Формулировка OpenAI подчёркнуто осторожна: не «десять задач решено», а «решает или существенно продвигает», это разграничение стоит сохранять и при пересказе.

Риски и подводные камни

Главный риск, упрощение: свести формулировку «решает или существенно продвигает» к плоскому «ИИ решил десять задач» и тем самым исказить масштаб (часть результатов, это новые оценки и границы, а не окончательные решения). Отдельный узел напряжения, вопрос авторства и признания: OpenAI сама заявляет, что приписывать полностью сгенерированное ИИ доказательство человеку было бы искажением, и ссылается на существование Лейденской декларации, подписанной математиками, обеспокоенными ролью ИИ в их дисциплине, то есть сообщество расколото в оценке того, как такие результаты должны учитываться в математической практике.

«Приписывать доказательство, полностью сгенерированное ИИ-системой, человеку, значит исказить и вклад системы, и природу подлинного человеческого интеллектуального труда.»

— OpenAI