通过形式化验证高效合成 PRM 训练数据
计算与语言
2026-04-10 v3
摘要
过程奖赏模型 (PRM) 作为一种通过对推理轨迹提供过程监督来提升大语言模型推理能力的有前景的方法，正在逐渐发展。然而，现有构建 PRM 训练数据的做法仍然昂贵且噪声较大，由于它们通常依赖人工标注或基于抽样的标注方法，需要重复调用大语言模型。本文提出了 FoVer 框架，通过使用形式化验证工具（如 Z3 和 Isabelle）对推理步骤级别的错误标签进行注释，从而从形式推理任务中合成 PRM 训练数据。凭借形式化验证，FoVer 无需人工标注或额外调用大语言模型即可高效准确地构建 PRM 数据。我们使用 FoVer 从形式逻辑和定理证明任务中创建 PRM 训练数据。在 12 个推理基准测试上进行实验，显示在我们的训练数据上进行微调，不仅能在数学和逻辑推理任务上提升 PRM 的表现（这些任务是训练任务的非正式变体），也能在自然语言推理 (NLI) 和 BBH 基准测试上提升表现（这些任务与用于构建训练数据的任务差异很大）。这些结果表明 FoVer 在实际中的有效性，表明使用形式化验证创建的 PRM 训练数据能够提升在自然语言中编写的非正式推理任务上的 PRM。数据集、模型和代码均提供于 https://github.com/psunlpgroup/FoVer。
引用
@article{arxiv.2505.15960,
title = {Efficient PRM Training Data Synthesis via Formal Verification},
author = {Ryo Kamoi and Yusen Zhang and Nan Zhang and Sarkar Snigdha Sarathi Das and Ranran Haoran Zhang and Wenpeng Yin and Rui Zhang},
journal= {arXiv preprint arXiv:2505.15960},
year = {2026}
}
备注
ACL 2026 Findings. Datasets, models, and code are provided at https://github.com/psunlpgroup/FoVer. Please also refer to our project website at https://fover-prm.github.io/