OpenAI опубликовала 722 математические работы, созданные внутренней ИИ-моделью

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

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

Коллекция включает PDF-файлы и исходные тексты работ, формализации многих доказательств на языке Lean, а также десять сокращённых описаний рассуждений модели. По данным компании, системе предложили около 4000 задач, а средние вычислительные затраты на один вошедший в каталог результат соответствовали примерно трём часам работы режима ChatGPT Pro.

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

Формат публикации подготовлен с учётом рекомендаций Консультативной группы по математике и искусственному интеллекту (AGMAI). Группа призывает лаборатории раскрывать сведения о применявшихся моделях, вычислительных затратах и процессе получения результатов, формализовать доказательства и обеспечивать их независимую проверку.