6 октября OpenAI открыла на GitHub сборник из 719 математических рукописей, которые написала внутренняя модель компании. Какая именно из моделей OpenAI стоит за ними, в репозитории не уточняется. В рукописях заявлены результаты по открытым задачам из теории чисел, алгебры, геометрии и математической физики. Через сутки Ассоциация за человеческую математику (AHM) призвала коллег прекратить сотрудничество с компанией.
Что опубликовала OpenAI
Рукописи сгруппированы в 372 семейства результатов, сообщается в репозитории OpenAI на GitHub. Модели дали около 4000 задач, и в среднем на каждый результат ушло три часа «размышлений» уровня ChatGPT Pro. Формальная проверка в системе Lean есть только у 300 рукописей из 719, это около 42%. Сама OpenAI предупреждает, что результаты находятся на разных стадиях проверки. Уже 7 октября компания отозвала три рукописи из-за ошибки в знаке, которая сломала рассуждение сразу в трёх связанных работах, и исправила ещё 14.
За что критикуют
Заявление AHM опубликовал у себя в блоге математик Теренс Тао с пометкой «гостевой пост». «Выложить больше 700 файлов разом — это демонстрация силы, а не научной работы», — говорится в заявлении. Авторы отвергают мысль, что такой выпуск двигает математику вперёд, и призывают коллег прекратить работать с OpenAI. По данным TechCrunch, компания выполнила не все рекомендации консультативной группы по математике и ИИ при Институте перспективных исследований в Принстоне. Ход рассуждений модели приложен лишь к 10 рукописям из 719. Сам Тао, как пишет издание, тоже раскритиковал такой подход: по его словам, задачи решают «ИИ-промптеры», которым нет дела до самой области.
Что с задачей на миллион
Отдельный спор идёт вокруг доказательства для уравнений Навье — Стокса, которое OpenAI заявила ещё в сентябре. Это одна из «задач тысячелетия» с премией в миллион долларов. По данным TechCrunch, математики из Кембриджа и Королевского колледжа Лондона нашли как минимум два расхождения между текстом этого доказательства и его версией на Lean. Это не опровергает результат, но ставит под сомнение, можно ли доверять модели, которая сама переводит своё доказательство на язык формальной проверки. Рецензирование это доказательство пока не прошло.
