Meta FAIR 的 h1：极简 agent 循环在形式化定理证明上达到 SOTA
meta-llama · hf · 2026-10-28
Meta FAIR 联合 EPFL、NYU 等机构发布 h1，回应「苦涩教训」之问：非结构化的简单 agent 循环能否匹敌人工设计的定理证明工作流？
- 方法：只给模型一个高效的 Lean 4 执行接口，靠验证器反馈和自我反思持续工作，不做任务分解、不加搜索结构。
- 结果：在 PutnamBench、FATE-X、FormalConjectures100-Solved 上达到 SOTA；解决 FormalConjectures 中 8 个公开问题；同模型条件下匹敌或超过 Goedel-Architect、AlphaProof Nexus 等专门工作流，且单次尝试（pass@1）常足以解决公开问题。
- 关键发现：消融和与 Claude Code、AxProverBase 的同模型对比表明，单纯「简单」并不够——高效的 Lean 接口本身在很大程度上决定成本和解题率。
- 建议：未来评测前沿模型时应先给高效的执行反馈接口，再考虑设计工作流，否则会重蹈「苦涩教训」。
「编程与Agent」频道最新
- Claude 拦下伪装成认证错误的朝鲜供应链攻击代码 — banteg · 2026-10-28
- Expo 官方开源 AI Agent 技能集,GitHub 星数突破 3300 — expo · 2026-10-28
- Lucas Meijer:写 skill 强迫你说清自己真正在意什么 — lucasmeijer · 2026-10-28
- 提示词注入被检测到≠被拦截：Agent 安全护栏验证四问 — shoumikgoswami · 2026-10-28
- 安全团队拷问：哪些 MCP Server 企业可用、如何治理？ — MorePerspectived · 2026-10-28
- mitsuhiko 谈 Pi 的 codemode 设计:classify 不配自定义 harness 就没意义 — mitsuhiko · 2026-10-28