OpenAI заявила, что её внутренняя модель получила новые результаты в математике, и 6 октября опубликовала материалы на GitHub. В каталоге — 722 рукописи, объединённые в 372 группы связанных результатов. Компания приглашает исследователей изучать и развивать эту работу.
Публикация последовала за несколькими месяцами споров о том, как ИИ-компаниям сообщать о математических открытиях. Математики признают, что модели могут помочь исследованию сложных задач. Их беспокоят качество объяснений, возможность независимой проверки и то, насколько корректно компании учитывают вклад людей.
В центре дискуссии — не только вопрос, способна ли модель выдать доказательство. Важно понять, может ли научное сообщество проверить его, разобраться в логике и безопасно использовать результат в дальнейшей работе.
Почему математики критикуют формат публикации.
Короткий анонс не заменяет разбор доказательства
До публикации новой подборки некоторые математики просили OpenAI сопровождать результаты полноценными научными текстами, а не ограничиваться постами и короткими объявлениями. По словам математика Брины Кра, участники встречи с компанией хотели получить объяснения, которые позволят специалистам осмыслить и использовать выводы. OpenAI сообщила, что разместила материалы на GitHub, добавила правила для обновлений и цитирования, а также планирует улучшать изложение и работу со ссылками в будущих релизах. Это шаг к более систематичной публикации, но проверка содержания всё равно остаётся за научным сообществом.
Машинная проверка полезна, но не отвечает на все вопросы
Часть доказательств OpenAI представила в формализованном виде на Lean — языке, который позволяет проверять математические утверждения с помощью компьютера. Компания обещает пополнять репозиторий такими формализациями. Однако формальная проверка касается конкретного утверждения, записанного в системе, и зависит от того, насколько точно оно соответствует математическому тексту. Она не заменяет проверку предпосылок, новизны результата и его связи с предыдущими исследованиями. Поэтому нужно читать и доказательство, и описание того, что именно было формализовано.
Нужно раскрывать, как получен результат
В первой публикации OpenAI указала некоторые сведения о процессе: выложила десять сокращённых описаний рассуждений модели, оценки вычислительных затрат и статистику по задачам. Компания сообщила, что в среднем на один результат затрачивались вычисления, эквивалентные примерно трём часам работы ChatGPT Pro. Консультативная группа по математике и ИИ при Институте перспективных исследований также рекомендует публиковать понятные научные тексты, сведения о моделях и методах, данные о формализации и ссылки на предыдущие работы. Группа отдельно уточняет: её консультации не означают одобрения конкретного релиза или оценки его научной значимости.
Споры об авторстве требуют аккуратного изложения
В материале WIRED описан конфликт вокруг работы математика Тристана Бакмастера и сотрудника Anthropic Левента Алпёге. Бакмастер утверждал, что OpenAI попыталась опередить их работу, и заявил, что исследователь компании Себастьян Бубек намекал на исключение Алпёге из будущей статьи. Бубек ранее отрицал, что просил не указывать Алпёге соавтором. Эти утверждения остаются предметом спора сторон. Их нельзя пересказывать как установленный факт кражи или доказанного давления. Но сам конфликт показывает, почему исследовательские команды должны заранее договариваться о том, как фиксировать вклад участников и использование ИИ-инструментов.
«Математика через твиты и пресс-релизы — не тот способ поддерживать научную экосистему».
Брина Кра, математик Северо-Западного университета
Как читать доказательство, созданное ИИ
- Уточните, какое именно утверждение доказывает рукопись и при каких условиях.
- Проверьте, является ли текст препринтом, прошёл ли он рецензирование и обновлялся ли после публикации.
- Найдите формализацию в Lean, если она есть, и выясните, какую часть доказательства она покрывает.
- Сопоставьте математическое изложение с формальным доказательством: формализация должна относиться к тому же утверждению.
- Проверьте ссылки на предыдущие работы и оцените, описана ли новизна результата.
- Посмотрите, раскрыты ли модель, методы, вычислительные затраты и ограничения.
- Проверьте историю изменений и исправлений в репозитории.
Что именно опубликовала OpenAI?
Компания разместила на GitHub математические рукописи и сопутствующие материалы, созданные внутренней моделью. В каталоге указаны 722 рукописи, объединённые в 372 группы связанных результатов.
Все ли доказательства проверены в Lean?
Нет. OpenAI пишет, что добавила формализации многих доказательств и будет пополнять ими репозиторий. При этом компания отдельно предупреждает о возможных проблемах в результатах, которые пока не формализованы.
Значит ли публикация, что результаты прошли рецензирование?
Нет. Размещение на GitHub делает материалы доступными для изучения, но само по себе не подтверждает независимую экспертизу или принятие результата научным сообществом.
Что такое Lean?
Lean — язык формального доказательства. В нём математическое утверждение и шаги доказательства записывают в строгом виде, чтобы компьютер мог проверить их по заданным правилам. Проверка полезна, но важно убедиться, что формализованное утверждение соответствует содержанию статьи.
Почему учёные спорят об авторстве?
В исследовании могут участвовать несколько математиков, а ИИ-инструменты — помогать на разных этапах. В споре вокруг OpenAI, Бакмастера и Алпёге стороны по-разному описывали разговор о признании вклада. Этот эпизод подчёркивает необходимость прозрачных правил, но обвинения участников не следует выдавать за доказанные факты.
Каковы рекомендации консультативной группы по математике и ИИ?
Группа выступает за понятное научное изложение, корректные ссылки на предыдущую работу, раскрытие сведений о методах и формализации, а также поддержку мероприятий, где исследователи смогут разобраться в сложных результатах. При этом группа подчёркивает, что её консультации не являются подтверждением качества конкретной публикации.
ИИ может ускорить математику, но проверка остаётся частью науки
Публикация OpenAI показывает, что модели уже могут выдавать результаты, требующие внимания математиков. Следующий шаг — не просто увеличить число рукописей, а сделать их понятными, проверяемыми и связанными с предыдущими исследованиями. Для читателя практический критерий прост: оценивать не громкость анонса, а содержание доказательства, степень независимой проверки и прозрачность процесса. В SpeShu.AI можно сравнивать ответы нескольких ИИ-моделей и использовать их как вспомогательный инструмент при изучении сложных тем.