Вчера OpenAI выпустила 722 рукописи по ИИ-математике за один раз, и только что она отозвала 3 из них.
Причина проста: был неправильно написан знак плюс-минус.
Только что OpenAI опубликовала свой первый журнал обновлений в репозитории openai/math. Журнал показывает, что OpenAI отозвала 3 рукописи, исправила 14 и обновила ссылки ещё для 13. Общее количество рукописей в репозитории сократилось с 722 до 719.
Один знак плюс-минус обрушил три статьи
Три отозванные статьи все связаны с гипотезой Ходжа, одной из проблем тысячелетия:
Algebraicity of Weil classes on split abelian eightfolds
Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
The rational Hodge conjecture for products of K3 surfaces
Проблема заключается в первой статье. В примечании об отзыве OpenAI написала, что в ключевом аргументе статья записала знак некоторой геометрической операции как +1, тогда как согласно собственному соглашению статьи он должен быть -1.
https://github.com/openai/math/blob/main/history.md
Плюс против минуса — это огромная разница. Счёт, который должен был сократиться и в конечном итоге стать нулевым, стал ненулевым числом. Классическая теорема, на которую опирается статья, имеет в качестве предварительного условия именно то, что этот счёт должен быть нулевым. Поскольку предварительное условие не выполняется, вся последующая конструкция теряет опору.
Две другие статьи обе заимствовали эту конструкцию, поэтому они также были отозваны.
Однако во всех трёх примечаниях об отзыве OpenAI подчеркнула одну и ту же фразу: отзывается доказательство, что не означает, что сами эти математические утверждения неверны. Исходные рукописи также не были удалены и всё ещё могут быть просмотрены по архивным ссылкам.
Эти три статьи все принадлежат семейству результатов репозитория № 032, то есть ранее наиболее внимательно отслеживаемым результатам, связанным с гипотезой Ходжа.
После отзыва название этого семейства также изменилось: с «Hodge and Kuga–Satake results for all projective K3 surfaces» на «the rational Hodge conjecture for CM abelian varieties».
Иными словами, часть выводов, касающихся поверхностей K3, была удалена из списка. Основной вывод этого семейства, а именно доказательство рациональной гипотезы Ходжа для всех комплексных CM абелевых многообразий, всё ещё сохраняется, и новая версия этой статьи лишь обновила ссылки.
Стоит упомянуть, что статья с ошибкой датирована 18 сентября, что делает её одной из самых ранних партий рукописей в репозитории. От её даты до публичного выпуска прошло почти три недели, и она была отозвана в течение одного-двух дней после публикации. Что касается того, кто обнаружил ошибку, OpenAI не сообщила.
Ещё 14 статей были пересмотрены
Помимо отзывов, OpenAI также пересмотрела 14 рукописей, включая исправление доказательств, корректировку формулировок выводов и уточнение предварительных условий и зависимостей.
Эти 14 касаются высот Липшица и модели Ашкина–Теллера в статистической физике (4 статьи), программы минимальных моделей Кэлера и обильности в комплексной геометрии (6 статей), симплектической геометрии (2 статьи), общих вычислений для жидкостей Навье-Стокса (1 статья) и одной статьи о формуле BSD, из которой были удалены устаревшие ссылки.
Одна правка весьма показательна. Семейство результатов № 342 утверждало, что доказывает гипотезу «совместимости tame pushforward», предложенную Саймоном Дональдсоном. Основной вывод не изменился, и существует формализация на Lean. Но более сильный побочный вывод в статье был признан преувеличенным: в пересмотренной версии он сужен до конкретного случая, а также добавлен пример, показывающий, что в общем случае он не выполняется.
Уровень формализации: 42%
Обновление также добавило 6 формализаций на Lean и 5 дополнительных вспомогательных результатов. Согласно подсчётам OpenAI, основные результаты 300 рукописей теперь формализованы, что составляет около 42% от всех 719.
Среди недавно добавленных формализаций несколько имеют значительный вес, например, 103-е семейство достижений в теоретической информатике, утверждающее, что доказало полную дерандомизацию вычислений в логарифмическом пространстве (L = RL = BPL).
Следует отметить, что «около шестидесяти процентов», о которых мы сообщали ранее, подсчитывались по семействам достижений, то есть если хотя бы одна статья в семействе сопровождается формализацией, она учитывается; 42%, объявленные OpenAI, подсчитываются по отдельным основным результатам, что лучше отражает фактическую долю, проверенную компьютером строка за строкой.
Там, где возникают ошибки, нет надзора Lean
Сравнение с каталогом репозитория выявляет закономерность: содержание, которое было отозвано и существенно пересмотрено на этот раз, почти всё относится к частям без формализации на Lean.
Это также подтверждает более раннее предупреждение математического сообщества: результаты, не прошедшие формализацию и рецензирование, в настоящее время можно рассматривать только как «утверждения».
К счастью, эта работа над ошибками была проведена довольно надлежащим образом: ошибки были чётко указаны, цепочка зависимостей объяснена, а старая версия сохранена для справки, что соответствует принципу «исправление с сохранением следа», рекомендованному Консультативной группой по математике и искусственному интеллекту Института перспективных исследований.
Однако всего через два дня после обнародования более 700 рукописей пришла первая работа над ошибками. Весьма вероятно, что она не будет последней.
Эта статья взята из публичного аккаунта WeChat «Machine Heart» (ID: almosthuman2014), редактор: Panda
