Meta 与 NYU 论文：简单循环 h1 在 Lean 定理证明上超越手工工作流
Meta 与 NYU 的论文提出 h1——一个只给模型快速 Lean 反馈和搜索工具、每次检查失败后继续工作的简单循环，不预设计划，仅在每轮前生成进度摘要。同一模型下，h1 在 PutnamBench 上以 598 比 597 击败手工构建的 Goedel-Architect，每题成本 $1.08 对 $1.47。
Rohan Paul· @rohanpaul_ai · X·2026-11-02 03:25· 36 分钟前AI 评分50
AI 导读
Meta 与 NYU 的论文提出 h1——一个只给模型快速 Lean 反馈和搜索工具、每次检查失败后继续工作的简单循环，不预设计划，仅在每轮前生成进度摘要。同一模型下，h1 在 PutnamBench 上以 598 比 597 击败手工构建的 Goedel-Architect，每题成本 $1.08 对 $1.47。
正文 · 原文
Meta 与 NYU 的新论文表明，一个配备良好 Lean 工具和更多算力的简单循环，就能匹敌甚至超越手工构建的定理证明工作流。
用 Lean（一种计算机可检查的语言）编写数学证明的系统，越来越多地采用手工设计的、用于规划和拆分问题的工作流。它们的提升往往来自更强的模型或更多算力，从而掩盖了工作流本身的贡献。
他们构建了 h1，这是一个循环，为模型提供快速的 Lean 反馈和搜索工具，并在每次检查失败后让它继续工作。它不施加任何计划，只在每轮开始前生成一份进度摘要。
在相同模型下，h1 在 PutnamBench 上以 598 题对 597 题击败了手工构建的 Goedel-Architect，每题成本为 $1.08 对 $1.47。接口仍然重要：使用 Opus 4.8 时，h1 解出了 100 道高难度代数题中的 83 道，而 Claude Code 为 63 道。
来源：Rohan Paul · x.com
来源：RadarAI · aihot.news