Entrenamiento de Verificadores de Razonamiento a Nivel de Paso con Herramientas de Verificación Formal

Training Step-Level Reasoning Verifiers with Formal Verification Tools

May 21, 2025

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

cs.AI

Resumen

Los Modelos de Recompensa de Procesos (PRMs, por sus siglas en inglés), que proporcionan retroalimentación paso a paso sobre el razonamiento generado por los Modelos de Lenguaje a Gran Escala (LLMs), están recibiendo una atención creciente. Sin embargo, persisten dos brechas clave de investigación: la recopilación de etiquetas precisas de errores a nivel de paso para el entrenamiento generalmente requiere una costosa anotación humana, y los PRMs existentes están limitados a problemas de razonamiento matemático. En respuesta a estas brechas, este artículo tiene como objetivo abordar los desafíos de la creación automática de conjuntos de datos y la generalización de los PRMs a diversas tareas de razonamiento. Para lograr este objetivo, proponemos FoVer, un enfoque para entrenar PRMs con etiquetas de errores a nivel de paso anotadas automáticamente por herramientas de verificación formal, como Z3 para lógica formal e Isabelle para pruebas de teoremas, las cuales proporcionan verificación automática y precisa para tareas simbólicas. Utilizando este enfoque, sintetizamos un conjunto de datos de entrenamiento con etiquetas de errores en las respuestas de los LLMs para tareas de lógica formal y pruebas de teoremas sin necesidad de anotación humana. Aunque esta síntesis de datos solo es factible para tareas compatibles con la verificación formal, observamos que los PRMs basados en LLMs entrenados con nuestro conjunto de datos exhiben generalización entre tareas, mejorando la verificación en diversas tareas de razonamiento. Específicamente, los PRMs entrenados con FoVer superan significativamente a los PRMs de referencia basados en los LLMs originales y logran resultados competitivos o superiores en comparación con los PRMs más avanzados entrenados con etiquetas anotadas por humanos o modelos más potentes, según se mide por la verificación a nivel de paso en ProcessBench y el rendimiento Best-of-K en 12 puntos de referencia de razonamiento, incluyendo MATH, AIME, ANLI, MMLU y BBH. Los conjuntos de datos, modelos y código están disponibles en 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.