OpenAI публикует результаты исследований по математике, подтверждённые формальными доказательствами в Lean

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

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

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

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

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

По данным openai.com.