h1：自动化定理证明中的“苦涩教训”初探
研究人员推出了 h1，这是一个简单的框架：它给模型提供高效的 Lean 4 接口，让模型通过验证器反馈和自我反思持续工作，而不强加分解或搜索结构。它在 PutnamBench、FATE-X 和 FormalConjectures100-Solved 上达到了当前最优水平，并解决了 FormalConjectures 中的 8 个公开问题，在相同模型下达到或超过了专门的工作流。之所以重要，是因为它表明，用简单的智能体循环扩大测试时算力——再配上高效的执行接口——就可能媲美复杂的人工设计证明工作流。
报道来源
- Rohan Paul2026-11-01 19:25