OpenAI выложила сотни математических результатов, полученных с помощью модели

По сообщению канала SeeAllochnaya, OpenAI запустила внутреннюю модель на наборе примерно из 4000 открытых задач. Автор публикации оценивает затраты на каждую как сравнительно небольшие: порядка трёх часов работы GPT Pro, а не запуск тысяч параллельных агентов. Это оценка из пересказа, а не воспроизводимая спецификация эксперимента.

Как утверждается в том же сообщении, модель получила 372 основных результата, после чего с её помощью подготовили 719 текстов: решения, дополнительные аргументы, следствия и альтернативные доказательства. Результаты выложили на GitHub. Примерно для 63% основных результатов, по данным публикации, есть также доказательства на Lean. Эта система проверяет, следует ли формальный вывод из заданных посылок; для оценки всей работы всё равно важно проверить формулировки и соответствие формализации исходной задаче.

Массив уже меняется: автор сообщения указывает, что три статьи были отозваны, а ещё 14 исправлены. Поэтому число опубликованных решений не стоит читать как число окончательно подтверждённых теорем. У отдельных результатов разная степень проверки, и исследователям предстоит разбирать их по одному, прежде чем опираться на них в новых работах.