Hugging Face 把 OpenAI 数学题做成开源 RL 环境,Lean4 沙箱自动判分
_lewtun · x · 2026-10-11
Hugging Face CEO Clement Delangue 宣布将 OpenAI 公开的数学问题转化为 HF 上的开源 RL 环境（FineEnvs/openai-math 数据集，Apache 2.0）。
- 每道题要求用 Lean 4 + Mathlib 形式化证明，在独立沙箱中由 Lean FRO 的 Comparator 校验器判分，通过得 1 分、部分证明得 0 分；沙箱无网络访问。
- 项目尚早期粗糙：校验器只接受与原始形式化完全一致的证明，等价证明也可能得 0 分。
- 他认为这是值得兴奋的方向：把开放研究变成人人可用的可执行训练基础设施，用于训练更好的开源模型。
「编程与Agent」频道最新
- 零融资零广告，GPT Researcher 开源项目突破 3 万星 — EdenEmarco177 · 2026-10-11
- shadcn 自述:为组件打磨数周抽象,AI 尚未加速设计只能加速试错 — shadcn · 2026-10-11
- 7 周生产级 Agentic RAG 免费课程开源,GitHub 已收获 9.7k 星 — mdancho84 · 2026-10-11
- Arize AI 演示 agent 自学习闭环:遥测数据自动发现并修复生产故障 — AI Engineer · 2026-10-11
- 重度用户实测:让 AI 编码智能体 24/7 跑活,周额度两天耗尽 — gandamu_ml · 2026-10-11
- 上线前6天发现代码里模型名是AI幻觉编造的,130个测试全没拦住 — Trout_dev · 2026-10-11