自动定理证明迎来“苦涩教训”：简单智能体也能击败复杂流程？

导语

在非形式化数学中，大语言模型往往通过更长的思维链、更大的测试时计算量和更强的智能体循环取得进展。但自动定理证明面对的是另一种更严格的环境：模型写出的每一步都必须通过 Lean 4 的形式化验证。近年来，研究者通常为模型设计规划、问题分解、搜索和专用证明器编排等流程。新论文 《h1: A Taste of the Bitter Lesson in Automated Theorem Proving》 追问的是：如果不预设这些复杂结构，只让一个模型持续尝试、接收反馈并反思，能否获得相当的效果？

h1 做了什么

h1 是一个围绕 Lean 4 构建的简洁 harness。它没有强制模型先拆分定理，也没有规定固定的搜索树或多智能体协作方式，而是提供更高效的 Lean 交互接口，让模型在证明失败时读取验证器反馈，修改方案，再继续工作。换言之，系统的重点不是替模型设计完整的解题路线，而是降低模型与形式化验证环境之间的交互成本。

论文报告的核心结果包括：

• h1 在 PutnamBench、FATE-X 和 FormalConjectures100-Solved 上取得当前最先进水平的结果；
• 在 FormalConjectures 中解决了八个此前开放的问题；
• 在使用相同模型进行比较时，h1 能够匹配或超过 Goedel-Architect、AlphaProof Nexus 等专门化流程；
• 一次尝试（pass@1）在不少情况下就能完成开放问题，而不一定依赖大量候选结果筛选。

“苦涩教训”体现在哪里

这里的“苦涩教训”并不是说工程设计毫无价值，而是提醒研究者重新审视一个常被忽略的变量：规模化的通用计算，可能比精心设计的任务流程更具普适性。若更强的模型、更多的调用次数和更复杂的编排同时出现，单凭最终分数很难判断真正的收益来自哪里。h1 通过匹配模型的比较，试图把流程本身的影响单独拿出来观察。

不过，论文的消融实验也给出了重要限制：简单并不等于自动有效。h1 的成本和求解率很大程度上取决于 Lean 接口是否高效，以及模型能否及时获得清晰、可操作的执行反馈。一个简短循环若每次交互都昂贵或反馈不易利用，规模化测试时计算资源仍会迅速消耗。

对形式化数学的影响

这项工作对自动证明系统的启示是，评估新工作流时，不能只比较最终分数，也要控制模型能力和测试时计算量，并优先检查基础工具链的效率。对于需要跟上前沿模型数学产出的形式验证来说，一个低摩擦的验证接口或许比继续叠加规划模块更值得优先投入。

更广泛地看，h1 并未证明所有定理都适合简单循环，也没有否定分解、搜索和专用证明器的作用。它提出的是一个更务实的基线：在引入复杂架构之前，先确认模型是否已经能够借助高效执行反馈解决问题。若这个基线足够强，未来的创新就需要证明额外结构带来的收益，确实超过了它增加的成本与复杂度。

来源：Hugging Face Daily Papers