用 484 万 Lean 标注程序训练 GPU verifier proxy：混合 Lean reward 将 GRPO 训练时间降低约 31%

Milikic、Bamas、Abbe 与 Kunčak 训练可在 GPU 上批量预测 Lean acceptance 的 neural evaluators，以缓解 RL / search 中频繁调用 Lean verifier 的吞吐瓶颈。训练集包含约 484 万个 Lean-labelled programs；两阶段 evaluator 在 68,932 个公开 prover 生成程序上达到 87.8% acceptance-prediction accuracy，并在单张 H100 上达到约 3.5 candidates/s，论文称相对具有 environment reuse 的 64-worker Lean baseline 吞吐提高 4.2 倍。将 learned feedback 与真实 Lean reward 混合用于 GRPO 后，训练 wall-clock 约降低 31%；一轮训练后的 miniF2F pass@1 与 Lean-only reward 基本持平，pass@32 略高。作者仍把 Lean verifier 保留在 hybrid loop 中，learned evaluator 是加速代理而非 trusted kernel 替代品。