Meta NYU 研究：简单循环配合 Lean 工具超越复杂定理证明工作流
原标题：New Meta, NYU paper shows that a simple loop with good Lean tools and more compute matches or beats ...
78AI 研判分
Meta 与 NYU 联合论文提出 h1 系统，通过结合 Lean 形式化验证反馈与搜索工具的简单循环，在同等模型下以更低成本击败手工设计的 Goedel-Architect 工作流。研究表明，在定理证明任务中，有效的工具接口与计算扩展比复杂的规划逻辑更具性价比。
报道正文
Rohan Paul (@rohanpaul_ai) · 2026-11-01 19
Meta 与纽约大学（NYU）的新论文表明，一个配备优质 Lean 工具并增加算力的简单循环，其表现可以匹敌甚至超越手工构建的定理证明工作流。
在 Lean（一种计算机可验证的数学语言）中编写数学证明的系统，越来越多地采用经过精心设计的工作流来规划和分解问题。这些系统的性能提升往往源于更强的模型或更多的算力，从而掩盖了工作流本身带来的增益。
他们构建了 h1，这是一个为模型提供快速 Lean 反馈和搜索工具的循环机制，并在每次检查失败后继续运行。它不强制进行规划，仅在每一轮开始前提供进度摘要。
在使用相同模型的情况下，h1 在 PutnamBench（包含 598 道题）上的表现超过了手工构建的 Goedel-Architect（597 题），且每道题的成本仅为 $1.08，低于后者的 $1.47。接口设计依然至关重要：使用 Opus 4.8 时，h1 解决了 100 道高难度代数题中的 83 道，而 Claude Code 仅解决了 63 道。
