1 августа компания OpenAI опубликовала доказательства для десяти математических задач, которые оставались открытыми как минимум с 2016 года.
Решения получила внутренняя версия Astra — так разработчик ChatGPT назвал свою следующую крупную модель. По подсчетам OpenAI, объем потраченных на поиск ответов токенов обошелся бы примерно в $2000 по тарифам API для Sol.
Рукописи готовили люди с той же моделью, после чего она формализовала каждое доказательство в Lean — языке для машинной проверки теорем. Все сертификаты и записи рассуждений фирма выложила в открытый доступ.
Astra станет отдельным классом моделей наряду с Sol, Terra и Luna, пишет The Information. По данным издания, в OpenAI пока не решили, выйдет ли она как GPT-6 или как версия внутри линейки GPT-5. Дату релиза представители компании также еще не назначили.
26 июля гендиректор фирмы Сэм Альтман показывал Astra политикам и регуляторам в Вашингтоне. Модель может стать первой, которую проверят по новым правилам администрации президента США Дональда Трампа. В соответствии с ними ИИ-разработчики должны передавать новые системы на оценку федеральным властям до публичного запуска.
Какие задачи решила Astra
В число ключевых результатов вошла конструкция, доказывающая существование несофических групп. Это закрыло центральный вопрос, который математики не могли решить с 1999 года, когда Михаил Громов ввел понятие софичности.
Среди других достижений — опровержение гипотезы жесткости Конна о фон-неймановых алгебрах, решение гипотезы Эрхарта об объеме, а также задачи Эрдеша №183 о мультицветных числах Рамсея. Astra также получила новые нижние оценки сложности вычисления перманента арифметическими схемами и доказала теорему о параллельном повторении для квантовых игр двух игроков.
Кроме того, модель улучшила верхние оценки плотности при упаковке сфер в высоких размерностях до порога Кона–Элкиса и усилила границы для двоичных кодов при любом заданном минимальном расстоянии.
Математик Манчестерского университета Томас Блум назвал опубликованные результаты «большой новостью» и «весомым шагом» в области конструкций.
Однако модель справилась не со всеми задачами. Ноам Браун, соавтор технологии рассуждений Astra, сообщил, что в OpenAI пробовали подступиться и к другим крупным проблемам, но безуспешно. Модель не смогла решить «задачи тысячелетия» — сем вопросов, которые в 2000 году Математический институт Клэя назвал главными в математике, пообещав $1 млн за решение каждого.
Напомним, в июле Claude от Anthropic опроверг математическую гипотезу 1939 года.