OpenAI открыла на GitHub математику невыпущенной модели

Каждый новый математический результат внутренней модели OpenAI в среднем потребовал около трёх часов размышлений ChatGPT Pro, если пересчитать затраченные вычисления в единицы, понятные подписчикам. Эти оценки компания приложила к большому набору результатов, о котором рассказала в блоге OpenAI. Саму модель пока не выпустили.

Коротко

• OpenAI выложила в репозиторий openai/math на GitHub широкий набор новых математических результатов невыпущенной модели вместе с правилами, по которым статьи будут исправлять и цитировать.
• Многие доказательства формализованы в Lean, где правильность проверяет компьютер. По данным Testing Catalog, за время оценки модели дали около 4 000 задач, и почти все результаты получены одной процедурой.
• Рассуждения модели раскрыты только в 10 сводках, а срок выпуска самой модели и подробности обещанных воркшопов и конференций OpenAI пока не называет.

Если вы не следили: математика давно служит лабораториям ИИ удобным полигоном, потому что доказательство либо верно, либо нет, и это можно проверить. Чем серьёзнее такие результаты, тем острее вопрос, как показывать их математикам, чтобы им можно было доверять и на них можно было ссылаться. На этом вопросе и построен нынешний релиз OpenAI.

Средний результат стоил около трёх часов размышлений ChatGPT Pro

Вместе с результатами OpenAI выложила в репозиторий описание того, как они были получены. Там есть оценки затраченных вычислений в пересчёте на использование Pro в ChatGPT, статистика по числу задач, за которые бралась модель, и 10 сводок её рассуждений. В среднем на один результат ушло столько вычислений, сколько примерно три часа размышлений ChatGPT Pro.

Testing Catalog, ссылаясь на репозиторий, добавляет два уточнения. За время оценки модели задали примерно 4 000 задач, а подавляющее большинство результатов получено одной и той же процедурой с невыпущенной внутренней моделью OpenAI. В блоге компании она названа просто внутренней frontier-моделью, то есть самой передовой из тех, что OpenAI пока держит у себя.

Формат релиза OpenAI обсуждала с группой при Институте перспективных исследований

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

Итогом стал репозиторий на GitHub с протоколами для правок статей и для цитирования. По словам OpenAI, параллельно она ищет площадки, которые держит само сообщество и которые соответствуют рекомендациям комитета. В следующих релизах компания обещает улучшать сами статьи: ссылки на литературу, математическое изложение и подачу результатов, чтобы их было проще понять.

Многие доказательства в репозитории проверены компьютером в Lean

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

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

OpenAI обещает деньги на воркшопы и готовит модель к выпуску

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

Параллельно OpenAI работает над тем, чтобы ответственно выпустить модель, получившую эти результаты, и напрямую дать учёным передовые возможности. В компании объясняют, что поэтому продолжают проверять внутренние frontier-модели на математике и других науках: так быстрее появляются инструменты для этих областей. Стандарты раскрытия крупных научных результатов OpenAI обещает обновлять с учётом отзывов сообщества.

На наш взгляд, 10 сводок рассуждений на такой объём результатов маловато, чтобы понять, как модель на самом деле приходит к доказательствам. В анонсе не сказано, сколько из примерно 4 000 задач, о которых пишет Testing Catalog, закончились результатом, и формализованы ли в Lean все доказательства, а не только «многие». Мера «три часа ChatGPT Pro», судя по всему, удобна для сравнения с подпиской, но не показывает, сколько вычислений стоит за ней в железе.

Когда модель дойдёт до учёных

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