# Efficient PRM Training Data Synthesis via Formal Verification

arXiv: https://arxiv.org/abs/2505.15960 · HTML: https://mlsanity.com/paper/2505.15960/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Placed in Reinforcement learning for reasoning, one of 17 directions in LLM reasoning.
- Builds on 43 of its 64 references that are in the map.
- First posted on arXiv 21 May 2025.

## Placed in

- LLM reasoning / [Reinforcement learning for reasoning](https://mlsanity.com/lr/reinforcement-learning-for-reasoning/)
- LLM alignment / RLHF / preference optimisation / [Process reward models for reasoning](https://mlsanity.com/alignment/process-reward-models-for-reasoning/)
- Synthetic data and self-improvement for LLMs / [Synthetic reasoning data and bootstrapping](https://mlsanity.com/synth/synthetic-reasoning-data-and-bootstrapping/)

## Builds on (most cited first, 30 of 43)

- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Direct Preference Optimization: Your Language Model is Secretly a Reward Model](https://mlsanity.com/paper/2305.18290/) (2023)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Challenging BIG-Bench Tasks and Whether Chain-of-Thought Can Solve Them](https://mlsanity.com/paper/2210.09261/) (2022)
- [LlamaFactory: Unified Efficient Fine-Tuning of 100+ Language Models](https://mlsanity.com/paper/2403.13372/) (2024)
- [Solving Quantitative Reasoning Problems with Language Models](https://mlsanity.com/paper/2206.14858/) (2022)
- [Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotations](https://mlsanity.com/paper/2312.08935/) (2023)
- [Solving math word problems with process- and outcome-based feedback](https://mlsanity.com/paper/2211.14275/) (2022)
- [Right for the Wrong Reasons: Diagnosing Syntactic Heuristics in Natural Language Inference](https://mlsanity.com/paper/1902.01007/) (2019)
- [Adversarial NLI: A New Benchmark for Natural Language Understanding](https://mlsanity.com/paper/1910.14599/) (2019)
- [Program Induction by Rationale Generation : Learning to Solve and Explain Algebraic Word Problems](https://mlsanity.com/paper/1705.04146/) (2017)
- [Generative Verifiers: Reward Modeling as Next-Token Prediction](https://mlsanity.com/paper/2408.15240/) (2024)
- [Improve Mathematical Reasoning in Language Models by Automated Process Supervision](https://mlsanity.com/paper/2406.06592/) (2024)
- [The Lessons of Developing Process Reward Models in Mathematical Reasoning](https://mlsanity.com/paper/2501.07301/) (2025)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Self-critiquing models for assisting human evaluators](https://mlsanity.com/paper/2206.05802/) (2022)
- [ReST-MCTS*: LLM Self-Training via Process Reward Guided Tree Search](https://mlsanity.com/paper/2406.03816/) (2024)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [ProcessBench: Identifying Process Errors in Mathematical Reasoning](https://mlsanity.com/paper/2412.06559/) (2024)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Making Large Language Models Better Reasoners with Step-Aware Verifier](https://mlsanity.com/paper/2206.02336/) (2022)
- [REFINER: Reasoning Feedback on Intermediate Representations](https://mlsanity.com/paper/2304.01904/) (2023)
- [Recall and Learn: Fine-tuning Deep Pretrained Language Models with Less Forgetting](https://mlsanity.com/paper/2004.12651/) (2020)

## Built on by (most cited first, 8 of 8)

- [A Survey of Process Reward Models: From Outcome Signals to Process Supervisions for Large Language Models](https://mlsanity.com/paper/2510.08049/) (2025)
- [Trust but Verify! A Survey on Verification Design for Test-time Scaling](https://mlsanity.com/paper/2508.16665/) (2025)
- [Beyond Statistical Learning: Exact Learning Is Essential for General Intelligence](https://mlsanity.com/paper/2506.23908/) (2025)
- [VeriBound: PAC-Bayesian Generalization Bounds for Process Reward Models Trained with Formal Verification Tools](https://mlsanity.com/paper/2606.20740/) (2026)
- [Program Learning with Verifiable Rewards: Symbolic Backpropagation for Post-Training LLMs](https://mlsanity.com/paper/2608.28421/) (2026)
- [Counterexample Generation via Per-Theorem Symbolic Verifiers: When Imitation Hurts and Reinforcement Repairs](https://mlsanity.com/paper/2610.02444/) (2026)
- [LeanPRM: Lean-Grounded Process Supervision for Natural Language Proof Verification](https://mlsanity.com/paper/2610.17697/) (2026)
- [Compiling Expert Procedures into Verified Programs: When a Small Model Is Enough](https://mlsanity.com/paper/2610.19148/) (2026)

## Abstract (arXiv)

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.