Meta FAIR 发布 h1:不用手工编排,纯 Lean 反馈循环拿下形式化定理证明 SOTA
burny_tech · x · 2026-10-13
Meta FAIR、EPFL、NYU 等机构论文《h1: A Taste of the Bitter Lesson in Automated Theorem Proving》,回应形式化数学领域的 Bitter Lesson 之问:与其手工设计证明工作流(分解、规划、多 agent 编排),不如给前沿模型一个高效的 Lean 4 接口,靠验证器反馈和自我反思让它持续工作。
- h1 是一个极简 harness:不给分解或搜索结构,只提供高效 Lean 交互界面 + 验证反馈循环。
- 在 PutnamBench、FATE-X、FormalConjectures100-Solved 上达到 SOTA;解决了 FormalConjectures 中 8 个开放猜想。
- 同模型对比下,匹配或超过 Goedel-Architect、AlphaProof Nexus 等手工工作流;单次长尝试(pass@1)常常胜过多次重试。
- 消融显示简单并不够:Lean 接口的效率很大程度上决定成本和解题率。
- 作者建议:在为前沿模型开工作流药方之前,先用高效执行反馈直接评测它们。
所属事件:Meta FAIR 发布 h1，纯 Lean 反馈循环刷新定理证明 SOTA(2 条相关)→
「编程与Agent」频道最新
- 跑数千万个无用程序实验：一种交给 LLM 的自动化玩法 — bushibuilds · 2026-10-13
- 开源个人智能体 Xiryn：Docker 沙盒桌面加 Telegram 遥控 — Scobleizer · 2026-10-13
- Witness：记录你的一切操作与视野，让智能体始终懂你上下文 — Scobleizer · 2026-10-13
- MecAgent 2.0 发布，作者宣称「CAD 即将被攻克」 — Scobleizer · 2026-10-13
- 开发者实测：约 25% AI 生成代码在 .NET 8+ 中引入回归 — lucasmeijer · 2026-10-13
- 投资人:编码代理时代,多数软件公司严重超员应立即裁员 — doodlestein · 2026-10-13