OpenAI впервые публично назвала Astra — свою следующую крупную модель. Но привычного релиза с кнопкой «попробовать» пока не произошло. Вместо этого компания выложила 249-страничный сборник с десятью новыми результатами в математике и теоретической информатике, полученными внутренней версией Astra.
Это уже не очередной рекорд на олимпиадных задачах и не улучшение процентов в специально подготовленном бенчмарке. OpenAI утверждает, что выбрала проблемы, по основному результату которых не было существенного прогресса как минимум десять лет, а в ряде случаев — значительно дольше.
Фраза «Astra решила десять нерешённых задач» всё же несколько упрощает картину. В одних случаях модель действительно закрыла открытый вопрос, в других — опровергла гипотезу, а где-то получила существенно более сильную математическую оценку.
Среди опубликованных результатов:
— построение явной несофической группы, закрывающее один из центральных вопросов теории групп;
— опровержение гипотезы Конна о жёсткости групповых алгебр фон Неймана;
— новые границы плотности упаковки сфер в пространствах высокой размерности;
— усиление оценок для двоичных и сферических кодов;
— теорема о параллельном повторении для квантовых игр;
— новый результат о сложности задачи поиска ближайшего вектора в решётке, связанной с теоретическими основами постквантовой криптографии;
— доказательство гипотезы Эрхарта об объёме выпуклых тел;
— решение трёх задач Эрдёша из теории Рамсея и экстремальной теории графов.
Особенно показателен результат по упаковке сфер. Авторы сборника называют его первым с 1978 года улучшением общей экспоненциальной оценки для пространств высокой размерности. Это не означает, что Astra решила знаменитую задачу упаковки сфер во всех измерениях, но она продвинула фундаментальную границу, которая почти полвека оставалась неподвижной.
Не просто «поверьте нейросети»
Самая важная часть публикации находится не в пресс-релизе, а на GitHub. Для каждого результата OpenAI опубликовала формализацию на языке Lean 4 — системе компьютерной проверки доказательств. Репозиторий открыт, содержит отдельные файлы для всех десяти результатов и инструкции для их независимой сборки.
По версии OpenAI, сама Astra нашла математические идеи и доказательства. Затем люди при помощи той же модели превратили рассуждения в научные рукописи, после чего Astra формализовала результаты в Lean. Компания подчёркивает, что люди отвечают за корректность опубликованного материала, но авторство математических аргументов приписывается модели.
Lean действительно позволяет проверить, что формальное доказательство логически следует из указанных определений, аксиом и ранее доказанных теорем. Но это не волшебная печать «истина». Специалисты всё ещё должны удостовериться, что формальная формулировка точно соответствует исходной математической задаче и что в зависимостях не спрятаны лишние предположения. Сама документация Lean отдельно подчёркивает различие между проверкой доказательства и проверкой смысла доказанной формулы.
Поэтому правильная формулировка сейчас звучит так: OpenAI представила десять воспроизводимых и машинно проверяемых кандидатов на крупные математические результаты. Превращение корпоративной публикации в общепризнанную математику потребует независимой проверки исследователями соответствующих областей.
Математика за $2000?
Наиболее эффектная цифра в сообщении OpenAI — примерно $2000. По оценке компании, столько стоили бы токены, потраченные Astra на поиск всех десяти решений, при тарификации API другой модели OpenAI под названием Sol.
Но это не означает, что десять научных открытий обошлись компании в две тысячи долларов. В сумму не входят обучение и разработка Astra, инфраструктура OpenAI, подбор задач, работа исследователей, подготовка 249-страничной рукописи и формальная проверка результатов.
Тем не менее даже с этой оговоркой цифра впечатляет. Если результаты подтвердятся, речь идёт не только о росте интеллектуальных возможностей моделей. Резко падает стоимость перебора гипотез, неудачных направлений и длинных цепочек рассуждений — той части научной работы, на которую у человека могут уходить годы.
Astra пока не выпущена и неизвестно, под каким названием она доберётся до пользователей. Но OpenAI уже показала её предполагаемую специализацию: не отвечать на вопросы быстрее человека, а неделями или месяцами автономно исследовать пространство решений.
До сих пор нейросети в математике в основном доказывали, что умеют сдавать экзамены. Теперь начинается гораздо более неприятный для человеческого самолюбия этап: они претендуют на участие в создании знаний, которых до них не существовало.
Сообщить о независимой проверке доказательств Astra
#ai @digitaltimeslv
Original in Telegram: https://t.me/digitaltimeslv/10063