OpenAI: внутренняя версия Astra с 10 математическими результатами

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

Компания указывает, что математические аргументы сгенерировала внутренняя версия Astra; люди редактировали рукописи, а затем модель формализовала аргументы в Lean‑сертификаты. В заявлении OpenAI приводится цитата: “Мы считаем, что атрибуция должна честно отражать то, как был получен результат: приписывать человеку авторство доказательства, полностью сгенерированного ИИ‑системой, означало бы искажать вклад системы и природу подлинной человеческой интеллектуальной работы”.

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

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

В документе перечислены и другие достижения в фундаментальной математике: построение не‑софической группы; улучшенные оценки для упаковки шаров в высоких размерностях; более строгие границы для бинарных и сферических кодов; новые нижние оценки в арифметической схемной сложности; результат по гипотезе Эрхарта об объёме; контрпример к гипотезе жёсткости Конна; новый результат по многоцветным числам Рамсея; и контрпримеры к двум гипотезам Эрдеша в экстремальной теории графов. В публикации отмечено, что практическое применение большинства этих результатов не является немедленным.

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

Публикация усилила обсуждение порядка рецензирования и атрибуции результатов, полученных с помощью систем машинного вывода. OpenAI сослалась на международные рекомендации по использованию ИИ в математике и указала, что берёт ответственность за корректность опубликованных материалов при одновременном указании вклада системы Astra в генерацию математических аргументов.