Meta 与 NYU 论文提出 h1 循环，在 PutnamBench 上以更低成本略胜…
New Meta, NYU paper shows that a simple loop with good Lean tools and more compute matches or beats hand-built theorem-proving workflows.
Meta 与 NYU 的新论文提出 h1，一个给模型提供快速 Lean 反馈和搜索工具、并在每次校验失败后继续尝试的循环，不预设解题计划，只在每轮开始前生成进度摘要。在相同模型下，h1 在 PutnamBench 上以 598 题对 597 题略胜手工构建的 Goedel-Architect，每题成本为 1.08 美元对 1.47 美元。作者还指出接口仍有影响：使用 Opus 4.8 时，h1 解出 100 道高难度代数题中的 83 道，Claude Code 为 63 道。
推荐理由
AI 评分 60
原文给出同一模型下简单循环与手工工作流的直接对比，以及每道题成本差异，便于判断工作流设计的实际增益。
主题
正文 · AI 翻译
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 道。