title: Training Step-Level Reasoning Verifiers with Formal Verification Tools
summary: 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.
paper_authors._id: 682fbf41098e5f16167723a0
paper_authors.name: Ryo Kamoi
paper_authors.status: claimed_verified
paper_authors.statusLastChangedAt: 2025-05-26T08:16:58.777Z
paper_authors._id: 60591896102f61b42f65ae37
paper_authors.avatarUrl: https://cdn-avatars.huggingface.co/v1/production/uploads/60591896102f61b42f65ae37/PSHcLoEeNnwvzAPOd6-6i.jpeg
paper_authors.fullname: Ryo Kamoi
paper_authors.type: user
paper_authors.user: ryokamoi
paper_authors._id: 682fbf41098e5f16167723a1
paper_authors.name: Yusen Zhang
paper_authors._id: 682fbf41098e5f16167723a2
paper_authors.name: Nan Zhang
paper_authors._id: 682fbf41098e5f16167723a3
paper_authors.name: Sarkar Snigdha Sarathi Das
paper_authors._id: 682fbf41098e5f16167723a4
paper_authors.name: Rui Zhang
paper_title: Training Step-Level Reasoning Verifiers with Formal Verification Tools
paper_summary: 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.
paper_ai_summary: 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.
paper_ai_keywords: 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