Training Step-Level Reasoning Verifiers with Formal Verification Tools

• URL: http://arxiv.org/abs/2505.15960v1
• Date: Wed, 21 May 2025 19:23:45 GMT
• Title: Training Step-Level Reasoning Verifiers with Formal Verification Tools
• Authors: Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Rui Zhang,
• Abstract summary: We propose FoVer, an approach for training PRMs on step-level error labels automatically annotated by formal verification tools.<n>FoVer is feasible only for tasks compatible with formal verification.<n>We observe that LLM-based PRMs trained on our dataset exhibit cross-task generalization, improving verification across diverse reasoning tasks.
• Score: 10.625896243556578
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Discriminative Policy Optimization for Token-Level Reward Models [55.98642069903191]
  Process reward models (PRMs) provide more nuanced supervision compared to outcome reward models (ORMs)<n>Q-RM explicitly learns token-level Q-functions from preference data without relying on fine-grained annotations.<n>Reinforcement learning with Q-RM significantly enhances training efficiency, achieving convergence 12 times faster than ORM on GSM8K and 11 times faster than step-level PRM on MATH.
  arXiv  Detail & Related papers  (2025-05-29T11:40:34Z)
• Beyond the First Error: Process Reward Models for Reflective Mathematical Reasoning [49.21525229904197]
  We propose a novel data annotation method for PRMs specifically designed to score the long CoT reasoning process.<n>We introduce the concepts of Error Propagation and Error Cessation, enhancing PRMs' ability to identify both effective self-correction behaviors and reasoning based on erroneous steps.<n>Our PRM achieves superior performance across various metrics, including search guidance, BoN, and F1 scores.
  arXiv  Detail & Related papers  (2025-05-20T14:12:05Z)
• Accurate and Diverse LLM Mathematical Reasoning via Automated PRM-Guided GFlowNets [6.001837672951086]
  We introduce a novel Process Reward Model (PRM) trained automatically using Monte Carlo Tree Search.<n>We then adapt Generative Flow Networks (GFlowNets) to operate at the reasoning step level.<n> Empirical evaluation shows strong improvements in both accuracy and solution diversity on challenging mathematical benchmarks.
  arXiv  Detail & Related papers  (2025-04-28T16:56:41Z)
• Process Reward Models That Think [86.88809596842428]
  Step-by-step verifiers -- also known as process reward models (PRMs) -- are a key ingredient for test-time scaling.<n>This work aims to build data-efficient PRMs as verbalized step-wise reward models that verify every step in the solution by generating a verification chain-of-thought (CoT)<n>We propose ThinkPRM, a long CoT verifier fine-tuned on orders of magnitude fewer process labels than those required by discriminative PRMs.
  arXiv  Detail & Related papers  (2025-04-23T15:44:54Z)
• GenPRM: Scaling Test-Time Compute of Process Reward Models via Generative Reasoning [35.429904556288996]
  We introduce GenPRM, a generative process reward model that performs explicit Chain-of-Thought (CoT) reasoning with code verification.<n> Experimental results show that GenPRM significantly outperforms prior PRMs with only 23K training data from MATH dataset.
  arXiv  Detail & Related papers  (2025-04-01T15:21:05Z)
• The First Few Tokens Are All You Need: An Efficient and Effective Unsupervised Prefix Fine-Tuning Method for Reasoning Models [69.798277882245]
  We introduce Unsupervised Prefix Fine-Tuning (UPFT) to enhance large language models' reasoning efficiency.<n>UPFT removes the need for labeled data or exhaustive sampling.<n> Experiments show that UPFT matches the performance of supervised methods.
  arXiv  Detail & Related papers  (2025-03-04T18:56:03Z)
• Free Process Rewards without Process Labels [55.14044050782222]
  We show that an textitimplicit PRM can be obtained at no additional cost, by simply training an ORM on the cheaper response-level labels.<n>We show that our implicit PRM, when instantiated with the cross-entropy (CE) loss, is more data-efficient and can keep improving generation models even when trained with only one response per instruction.
  arXiv  Detail & Related papers  (2024-12-02T21:20:02Z)
• InfiMM-Eval: Complex Open-Ended Reasoning Evaluation For Multi-Modal Large Language Models [50.03163753638256]
  Multi-modal Large Language Models (MLLMs) are increasingly prominent in the field of artificial intelligence. Our benchmark comprises three key reasoning categories: deductive, abductive, and analogical reasoning. We evaluate a selection of representative MLLMs using this rigorously developed open-ended multi-step elaborate reasoning benchmark.
  arXiv  Detail & Related papers  (2023-11-20T07:06:31Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.