Efficient PRM Training Data Synthesis via Formal Verification

TL;DR

FoVer introduces a formal verification-based framework to synthesize PRM training data efficiently, improving reasoning capabilities of LLMs across various benchmarks without human annotation.

Contribution

The paper presents FoVer, a novel method that uses formal verification tools to generate PRM training data from formal tasks, reducing cost and noise compared to prior approaches.

Findings

PRMs trained on FoVer data improve performance on math and logic reasoning tasks.

PRMs also show enhanced results on NLI and BBH benchmarks.

FoVer enables efficient, accurate data synthesis without additional LLM calls.

Abstract

Process Reward Models (PRMs) have emerged as a promising approach for improving LLM reasoning capabilities by providing process supervision over reasoning traces. However, existing approaches for constructing PRM training data remain costly and noisy, as they typically rely on human annotation or sampling-based labeling methods that require repeated LLM calls. In this work, we propose FoVer, a framework that synthesizes PRM training data from formal reasoning tasks by annotating step-level error labels using formal verification tools such as Z3 and Isabelle. By leveraging formal verification, FoVer enables efficient and accurate PRM data construction without requiring human annotation or additional LLM calls. Using FoVer, we create PRM training data from formal logic and theorem proving tasks. Experiments on 12 reasoning benchmarks show that fine-tuning on our training data improves PRMs not only on math and logic reasoning tasks, which are informal variants of the training tasks, but also on NLI and BBH benchmarks, which differ substantially from the tasks used to construct the training data. These results demonstrate the practical effectiveness of FoVer, showing that PRM training data created using formal verification improves PRMs on informal reasoning tasks written in natural language. The datasets, models, and code are provided at https://github.com/psunlpgroup/FoVer.