Astra от OpenAI формализовала решения десяти задач

OpenAI 1 августа опубликовала формальные доказательства решений десяти математических задач, которые оставались открытыми как минимум с 2016 года. Доказательства сгенерировала внутренняя модель Astra; конечная формализация выполнена в системе верификации Lean. Компания выложила в открытый доступ формальные сертификаты и записи рассуждений модели.

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

Среди решений — конструкция, доказывающая существование несофических групп, что закрывает ключевой вопрос, связанный с введённым в 1999 году понятием софичности. Модель представила опровержение гипотезы жёсткости Конна о фон-Неймановых алгебрах и решение гипотезы Эрхарта, связанной с объёмом многомерных тел. В числе результатов — решение задачи Эрдеша №183 о мультицветных числах Рамсея.

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

Реакция научного сообщества была разной. Математик Томас Блум охарактеризовал опубликованные материалы как “большую новость” и “весомый шаг” в области конструкций. Соавтор технологии рассуждений Ноам Браун отметил, что модель не решила все целевые задачи и что команда пыталась подступиться к другим крупным проблемам без успеха; среди нерешённых остались так называемые задачи тысячелетия, за которые Математический институт Клэя предлагал премии.

Внутри OpenAI Astra выделили в отдельный класс моделей наряду с Sol, Terra и Luna. Компания не определилась, будет ли Astra выпущена как GPT-6 или как новая версия в линейке GPT-5, и не назвала дату публичного релиза. Представители OpenAI демонстрировали возможности Astra политикам и регуляторам в Вашингтоне 26 июля. По представленным правилам федеральных органов США, новые крупные модели могут потребовать предварительной оценки перед публичным запуском.

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

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