Meta 发布 AutoformBench:341 道题实测前沿模型 Lean 形式化能力与成本
ChrSzegedy · x · 2026-10-13
Meta AI 团队（Charles Arnal 等）发布 AutoformBench，一个针对前沿模型 Lean 4 形式化能力的基准，聚焦把高等数学大规模、低成本地形式化这一难点。
- 动机：SOTA 模型单次解题已很强，但大规模形式化仍难——AutoformBench 发布前，openai/math 中约只有 42% 的结果可被形式化；且「形式化一个大定理要花多少钱」此前没有公开数据，而这决定形式化能否进入同行评审流程。
- 构成：341 个证明任务，全部由人类专家从研究生及科研级数学文献中选取并形式化，每个任务要求写出实质性 Lean 4 证明。
- 成本曲线：附图给出各模型在「每任务最大花费（1/10/50/100/200 美元档）」下解题数（共 341 题）的对比，可直观看到不同预算下的性价比差距。
对关注形式化数学、定理证明与模型推理成本的人，这是少见的公开成本基准。
「研究」频道最新
- 机器学习复核历史底片:神秘瞬变源与核试验时间强相关 — coherence · 2026-10-13
- AI 解题引发数学家集体悲伤，经验主义正重塑数学价值体系 — manoelribeiro · 2026-10-13
- 开发者把 EmbeddingGemma 2 改造成语音转文字，M3 上 13 秒转录 1 小时音频 — solyarisoftware · 2026-10-13
- 用模拟测试 AI Agent：重放真实生产流量，50 个精选胜过千个随机 — HamelHusain · 2026-10-13
- Lanyon 用神经符号架构复现 Z-pinch 香肠不稳定性物理机制 — CatAstro_Piyush · 2026-10-13
- 斯坦福等提出无状态智能体 SLA,追平最强基线省 14.5 倍 token — RulinShao · 2026-10-13