Hugging Face превратила 369 теорем OpenAI в задачи для обучения моделей

Hugging Face собрала из математических результатов, опубликованных OpenAI 6 октября, 369 открытых сред обучения с подкреплением¹, написал в соцсети X глава компании Клеман Деланг.

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

Предыстория: 6 октября OpenAI выложила 722 статьи, в которых её закрытая модель предлагает решения открытых математических задач, и математики разошлись в оценке. 405 результатов компания записала на языке Lean — это программа, которая проверяет каждый шаг доказательства, как компилятор проверяет код.

Как это работает: задачи собраны в формате фреймворка Harbor², каждая — одна теорема:

• Агент получает изолированную песочницу без интернета, где есть Lean 4 и библиотека Mathlib³, и четыре часа на работу.
• Теорема записана ровно так, как её сформулировала OpenAI, а вместо доказательства стоит заглушка: с ней файл проходит сборку, хотя ничего не доказано.
• Агент должен заменить каждую заглушку настоящим доказательством; эталоном служат доказательства OpenAI, но агенту их не показывают.
• Решение в отдельной чистой песочнице проверяет программа Comparator от разработчиков Lean: балл 1 дают, только если доказательство принято без заглушек и новых аксиом.

В цифрах:

• В набор вошли 369 теорем из 405 — только те, где доказательство самой OpenAI прошло ту же проверку, что ждёт агента.
• Теоремы относятся к 214 семействам результатов OpenAI из 17 областей математики.
• Каждой задаче нужны 4 процессорных ядра, 8 ГБ памяти и 10 ГБ диска.
• Медианное время проверки одного принятого доказательства составило восемь минут.

Детали: авторы набора сами пытались обмануть свою проверку: подсовывали ей заглушки в разных обличьях, поддельные аксиомы, ослабленные формулировки, файлы с заранее вписанным баллом и код, который запускается во время проверки. Все такие решения получили 0, как и агент, который ничего не делает. Заодно Hugging Face закрыла лазейку у OpenAI: в восьми её настройках проверки Comparator не сверял определения из формулировки теоремы, и решение могло их подменить. В наборе эти определения должны точно совпадать с исходными.

Но: авторы советуют ждать нуля почти на каждой задаче и сами перечисляют ограничения:

• Верное доказательство равносильного утверждения в другой формулировке или с другими определениями получает 0.
• Полезные леммы, частный случай или верная стратегия с пробелом в рассуждении тоже дают 0.
• Лучшим сигналом для обучения авторы считают награду за любое верное решение и частичный прогресс, но выбрали строгую проверку, потому что её не обмануть.
• Формулировки и доказательства открыты с 6 октября, поэтому новые модели могли видеть их при обучении.

5 октября Hugging Face показала, как обучать открытые модели прямо в агентах для программирования. Новый набор Деланг назвал ранним и сырым, но само направление считает захватывающим: «превращать открытые исследования в открытые среды, на которых любой может обучать более сильные открытые модели».