Математики требуют объяснений от OpenAI: компания опубликовала 722 рукописи

Спор об объяснениях. По словам математика Брины Кра, около 40 участников августовской встречи просили OpenAI публиковать объясняющие работы вместо блогов и твитов. Кра считает, что компания проигнорировала этот совет.

1 августа OpenAI опубликовала 10 результатов внутренней версии Astra и сообщила о Lean-сертификате для каждого аргумента. Lean проверяет, что шаги формального доказательства следуют из заданных правил. В октябрьском каталоге формализация есть у части работ, а неформализованные результаты OpenAI публикует с предупреждением о возможных ошибках.

Материалы для проверки. В репозитории openai/math лежат обзор overview.pdf, карта работ CONTENTS.md, а в preprints/ находятся PDF, исходники и инструкции сборки. Компания также опубликовала 10 сокращённых изложений рассуждений модели, включая результаты о показателе иррациональности π и гипотезах Mahler.

Для проверки примера OpenAI предлагает установить comparator, landrun и lean4export в PATH. Затем из каталога lean/ последовательно выполнить:

``` lake update lake exe cache get lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json ```

Модели предложили около 4 000 задач. По данным OpenAI, в среднем результат потребовал вычислений, эквивалентных 3 часам ChatGPT Pro thinking. Результаты создала внутренняя невыпущенная модель, поэтому переносить их на доступный ChatGPT оснований нет.

После более 600 ответов математиков консультативная группа IAS 29 сентября рекомендовала публиковать результаты в научных репозиториях вне контроля ИИ-лабораторий. Группа также предложила раскрывать модель, промпты, время и стоимость вычислений. OpenAI обещает сохранять предыдущие версии работ при исправлениях.

Первоисточники: [репортаж WIRED от 6 октября](https://www.wired.com/story/openai-is-pissing-off-a-bunch-of-mathematicians-again), [работы и инструкции OpenAI](https://github.com/openai/math).

OpenAI работает над выпуском модели, которая создала опубликованные результаты.