OpenAI 6 октября опубликовала 722 математические рукописи, созданные преимущественно внутренней ИИ-моделью. На следующий день компания отозвала три работы: ошибка знака сделала недействительным аргумент в одной рукописи и конструкцию, на которую опирались две другие.
В репозитории OpenAI осталось 719 рукописей, объединённых в 372 тематические семьи. Подавляющее большинство результатов модель получила в рамках одной и той же процедуры оценки. Для каждого результата в среднем потребовалось около трёх часов вычислений в режиме ChatGPT Pro, а всего модели предложили примерно 4000 задач. Использованная внутренняя модель пока не выпущена.
Почему результаты ещё требуют проверки
Материалы находятся на разных стадиях верификации. Формализации опубликованы для 300 из 719 основных результатов, или примерно 42%. Они выполнены в Lean — языке и программном инструменте для машинной проверки логической структуры доказательств. Остальные результаты приходится проверять традиционным способом.
Читайте также
Машинная проверка подтверждает корректность логических переходов внутри формализации, но математикам всё равно нужно независимо оценить исходные утверждения и допущения. Опрошенные The Verge (заблокирован в РФ) исследователи также отмечали, что в некоторых случаях формулировки, проверяемые кодом Lean, не вполне соответствовали утверждениям в сопровождающих рукописях.
Из-за объёма коллекции её оценка может занять годы, сообщили изданию математики.
Что исправила OpenAI
В журнале изменений компания сообщила об отзыве трёх рукописей и сохранила их прежние версии в истории репозитория. Ещё 14 работ пересмотрели: в них исправили доказательства и формулировки, уточнили условия применимости и зависимости, а также заменили одну устаревшую ссылку. В 13 других рукописях обновили ссылки на исправленные материалы.
OpenAI также добавила шесть формализаций и пять вспомогательных материалов. Представитель компании сообщил Retraction Watch, что ошибки обнаружили во время аудита. Новые ошибки OpenAI намерена оперативно исправлять, а рукописи — отзывать, если исправление невозможно.
Что это значит
- Перед использованием или цитированием результата математикам нужно проверить актуальную версию рукописи и историю исправлений.
- Для работы с формализацией необходимо сверить, что код Lean доказывает именно то утверждение, которое заявлено в тексте, с теми же определениями и допущениями.
- Число опубликованных рукописей нельзя считать числом подтверждённых открытий: формализации есть примерно для 42% основных результатов, а вся коллекция ещё требует независимой оценки.