形式化数学验证中生成式奖励建模的期望值对齐

大语言模型（LLM）正越来越多地与Lean 4等形式化交互式定理证明器配合使用。用强化学习或搜索方法扩展这些系统，需要能够评估中间推理步骤的过程奖励模型（PRM）。现有的奖励模型设计存在一种现实中的权衡。价值头模型提供连续分数，但会改变生成式模型的接口；而生成式奖励模型保留了文本化的推理依据，却因数值被拆分到多个词元而难以适配连续浮点回归。我们提出期望值对齐（Expected Value Alignment，EVA），这一奖励建模流程在保持表面输出离散的同时，从模型的词元分布中提取连续分数。模型以结构化JSON格式输出整数分数，EVA对相应锚点词元的logits取期望，计算得到连续分数。训练将因果语言建模目标与基于这些期望值的辅助均方误差损失相结合。我们将EVA实例化为Leibniz——一个面向Lean 4形式化验证的奖励模型，并将其与零样本及奖励建模基线进行对比评估。评估表明，基于logits的连续打分显著减少了离散化伪影，同时保留了生成式评判的可解释性。