arXiv · cs.AI · Yutong Wang, Xuanzhi Ren, Tianyi Xu, Ruitong Liu, Jingda Xu, Peihao Wu, Bryan Dai, Bin Dong · 10 小时前模型评分50
Reap：用轻量模型揭示蒙特卡洛证明搜索
Reap: Uncovering Monte Carlo proof search with a lightweight model
导读
作者提出 Reap，一个在 Lean4 中学习和分析形式化证明搜索的开放框架，并训练出 1.7B 参数的策略价值模型 Reaper-1。Reaper-1 配合独立的前提选择器，在 miniF2F-test 上以 pass@32 解决 79.9% 的题目，在同规模开源证明器中达到领先水平，并与更大模型保持竞争力。
分类置信度
中 · 待人工复核
- 只有单一媒体来源，需要人工复核。
来源级别：媒体与个人
应用领域：科学研究
事件类型：研究发布
证据摘录
- “We present Reap, an open framework for learning and analyzing formal proof search in Lean4.”
来源：arXiv · cs.AI · arxiv.org