★ 3
h1 框架：简单智能体循环在 Lean 4 定理证明达 SOTA
论文提出 h1，一个仅给模型提供高效 Lean 4 接口、依靠验证器反馈与自我反思持续迭代的简单框架，不预设分解或搜索结构。h1 在 PutnamBench、FATE-X、FormalConjectures100-Solved 上取得 SOTA，并解决 FormalConjectures 中 8 …
arXiv cs.LG5 天前
共 1 篇相关资讯，按重要度与时间排序，每 3 小时更新。
论文提出 h1，一个仅给模型提供高效 Lean 4 接口、依靠验证器反馈与自我反思持续迭代的简单框架，不预设分解或搜索结构。h1 在 PutnamBench、FATE-X、FormalConjectures100-Solved 上取得 SOTA，并解决 FormalConjectures 中 8 …