Entraînement de vérificateurs de raisonnement au niveau des étapes avec des outils de vérification formelle

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

Résumé

Les modèles de récompense de processus (Process Reward Models, PRMs), qui fournissent un retour d'information étape par étape sur le raisonnement généré par les grands modèles de langage (Large Language Models, LLMs), suscitent un intérêt croissant. Cependant, deux lacunes majeures persistent dans la recherche : la collecte d'étiquettes d'erreur précises au niveau des étapes pour l'entraînement nécessite généralement une annotation humaine coûteuse, et les PRM existants se limitent aux problèmes de raisonnement mathématique. Pour répondre à ces lacunes, cet article vise à relever les défis de la création automatique de jeux de données et de la généralisation des PRM à des tâches de raisonnement variées. Pour atteindre cet objectif, nous proposons FoVer, une approche pour entraîner les PRM sur des étiquettes d'erreur au niveau des étapes annotées automatiquement par des outils de vérification formelle, tels que Z3 pour la logique formelle et Isabelle pour les preuves de théorèmes, qui fournissent une vérification automatique et précise pour les tâches symboliques. En utilisant cette approche, nous synthétisons un jeu de données d'entraînement avec des étiquettes d'erreur sur les réponses des LLM pour des tâches de logique formelle et de preuve de théorèmes sans annotation humaine. Bien que cette synthèse de données ne soit réalisable que pour les tâches compatibles avec la vérification formelle, nous observons que les PRM basés sur les LLM entraînés sur notre jeu de données présentent une généralisation inter-tâches, améliorant la vérification sur diverses tâches de raisonnement. Plus précisément, les PRM entraînés avec FoVer surpassent significativement les PRM de référence basés sur les LLM originaux et obtiennent des résultats compétitifs ou supérieurs par rapport aux PRM de pointe entraînés sur des étiquettes annotées par des humains ou des modèles plus puissants, mesurés par la vérification au niveau des étapes sur ProcessBench et la performance Best-of-K sur 12 benchmarks de raisonnement, incluant MATH, AIME, ANLI, MMLU et BBH. Les jeux de données, modèles et code sont disponibles à l'adresse 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.