面向形式化数学验证的生成式奖励模型期望值对齐

大型语言模型正日益与 Lean 4 等形式化交互式定理证明器结合使用。利用强化学习或搜索方法扩展这些系统，需要能够评估中间推理步骤的过程奖励模型（PRM）。现有设计存在权衡：值头模型提供连续分数但改变生成接口，而生成式奖励模型保留文本理由却难以匹配连续回归。本文提出期望值对齐（EVA），一种在保持离散输出的同时从令牌分布中提取连续分数的奖励建模方法。该模型以结构化 JSON 格式输出整数分数，EVA 则计算对应锚点令牌 logits 的期望值得出连续分数。我们在 Lean 4 形式化验证奖励模型 Leibniz 中实例化了 EVA，实验表明该方法显著减少了离散化伪影，同时保留了生成式批评的可解释性。