Hugging Face 开源 369 个数学 RL 环境,Lean 判分器自动验证证明
aigclink · x · 2026-10-12
Hugging Face 把 OpenAI 前几天发布的数学成果转成了开源强化学习环境,可直接挂进训练流程让模型刷题进化。
- 规模:369 个任务、405 道形式化数学题、214 个题型,每个任务给一份带 sorry 的 Lean 题面
- 玩法:AI 要把题面补成完整证明,独立沙箱里的 Lean 判分器自动编译验证,对 1 错 0,reward 直接用于训练
- 策略:先挑会做的刷,刷不动的攒着慢慢练
目前还是早期版本,verifier 只认原始形式化写法,等价证明也可能被误判,适合当练兵场使用。
所属事件:Hugging Face 将 OpenAI 数学成果转为开源 RL 环境(3 条相关)→
「研究」频道最新
- 陶哲轩:AI 让证明变廉价,数学家的新工作是想象力 — burny_tech · 2026-10-12
- EMNLP 论文:按主机采样式爬取可多收数倍高质量预训练页面 — metehan777 · 2026-10-12
- Ethan Mollick：赛博格研究者正迅速主导数学研究 — TinfoilTricorn · 2026-10-12
- AI 证算是暴力破解还是真智能,X 上的争论 fusillade — teortaxesTex · 2026-10-12
- OpenAI 论文宣称证明 π 无理性指数恰为 2,355/113 已近极限 — TinfoilTricorn · 2026-10-12
- Nature：字节化改造让 LLM 终于能数对单词里的字母 — PontiEdoardo · 2026-10-12