热点事件持续更新
Meta 发布 AutoformBench 形式化基准
1 篇报道1 个报道来源2 小时前更新
先了解这件事
AI 综述
2026 年 10 月 13 日，Meta AI 团队发布 AutoformBench，用 341 道研究生及科研级数学证明任务，评测前沿模型的 Lean 4 形式化能力与成本。该基准给出各模型在每任务最大花费 1/10/50/100/200 美元档下的解题数对比，报道称这是此前缺少的公开成本数据。此外，发布前 openai/math 中约只有 42% 的结果可被形式化。目前该基准已随发布公开，尚无其他机构针对其结果的后续反馈或复现报道。
AI 根据报道生成 · 1 小时前更新
最新进展10月13日 01:16
Meta 发布 AutoformBench，341 道题评测 Lean 4 形式化能力并首次公开多档成本数据。报道时间线
沿着报道，了解事件的不同侧面。
10月13日
- AGI HuntMeta 发布 AutoformBench：341 道题实测前沿模型 Lean 形式化能力与成本
Meta AI 团队发布 AutoformBench，用 341 道研究生及科研级数学证明任务评测前沿模型的 Lean 4 形式化能力与成本。基准给出各模型在每任务最大花费 1/10/50/100/200 美元档下的解题数对比，这也是此前缺少的公开成本数据。发布前 openai/math 中约只有 42% 的结果可被形式化。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。