OpenAI опубликовала 722 математические рукописи от закрытой модели

Что произошло

OpenAI опубликовала на GitHub 722 математические рукописи, созданные внутренней моделью, которую компания пока не выпустила. Представитель OpenAI заявил, что почти всё собрание было получено одним ИИ-агентом по одному запросу, хотя некоторые материалы могли потребовать нескольких попыток.

Компания сообщила, что предложила модели около 4 000 задач и отобрала для публикации результаты, которые сочла достаточно значимыми.

Что известно о материалах

Работы распределены по 372 семействам связанных результатов. В одно семейство могли входить основная теорема, сопутствующие аргументы, следствия или альтернативные доказательства. Поэтому 722 рукописи не означают 722 решённые задачи.

В среднем на один результат приходился объём вычислений, эквивалентный примерно трём часам размышлений ChatGPT Pro. Для сравнения, в предыдущем заявлении о задаче Навье—Стокса участвовали 10 000 взаимодействующих агентов, работавших 88 часов.

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

Почему выводы пока не подтверждены

Математик MIT Andrew Sutherland заявил Scientific American, что до публикации модели и независимого воспроизведения результатов утверждения о решении задач одним агентом следует считать непроверенными.

OpenAI признаёт, что не для всех рукописей существуют формализации в Lean и что в некоторых неформализованных результатах могут быть ошибки. Успешная проверка в Lean подтверждает лишь соответствие доказательства формулировке, записанной в этой системе. Она не показывает, соответствует ли формулировка исходной задаче, а также является ли результат новым или значимым.

В исходном материале также отмечается, что репозиторий openai/math не принимает сообщения в Issues и ранее не принимал запросы на изменение. Это ограничивает возможности для отправки формализаций и обсуждения опубликованных работ.

Контекст проверки

Среди приведённых примеров упоминается доказательство утверждения о том, что хроматическое число плоскости не меньше 6. Автор исходного материала назвал такую математику совершенно невероятной и чуждой для понимания.

Заявление OpenAI может стать значимым прорывом для математики, но без публикации модели и возможности воспроизвести результаты его масштаб и корректность остаются открытыми вопросами.