Training Step-Level Reasoning Verifiers with Formal Verification Tools
Process Reward Models (PRMs), which provide step-by-step feedback on the
reasoning generated by Large Language Models (LLMs), are receiving increasing
attention. However, two key research gaps remain: collecting accurate
step-level error labels for training typically requires costly human
annotation, and existing PRMs are limited to math reasoning problems. In
response to these gaps, this paper aims to address the challenges of automatic
dataset creation and the generalization of PRMs to diverse reasoning tasks. To
achieve this goal, we propose FoVer, an approach for training PRMs on
step-level error labels automatically annotated by formal verification tools,
such as Z3 for formal logic and Isabelle for theorem proof, which provide
automatic and accurate verification for symbolic tasks. Using this approach, we
synthesize a training dataset with error labels on LLM responses for formal
logic and theorem proof tasks without human annotation. Although this data
synthesis is feasible only for tasks compatible with formal verification, we
observe that LLM-based PRMs trained on our dataset exhibit cross-task
generalization, improving verification across diverse reasoning tasks.
Specifically, PRMs trained with FoVer significantly outperform baseline PRMs
based on the original LLMs and achieve competitive or superior results compared
to state-of-the-art PRMs trained on labels annotated by humans or stronger
models, as measured by step-level verification on ProcessBench and Best-of-K
performance across 12 reasoning benchmarks, including MATH, AIME, ANLI, MMLU,
and BBH. The datasets, models, and code are provided at
https://github.com/psunlpgroup/FoVer.
682fbf41098e5f16167723a0
Ryo Kamoi
claimed_verified
2025-05-26T08:16:58.777Z
60591896102f61b42f65ae37
https://cdn-avatars.huggingface.co/v1/production/uploads/60591896102f61b42f65ae37/PSHcLoEeNnwvzAPOd6-6i.jpeg
Ryo Kamoi
user
ryokamoi
682fbf41098e5f16167723a1
Yusen Zhang
682fbf41098e5f16167723a2
Nan Zhang
682fbf41098e5f16167723a3
Sarkar Snigdha Sarathi Das
682fbf41098e5f16167723a4
Rui Zhang
Training Step-Level Reasoning Verifiers with Formal Verification Tools
Process Reward Models (PRMs), which provide step-by-step feedback on the
reasoning generated by Large Language Models (LLMs), are receiving increasing
attention. However, two key research gaps remain: collecting accurate
step-level error labels for training typically requires costly human
annotation, and existing PRMs are limited to math reasoning problems. In
response to these gaps, this paper aims to address the challenges of automatic
dataset creation and the generalization of PRMs to diverse reasoning tasks. To
achieve this goal, we propose FoVer, an approach for training PRMs on
step-level error labels automatically annotated by formal verification tools,
such as Z3 for formal logic and Isabelle for theorem proof, which provide
automatic and accurate verification for symbolic tasks. Using this approach, we
synthesize a training dataset with error labels on LLM responses for formal
logic and theorem proof tasks without human annotation. Although this data
synthesis is feasible only for tasks compatible with formal verification, we
observe that LLM-based PRMs trained on our dataset exhibit cross-task
generalization, improving verification across diverse reasoning tasks.
Specifically, PRMs trained with FoVer significantly outperform baseline PRMs
based on the original LLMs and achieve competitive or superior results compared
to state-of-the-art PRMs trained on labels annotated by humans or stronger
models, as measured by step-level verification on ProcessBench and Best-of-K
performance across 12 reasoning benchmarks, including MATH, AIME, ANLI, MMLU,
and BBH. The datasets, models, and code are provided at
https://github.com/psunlpgroup/FoVer.
FoVer is a method for automatically annotating step-level error labels using formal verification tools to train Process Reward Models, which significantly improves cross-task generalization and outperforms human-annotated methods in various reasoning benchmarks.
Process Reward Models Large Language Models step-level error labels automatic dataset creation formal verification Z3 Isabelle symbolic tasks step-level verification ProcessBench Best-of-K reasoning benchmarks MATH AIME ANLI MMLU BBH