Treinamento de Verificadores de Raciocínio em Nível de Passo com Ferramentas de Verificação 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

Resumo

Modelos de Recompensa de Processo (PRMs), que fornecem feedback passo a passo sobre o raciocínio gerado por Modelos de Linguagem de Grande Escala (LLMs), estão recebendo atenção crescente. No entanto, duas lacunas importantes de pesquisa permanecem: a coleta de rótulos precisos de erros em nível de etapa para treinamento geralmente requer anotação humana custosa, e os PRMs existentes são limitados a problemas de raciocínio matemático. Em resposta a essas lacunas, este artigo visa abordar os desafios da criação automática de conjuntos de dados e da generalização de PRMs para diversas tarefas de raciocínio. Para alcançar esse objetivo, propomos o FoVer, uma abordagem para treinar PRMs em rótulos de erros em nível de etapa anotados automaticamente por ferramentas de verificação formal, como Z3 para lógica formal e Isabelle para provas de teoremas, que fornecem verificação automática e precisa para tarefas simbólicas. Usando essa abordagem, sintetizamos um conjunto de dados de treinamento com rótulos de erros em respostas de LLMs para tarefas de lógica formal e provas de teoremas sem anotação humana. Embora essa síntese de dados seja viável apenas para tarefas compatíveis com verificação formal, observamos que PRMs baseados em LLMs treinados em nosso conjunto de dados exibem generalização entre tarefas, melhorando a verificação em diversas tarefas de raciocínio. Especificamente, PRMs treinados com FoVer superam significativamente PRMs de linha de base baseados nos LLMs originais e alcançam resultados competitivos ou superiores em comparação com PRMs state-of-the-art treinados em rótulos anotados por humanos ou modelos mais fortes, conforme medido pela verificação em nível de etapa no ProcessBench e pelo desempenho Best-of-K em 12 benchmarks de raciocínio, incluindo MATH, AIME, ANLI, MMLU e BBH. Os conjuntos de dados, modelos e código são fornecidos em 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.