OpenAI залучила незалежну консультативну групу з дев'яти провідних світових учених для оцінки та оприлюднення досягнень своєї внутрішньої передової моделі штучного інтелекту. Компанія виклала в репозиторії на GitHub 722 формалізовані версії доведень, які можна перевірити за допомогою комп’ютера.
Кожна з публікацій присвячена розв'язанню окремої відкритої математичної задачі. Їх згенерувала внутрішня модель OpenAI, яку ще не випустили. Всі результати розробники об'єднали в 372 групи пов'язаних досліджень за різними розділами математики.
Частину доведень OpenAI представила мовою програмування Lean. Вона дозволяє формально записувати математичні доведення та перевіряти їхню правильність за допомогою комп’ютера, тому результати можна незалежно перевірити.
Разом із математичними результатами компанія опублікувала додаткову інформацію про роботу моделі. Зокрема, у репозиторії є 10 описів її логічних міркувань, статистика кількості спроб розв’язання задач і оцінка використаних обчислювальних ресурсів. Для отримання середнього результату модель використовувала обчислювальні ресурси, еквівалентні приблизно трьом годинам роботи ChatGPT Pro у режимі міркування.
Компанія планує надалі оновлювати репозиторій новими формалізованими доведеннями. OpenAI також обіцяє вдосконалювати математичний виклад, систему цитування та спосіб представлення результатів, щоб їх було легше оцінювати науковцям.
Розв'язання відкритих математичних задач свідчить про здатність ШІ будувати складні ланцюжки міркувань, а інструменти на кшталт мови Lean дозволяють чітко верифікувати ці доведення. Проте, як йдеться в публікації видання Nature Machine Intelligence, успіхи в математиці не означають надійності алгоритмів у медицині чи критичних системах. Оприлюднений масив даних від OpenAI демонструє безпрецедентний масштаб автоматизованих досліджень, але його реальна цінність для науки залежатиме від того, чи підтвердить незалежна перевірка вчених новизну та коректність цих результатів.
