Математические задачи в средах Harbor

Что внутри

Экспериментальный набор из 369 Harbor-сред с математическими задачами, перенесёнными из релиза openai/math (коммит adc7f12). В релизе 405 результатов формализованы как Lean-утверждения; в набор вошли среды, для которых официальное доказательство проверено от начала до конца. Авторы предупреждают, что релиз новый и не проходил независимую проверку, возможны шероховатости.

Что можно сделать

• Проверка моделей и агентов на математических доказательствах
• Оценка работы с Lean-формализацией
• Тестирование Harbor-сред для математики

Модели, обученные на нём

• ysh-david/david-testРазметка токенов 0

Как загрузить

from datasets import load_dataset

ds = load_dataset("FineEnvs/openai-math")