OpenAI отзывает три математических результата

Так значит, три отозванных доказательства — это те, что были без верификации в Lean?

Если так, почему они смешали доказательства, проверенные в Lean, и доказательства на естественном языке?

Я как раз об этом думал, читая блог Ааронсона:

https://scottaaronson.blog/?p=10169

Или, по крайней мере, мы почти уверены, что это доказательство! Есть сертификат Lean, как и для некоторых других из 372 прорывных результатов (не для всех). Но также похоже, что ни один человек пока не понял почти ни одного из этих доказательств.

Очевидным шагом было бы выпустить их в ДВУХ частях: те, что проверены, и те, что могут содержать хорошие идеи, но также и ошибки. Предположительно, проверка последних людьми обойдётся гораздо дороже.

Думаю, при более близком рассмотрении многие из этих полностью сгенерированных ИИ доказательств развалятся. Даже в Lean можно построить теории, которые компилируются, но при этом утверждают не совсем то, что вы на самом деле имели в виду. Просто объём доказательств настолько ошеломляюще велик, что, вероятно, пройдут годы, прежде чем мы найдём проблемы, как в случае с гипотезой abc.

Статья о преодолении O(n log n) для целочисленного умножения тоже кажется мне довольно подозрительной, не уверен, но выглядит слишком хорошо, чтобы быть правдой; чувствую, что там должна быть какая-то тонкая ошибка. Может, это просто я недолюбливаю эти маленькие числа в статье, но это кажется неправильным, даже неестественным! Я был бы так же скептичен к статье по физике, которая утверждает, что может превысить скорость света на крошечную долю. Нет причин, по которым n log n был бы здесь естественным пределом, но я вижу несколько хороших интуиций, так что наличие чего-то другого, что не представимо в элегантной форме, кажется мне очень «нематематичным».

Если вы публикуете такой дамп, всё это должно быть формализовано — материала слишком много, чтобы проверять вручную, к тому же он написан ИИ, что затрудняет чтение по сравнению с человеческой работой.

Вот это таймлайн: модель OpenAI настолько хороша, что публикует сотни математических статей.

Последняя модель даже находит ошибки в ранее опубликованных математических статьях!!!*

* пока что только математические статьи OpenAI были ошибочными и требовали отзыва.

Вот как это выглядит, когда практики программной инженерии встречаются с математикой. «openai/math релиз 1.3.42: отозваны статьи 139 и 140, исправлена ошибка со знаком в статье 47, восстановлена ранее отозванная статья 85, отрефакторены аргументы в статье 101».

Мне любопытно узнать, был ли отзыв вызван тем, что настоящий математик посмотрел на статьи и заметил ошибки, или они прогнали модель для вычитки, что, вероятно, не в первый раз, поскольку они наверняка делали это перед публикацией. Оба варианта имеют интересные последствия.

3 ошибки (пока что) из ~400 — всё ещё довольно хороший процент попаданий.

Итак, математика вступила в фазу «кидай всё на доску и смотри, прилипнет ли»..

Это просто OpenAI снова крадёт работу.

Я не против того, что они публикуют. У меня нет проблем с процессом и тем, как они в нём взаимодействуют. Я в восторге от того, что они на самом деле выступают хранителями этих работ.

Но при всём этом они должны платить людям, проверяющим задачи. Что действительно задевает, так это то, что мы знаем: всё, опубликованное в процессе проверки этого, будет высосано в следующую сессию обучения.