利用形式化验证工具训练步骤级推理验证器

过程奖励模型 (PRMs) 用于提供关于大型语言模型 (LLMs) 生成的推理的分步反馈，正受到越来越多的关注。然而，仍然存在两个关键的研究空白：收集用于训练的准确的步级错误标签通常需要昂贵的人工标注，且现有 PRMs 仅限于数学推理问题。针对这些空白，本文旨在解决自动数据集创建以及将 PRMs 泛化到各种推理任务的挑战。为了实现这一目标，我们提出了 FoVer，这是一种训练 PRMs 的方法，它使用由形式化验证工具（如用于形式逻辑的 Z3 和用于定理证明的 Isabelle）自动标注的步级错误标签，这些工具为符号任务提供了自动且准确的验证。使用这种方法，我们合成了一个训练数据集，其中包含了针对形式逻辑和定理证明任务的 LLM 响应的错误标签，且无需人工标注。尽管这种数据合成仅对与形式化验证兼容的任务可行，但我们观察到，在我们的数据集上训练的基于 LLM 的 PRMs 表现出跨任务泛化能力，从而改进了在各种推理任务上的验证效果。具体而言，使用 FoVer 训练的 PRMs 显著优于基于原始 LLMs 的基线 PRMs，并且与在由人类或更强模型标注的标签上训练的最先进的 (SOTA) PRMs 相比，取得了具有竞争力或更优异的结果。这些结果是根据在 ProcessBench 上的步级验证以及在包括 MATH、AIME、ANLI、MMLU 和 BBH 在内的 12 个推理基准测试上的 Best-of-K 性能来衡量的。数据集、模型和代码可在 https://github.com/psunlpgroup/FoVer 获取。