Meta与NYU提出Lean定理证明循环h1
热点事件持续更新
Meta与NYU提出Lean定理证明循环h1
1 篇报道1 个报道来源19 小时前更新
先了解这件事
AI 综述
Meta 与 NYU 的论文提出名为 h1 的 Lean 定理证明循环：它不预设计划，只在每轮前生成进度摘要，为模型提供快速 Lean 反馈与搜索工具，并在每次校验失败后继续尝试。 在 PutnamBench 上，同一模型下 h1 以 598 比 597 略胜手工构建的 Goedel-Architect，每题成本 1.08 美元对 1.47 美元。论文称，简单循环配合良好的 Lean 工具和更多算力，即可匹敌或超过手工构建的定理证明流程。
AI 根据报道生成 · 18 小时前更新
最新进展11月2日 03:25
Meta 与 NYU 论文：简单循环加 Lean 工具媲美手工定理证明流程报道时间线
沿着报道，了解事件的不同侧面。
11月2日
- Rohan PaulMeta 与 NYU 论文：简单循环加 Lean 工具媲美手工定理证明流程
Meta 与 NYU 的论文提出 h1——一个给模型提供快速 Lean 反馈与搜索工具、并在每次校验失败后继续工作的循环，不预设计划，只在每轮前生成进度摘要。同一模型下 h1 在 PutnamBench 上以 598 比 597 略胜手工构建的 Goedel-Architect，每题成本 $1.08 对 $1.47。
本事件热度走势
- 可比范围当前
- 6
- 可比范围峰值
- 1011月2日 04:00
- 近 24 小时变化
- –
02.557.510
06:0009:0012:0015:0018:0021:00
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。