Hugging Face Daily Papers· Skander Moalla, Ahmad Rammal, Niket Patel, Remi Munos, Julia Kempe·· 4 天前精选AI 评分60
h1：用简单智能体循环在自动定理证明中验证苦涩教训
h1: A Taste of the Bitter Lesson in Automated Theorem Proving
AI 导读
论文提出 h1，一个仅提供高效 Lean 4 接口、靠验证器反馈与自我反思驱动的简单智能体框架，在 PutnamBench、FATE-X 和 FormalConjectures100-Solved 上达到 SOTA，解决 FormalConjectures 中八个开放问题。
推荐理由
论文用同模型对比表明简单智能体循环可匹敌复杂证明工作流，并指出高效 Lean 接口才是成本与解题率的关键。