Efficient PRM Training Data Synthesis via Formal Verification (2026.findings-acl)
Copied to clipboard
Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Ranran Haoran Zhang, Wenpeng Yin, Rui Zhang
| Challenge: | Existing approaches for constructing PRM training data rely on human annotation or sampling-based labeling methods that require repeated LLM calls. |
| Approach: | They propose a framework that synthesizes PRM training data by annotating step-level error labels using formal verification tools such as Z3 and Isabelle. |
| Outcome: | The proposed framework synthesizes PRM training data from formal logic and theorem proving tasks without human annotation or additional LLM calls. |
Similar Papers
An Efficient and Precise Training Data Construction Framework for Process-supervised Reward Model in Mathematical Reasoning (2025.acl-long)
Copied to clipboard
| Challenge: | Existing methods for constructing process supervision training data are costly or suffer from poor quality. |
| Approach: | They propose a framework called EpicPRM which annotates each intermediate reasoning step based on its quantified contribution and uses an adaptive binary search algorithm to enhance annotation precision and efficiency. |
| Outcome: | The proposed framework improves annotation precision and efficiency and can be used to train a high-quality training dataset with 50k annotated intermediate steps. |
Process-Supervised Reward Models for Verifying Clinical Note Generation: A Scalable Approach Guided by Domain Expertise (2025.emnlp-main)
Copied to clipboard
Hanyin Wang, Chufan Gao, Qiping Xu, Bolun Liu, Guleid Hussein, Hariprasad Reddy Korsapati, Mohamad El Labban, Kingsley Iheasirim, Mohamed Hassan, Gokhan Anil, Brian Bartlett, Jimeng Sun
| Challenge: | Currently, no automated, scalable method exists to evaluate the quality of LLM-generated clinical notes, leaving manual evaluation the gold standard. |
| Approach: | They propose a framework for training PRMs to deliver step-level reward signals for LLM-generated clinical notes. |
| Outcome: | The proposed framework outperforms reasoning and non-reasoning models on key evaluations and selects physician-preferred clinical notes with 56.2% accuracy. |
Process Reward Models Meet Planning: Generating Precise and Scalable Datasets for Step-Level Rewards (2026.acl-long)
Copied to clipboard
| Challenge: | Existing PRM datasets are expensive to construct and limited to the mathematical domain. |
| Approach: | They propose a method to generate a corpus of one million reasoning steps using the Planning Domain Definition Language. |
| Outcome: | The proposed model generates a corpus of approximately one million reasoning steps across various PDDL domains and trains them. |
Error Typing for Smarter Rewards: Improving Process Reward Models with Error-Aware Hierarchical Supervision (2025.findings-emnlp)
Copied to clipboard
| Challenge: | Large Language Models (LLMs) are prone to hallucination, especially during multihop tasks. |
| Approach: | They propose a hierarchical, erroraware discriminative PRM that classifies math errors at each step and combines finegrained signals to estimate step correctness. |
| Outcome: | The proposed model outperforms the prior best in a new stateof-theart PRMScore of 67.7 on a 400Ksample dataset . |
The Lessons of Developing Process Reward Models in Mathematical Reasoning (2025.findings-acl)
Copied to clipboard
Zhenru Zhang, Chujie Zheng, Yangzhen Wu, Beichen Zhang, Runji Lin, Bowen Yu, Dayiheng Liu, Jingren Zhou, Junyang Lin
| Challenge: | a recent study shows that process reward models can make mistakes, leading to wrong conclusions. |
| Approach: | They propose a consensus filtering mechanism that integrates MC estimation with LLM-as-a-judge to improve model performance and data efficiency. |
| Outcome: | The proposed model outperforms existing open-source alternatives and provides practical guidelines for future research. |
Beyond the First Error: Process Reward Models for Reflective Mathematical Reasoning (2025.findings-emnlp)
Copied to clipboard
| Challenge: | Existing methods for training effective PRMs focus on the first incorrect step and all preceding steps, assuming that all subsequent steps are incorrect. |
| Approach: | They propose a data annotation method specifically designed to score the long CoT reasoning process by using an LLM-based judger for annotation. |
| Outcome: | The proposed method improves PRMs' ability to identify effective self-correction behaviors and reasoning based on erroneous steps. |
Enhancing Logical Reasoning in Language Models via Symbolically-Guided Monte Carlo Process Supervision (2025.emnlp-main)
Copied to clipboard
| Challenge: | Large language models have shown strong performance in many reasoning benchmarks, but lack robust planning or symbolic abstractions. |
| Approach: | They propose to synthesize high-quality symbolic reasoning trajectories with stepwise pseudo-labels at scale via Monte Carlo estimation. |
| Outcome: | The proposed method can be trained on high-quality symbolic reasoning trajectories with stepwise pseudo-labels at scale using Monte Carlo estimation. |
R-PRM: Reasoning-Driven Process Reward Modeling (2025.emnlp-main)
Copied to clipboard
| Challenge: | Existing Process Reward Models (PRMs) output evaluation scores directly, limiting both learning efficiency and evaluation accuracy. |
| Approach: | They propose a Reasoning-Driven Process Reward Modeling (R-PRM) which activates inherent reasoning to enhance process-level evaluation. |
| Outcome: | The proposed model outperforms baseline models on ProcessBench and PRMBench by 13.9 and 8.5 F1 scores. |
From Informal to Formal – Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs (2025.acl-long)
Copied to clipboard
Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian
| Challenge: | Recent studies in formal mathematical reasoning have shown an unstoppable growth trend. |
| Approach: | They constructed 18k high-quality instruction-response pairs across five mainstream formal specification languages and evaluated them against ten open-sourced LLMs. |
| Outcome: | The proposed model compared instruction-response pairs across five formal specification languages and found that the LLMs were good at writing proof segments when given either the code, or the detailed description of proof steps. |
Efficient Process Reward Modeling via Contrastive Mutual Information (2026.acl-long)
Copied to clipboard
| Challenge: | Existing methods to verify intermediate reasoning steps require human annotators to assign reward scores to each reasoning step, which is labor-intensive and costly. |
| Approach: | They propose a method that leverages the model's internal probability to infer step-level supervision while significantly reducing the computational burden of annotating dataset. |
| Outcome: | The proposed method reduces dataset construction time by 84% and token generation by 98% compared to MC estimation, while achieving higher accuracy on process-level evaluations and mathematical reasoning benchmarks. |