reuF2F 基准发布:244 道 Lean 形式化开放数学题,最强模型仅解出约四成
AkariAsai · x · 2026-10-20
CMU、港中深、清华等机构联合推出 reuF2F,一个面向编码智能体的 Lean 4 形式化数学基准。
- 题目来源:244 道来自本科生科研项目(REU)的开放数学问题,由专家用 Lean 形式化,覆盖广泛数学子领域;这类低关注度开放问题比知名猜想更适合做「盲测」评估
- 任务设置:智能体拿到开放问题的 Lean 陈述,产出形式化证明并由 Lean 内核检验;每个问题连同其否定命题放入 Docker 容器中的 Lean 项目,采用标准 coding-agent 评测协议
- 统一评测框架:团队还构建了 Leanimum-agent(基于 mini-SWE-agent 的极简 Lean 编码智能体),保证各模型在同一 harness 下对比
- 结果:表现最好的模型也只解决了约 40%(109/244)的问题,说明端到端形式化开放问题仍有巨大提升空间
论文指出,随着 LLM 开始大规模证明猜想,可靠验证成为瓶颈,形式化数学提供了可机器校验的信任框架。
所属事件:reuF2F 基准发布:244 道 Lean 形式化开放数学题,最强模型仅解约四成(5 条相关)→
「编程与Agent」频道最新
- REA 一周狂涨 21.4 万星，AI 逆向工程工具登顶 GitHub 周榜 — sven_ai · 2026-10-20
- 开发者转粉：图将成每家公司世界模型的核心数据结构 — _AustinCalvert_ · 2026-10-20
- RuneBench：让 AI Agent 在游戏 RuneScape 里刷经验测能力 — charliermarsh · 2026-10-20
- Claude 官方 Cookbook:让 Claude 自动审计 Agent 会话安全风险 — brada · 2026-10-20
- 用 Codex 驱动 CapCut Web,对话式 AI 工作流做营销视频 — Div_pradeep · 2026-10-20
- 给 Claude 一个 URL，逆向出 Revolut 完整品牌设计系统 — CurieuxExplorer · 2026-10-20