arXiv 机器学习· Skander Moalla, Ahmad Rammal, Niket Patel, Remi Munos, Julia Kempe·· 6 小时前AI 评分55
h1：通过测试时计算扩展探索自动定理证明的“苦涩教训”
h1: A Taste of the Bitter Lesson in Automated Theorem Proving
AI 导读
研究人员推出轻量化自动定理证明测试框架 h1，仅依靠模型与 Lean 4 的高效交互接口、验证器反馈和自我反思循环，无需强加任务分解或搜索结构。该框架在 PutnamBench、FATE-X 和 FormalConjectures100-Solved 上取得 SOTA 表现，解决了 FormalConjectures 中的 8 个开放性问题。
来源：arXiv 机器学习 · arxiv.org