OpenAI 26 октября опубликовала три научных результата, полученных внутренними ИИ-моделями, и пригласила внешних исследователей проверить и объяснить их. Компания отдельно подчёркивает: рукописи следует считать сырыми исследовательскими данными, а не уже признанными научным сообществом открытиями.
Заявленные результаты относятся к трём областям:
- Математика. Доказательство гипотезы о локальном сглаживании во всех размерностях, из которого, по утверждению OpenAI, следуют решения гипотез Кэкея и Штейна.
- Теория вычислительной сложности. Опровержение гипотезы экспоненциального времени, или ETH.
- Математическая физика. Доказательство существования ряда четырёхмерных квантовых теорий поля, включая квантовую хромодинамику, а также чистой теории Янга — Миллса.
Для математического результата OpenAI открыла текст, сгенерированный моделью, и формализацию в Lean. По данным компании, исходный ответ был получен 18 октября, а формальная версия — 19 октября.
Материалы по ETH также опубликованы: естественно-языковое доказательство получено 16 октября, а формализация в Lean — 17 октября. Разбор возглавят исследователи Рассел Импальяццо и Рамамохан Патури из Калифорнийского университета в Сан-Диего и Райан Уильямс из MIT. Импальяццо и Патури были среди авторов исходной гипотезы. Даже если результат подтвердится, он сам по себе не доказывает равенство P и NP и не обещает практического ускорения вычислений.
В физической части OpenAI пока не опубликовала полный комплект материалов. Группа под руководством лауреата Нобелевской премии Дэвида Гросса сначала подготовит собственное объяснение. Заявление о существовании чистой теории Янга — Миллса не следует путать с полным решением задачи тысячелетия: в ней требуется также доказать наличие массовой щели.
Компания предложила четыре правила работы с внешними группами:
- прозрачность без соглашений о неразглашении;
- отказ OpenAI от академического авторства результатов;
- признание вклада исследователей в проверку и объяснение;
- независимость и неоплачиваемое участие экспертов.
Наличие формализации в Lean означает, что компьютер может проверить корректность доказательства относительно записанного формального утверждения и использованных зависимостей. Оно не заменяет проверку того, что формальное утверждение полностью соответствует заявленной научной проблеме, и не подтверждает автоматически новизну, корректность исходных предпосылок и значение результата.
На момент проверки 27 октября независимые экспертные заключения ни по одной из трёх работ не опубликованы. OpenAI также не назвала сроки их появления, а без полного комплекта физической работы сторонние исследователи пока не могут оценить её целиком. Поэтому все три вывода сохраняют статус заявлений разработчика.
Пока никто не ответил. Начните обсуждение.