Trainen van Redeneerverifiers op Stapniveau met Formele Verificatietools

Training Step-Level Reasoning Verifiers with Formal Verification Tools

May 21, 2025

Auteurs: Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Rui Zhang

cs.AI

Samenvatting

Proces Beloningsmodellen (PRMs), die stap-voor-stap feedback geven op de redeneringen gegenereerd door Grote Taalmodellen (LLMs), krijgen steeds meer aandacht. Er blijven echter twee belangrijke onderzoekslacunes bestaan: het verzamelen van nauwkeurige foutlabels op stapniveau voor training vereist doorgaans kostbare menselijke annotatie, en bestaande PRMs zijn beperkt tot wiskundige redeneerproblemen. Als reactie op deze lacunes beoogt dit artikel de uitdagingen van automatische datasetcreatie en de generalisatie van PRMs naar diverse redeneertaken aan te pakken. Om dit doel te bereiken, stellen we FoVer voor, een benadering voor het trainen van PRMs op foutlabels op stapniveau die automatisch zijn geannoteerd door formele verificatietools, zoals Z3 voor formele logica en Isabelle voor stellingbewijzen, die automatische en nauwkeurige verificatie bieden voor symbolische taken. Met deze benadering synthetiseren we een trainingsdataset met foutlabels op LLM-reacties voor taken in formele logica en stellingbewijzen zonder menselijke annotatie. Hoewel deze datasynthese alleen haalbaar is voor taken die compatibel zijn met formele verificatie, observeren we dat LLM-gebaseerde PRMs die op onze dataset zijn getraind, kruistaskgeneralisatie vertonen, wat de verificatie over diverse redeneertaken verbetert. Specifiek presteren PRMs die met FoVer zijn getraind aanzienlijk beter dan baseline PRMs gebaseerd op de originele LLMs en behalen ze competitieve of superieure resultaten vergeleken met state-of-the-art PRMs die zijn getraind op labels geannoteerd door mensen of sterkere modellen, zoals gemeten door stap-voor-stap verificatie op ProcessBench en Best-of-K prestaties over 12 redeneerbenchmarks, waaronder MATH, AIME, ANLI, MMLU en BBH. De datasets, modellen en code zijn beschikbaar op https://github.com/psunlpgroup/FoVer.

English

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.