精选理由
这篇论文用Lean在定理证明训练中引入细粒度过程奖励，比只判对错的强化学习效果好，在MiniF2F和ProofNet上都有提升。
研究者提出利用Lean证明助手作为符号过程预言机，在训练中提供细粒度的策略级验证反馈，弥补了传统RLVR仅依赖二元验证信号的不足。通过将证明尝试解析为策略序列，Lean能标记局部正确步骤及最早失败步骤，从而产生基于类型论的密集可验证信用信号。在STP-Lean和DeepSeek-Prover-V1.5上的实验表明，策略级监督在多数设置下优于仅结果监督的基线，在MiniF2F和ProofNet基准上取得提升。该工作展示了符号证明助手不仅可在评估时用作验证器，还能在训练中充当过程级奖励预言机。
AI 翻译 · 中文
研究者提出利用Lean证明助手作为符号过程预言机，在训练中提供细粒度的策略级验证反馈，弥补了传统RLVR仅依赖二元验证信号的不足。通过将证明尝试解析为策略序列，Lean能标记局部正确步骤及最早失败步骤，从而产生基于类型论的密集可验证信用信号。在STP-Lean和DeepSeek-Prover-V1.5上的实验表明，策略级监督在多数设置下优于仅结果监督的基线，在MiniF2F和ProofNet基准上取得提升。该工作展示了符号证明助手不仅可在评估时用作验证器，还能在训练中充当过程级奖励预言机。
While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This ga…