AREX Feed Article
Hugging Face 将 OpenAI 公开数学题变成 369 个开源 RL 环境，并自述「早期且粗糙」
2026 年 10 月 11 日 14:31 UTC（北京时间 22:31），Hugging Face 联合创始人兼 CEO Clement Delangue 在 宣布，Hugging Face 把 OpenAI 的数学题变成了平台上的开源强化学习（RL）环境，帖文中的链接指向数据集 。他写道，这就是研究发布变成「人人可用的可执行训练基础设施」时的样子，同时自述发布「早期且粗糙」——验证器只接受与原始形式化完全一致的答案，数学上等价的证明可能得 0 分。
同日 16:11 UTC，Fathom News 刊发，补充了一层机制细节：这批环境的验证层由 Hugging Face 自行重建，而非复制 OpenAI 的版本；报道称，开发者因此无需 OpenAI 的专有技术栈，就能在可验证的数学任务上训练推理模型。数据集卡片则显示，369 个环境各自是一个可运行的任务——一个 Lean 定理、一处留空的证明位置和一套判定程序。
从 openai/math 到 Lean 沙箱：把 sorry 换成证明
帖文附带的截图给出了数据集页面的样子：顶部标注「RL Environment」，许可证为 Apache-2.0，标签里列着 harbor、reinforcement-learning、code-agent、lean4、mathlib；查看器中的 test 分割有 369 行，卡片标题是「openai/math as Harbor environments」。
数据集卡片把来源写得很具体：OpenAI 的 openai/math 发布（commit adc7f12）把 405 项结果形式化为 Lean 命题；Hugging Face 把它们移植成 Harbor 环境，被收入的 369 个，官方证明都能在环境里通过端到端验证，覆盖 214 个结果族、17 个领域。其余 36 个被逐个列出原因：21 个的官方证明用到了沙箱里没有的 Lean 库，10 个的证明构建需要超过 8 GB 内存，2 个因定义编译方式不同、精确匹配检查失败，2 个评分未跑完，另有 1 个按设计排除。卡片写明，这轮验证由卡片作者自己逐一运行 Harbor 的 oracle 完成。
每个任务是一个 Lean 4 沙箱：预装 Mathlib、不联网，定理以 OpenAI 的原始语句给出，证明位置写着 sorry。在 Lean 里，sorry 是省略证明的占位符：文件能编译，但等于什么都没证明；智能体要做的是把每个 sorry 换成真正的证明。完成后，另一个全新沙箱里的 Comparator（Lean FRO 的证明检查器）负责核对。OpenAI 的官方证明充当参考解，由 Harbor 的 oracle 在运行时从 GitHub 取回，不随数据集分发，智能体全程看不到。仓库里还有 registry.json（openai-math@1.0）、manifest.parquet、生成器与评分脚本；打包、验证器和生成器按 Apache-2.0 授权，Lean 语句照原样复制自 openai/math（© OpenAI）。
要跑起来，需要 Harbor 0.24+、Daytona 后端，以及运行智能体所需的凭证；每个任务提供 4 个 CPU、8 GB 内存、10 GB 磁盘和 4 小时时限；共享沙箱镜像约 9 GB，构建大约要一小时。
奖励只有 1 和 0：验证器如何判定
Fathom 把 RL 环境描述为让模型反复尝试任务、按可验证的得分调整参数的结构化设置；这批环境里负责判分的程序称为验证器（verifier），判定规则只有三条：定理保持 OpenAI 的原始语句不变，证明只使用 Lean 的标准公理（propext、Quot.sound、Classical.choice，不允许残留 sorry，也不允许引入新公理），且 Lean 内核接受。三条都满足得 1 分，否则 0 分。
严格性的后果，卡片自己写明了：用不同定义或等价表述写出的正确证明得 0 分；部分进展——有用的引理、特例的证明、思路正确但留有缺口的证明——得 0 分；不以完整证明收尾的创造性方法同样什么也得不到。卡片承认，这让判定很难被钻空子，但也是这批任务的真实限制。
卡片还记录了一轮反作弊测试：以各种方式试图欺骗验证器的提交——伪装成多种样式的 sorry、伪造公理、native_decide、弱化语句、重定义定义、植入奖励文件、在评分期间运行的代码、把验证器磁盘塞满的构建——全部得 0 分；什么都不做的智能体也是 0 分。评分一份被接受的证明，中位耗时约 8 分钟。
Fathom 的判断：被低估的正确答案与需要放宽的匹配逻辑
Fathom 在报道里给出了一个时间上的对照：过去，闭源实验室发表基准论文、却不放出底层验证器代码之后，独立团队往往要花数月才能重建出可比的 RL 环境；而当题目本身已经公开，从基准到可用的训练环境可以在数天内完成。
报道同时指出限制的另一面：严格匹配会让表述不同但正确的答案失败，从而低估模型的真实能力。要让这批环境在规模上可靠地衡量推理进展，报道认为下一步是放宽匹配逻辑，例如用一个次级模型判断等价答案。
帖文下的讨论：严格判定与训练信号
发布四个多小时后，帖文有 629 个赞、21,634 次浏览。回复与引用转发里，几位用户围绕判定规则给出了各自的解读。
X 用户 写道：「研究以可运行环境的形式发布，而不只是一份 PDF，这个方向非常好；希望之后每个新基准发布都能附带一个。」
写道：「不被支持的证明和错误的证明应该是两种结果。一个 0 掩盖了这个区别。」
则点出了训练层面的后果：「如果策略把定理等价地重述并给出证明，这个 0 在 RL 里会被读成错误，模型会被推回参考表述。作为早期版本没问题，但还不是我会用来报告分数的东西。」
标注为实验性：几乎每个任务都预期 0 分
卡片开头的警示写着：这是实验性发布，建立在一个本身很新、尚未经过独立评审的研究发布之上；「对任何得分为 1 的证明，先读一遍再依赖它。」卡片还在「污染」条目下注明，命题与证明自 2026 年 10 月 6 日起已经公开；在「难度」条目下写道，这些是开放研究问题，预期几乎每个任务都会得 0 分。
卡片自己写道，对于开放研究问题，一种能承认任何有效解法——包括创造性重构和部分进展——的更通用奖励函数会是更好的训练信号。当前采用严格检查的理由是它精确、无法被欺骗；卡片请使用者把这一选择看作「这个设计空间的一端」。