reuF2F 基准发布:244 道 Lean 形式化开放数学题,最佳模型仅解出 109

wellecks · x · 2026-10-23

新基准 reuF2F 从美国 REU(本科生科研项目)中收集 244 道开放数学问题,覆盖广泛数学领域,全部由专家在 Lean 中形式化,用于端到端测试 AI 智能体证明开放问题的能力。团队还构建了 Leanimum-agent——一个最小化的 Lean 编码智能体,保证所有模型在同一 harness 下公平对比。结果显示,即使表现最好的模型也只能解决 244 题中的 109 道,说明验证(形式化)正成为 LLM 大规模证明猜想时代的瓶颈。