Hugging Face 将 OpenAI 数学成果转为开源 RL 训练环境
精选理由
Hugging Face 把 OpenAI 的数学题搬进了开源 RL 环境，405 道 Lean 形式化题自动判分，接进训练流程就能让模型自己刷题学证明。
Hugging Face 把 OpenAI 近期公布的数学成果改造成开源强化学习环境，共包含 369 个任务、405 道形式化数学题和 214 个题型。每个任务提供一份带 sorry 的 Lean 题面，模型需要补全成完整证明。环境内置独立沙箱中的 Lean 判分器，自动编译验证，答对记 1、答错记 0，reward 可直接用于训练。目前 verifier 只认原始形式化写法，等价证明可能被误判，项目还处于早期版本。
原文 · AIGCLINK
Hugging Face把OpenAI前两天放出来的那批数学成果转成了开源强化学习环境，大家可以拿去训练模型
挂进你的训练流程，让模型自己刷题进化，先挑会做的刷，刷不动的攒着慢慢练
369个任务、405道形式化数学题、214个题型。每个任务给一份带`sorry`的Lean题面，AI要把它补成完整证明，独立沙箱里的Lean判分器自动编译验证，对1错0，reward直接拿去训练
不过还处于早期版本，verifier目前只认原始形式化写法，等价证明也可能会被误伤，当练兵场来用
#RL训练环境
