学习 Lean 反馈以在 GPU 上高效评估候选证明

arXiv:2610.21881v1 公告类型：new 摘要：训练用于形式化定理证明的语言模型需要大量验证器调用。缓慢的检查和超时经常使 GPU 处于等待状态，也使原本可能正确的证明无法获得奖励。我们使用 4.84M 个带标签的程序，在 GPU 上训练神经评估器，以预测 Lean 4 的判定结果和编译器反馈。我们比较了两个有效性分类器，以及一个能够利用预测的目标状态和错误消息标注证明尝试的反馈模型。一个两阶段评估器首先使用分类器筛选候选证明，再使用反馈模型为其正向预测结果打分；在一个从公开证明器收集的、包含 68,932 个程序的基准集上进行评估时，该评估器预测 Lean 是否接受候选证明的准确率达到 87.8%。组合评估器在单张 H100 上每秒处理 3.5 个候选证明，吞吐量是采用环境复用的 64-worker Lean 基线的 4.2 倍。最后，我们将该评估器与 Lean 判定结果结合，得到一种混合奖励系统，使 GRPO 训练步骤耗时缩短约 31%。使用混合奖励完成一个 GRPO epoch 后，证明器的 miniF2F pass@1 几乎与仅使用 Lean 奖励时相同（62.2% 对 62.4%），而 pass@32 则达到 72.4%，高于 71.3%。