Reap: 利用轻量级模型揭示蒙特卡洛证明搜索机制

Reap 提出基于 Lean4 的开放证明搜索框架，训练的 1.7B 参数模型 Reaper-1 在 miniF2F-test 基准上以 pass@32 达到 79.9% 解题率，确立了同级别开源求解器的前沿性能。 系统通过共享状态转换与重放验证，结合策略价值引导的蒙特卡洛树搜索，利用强化学习增强证明组织能力，使更少显式搜索决策能驱动更复杂的策略程序执行。