Addestramento di Verificatori di Ragionamento a Livello di Passo con Strumenti di Verifica Formale

Training Step-Level Reasoning Verifiers with Formal Verification Tools

May 21, 2025

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

cs.AI

Abstract

I Modelli di Ricompensa del Processo (PRM), che forniscono feedback passo-passo sul ragionamento generato dai Modelli Linguistici di Grande Scala (LLM), stanno ricevendo crescente attenzione. Tuttavia, rimangono due lacune di ricerca chiave: la raccolta di etichette accurate a livello di passo per l'addestramento richiede tipicamente costose annotazioni umane, e gli attuali PRM sono limitati ai problemi di ragionamento matematico. In risposta a queste lacune, questo articolo mira ad affrontare le sfide della creazione automatica di dataset e della generalizzazione dei PRM a compiti di ragionamento diversi. Per raggiungere questo obiettivo, proponiamo FoVer, un approccio per addestrare PRM su etichette di errore a livello di passo annotate automaticamente da strumenti di verifica formale, come Z3 per la logica formale e Isabelle per la dimostrazione di teoremi, che forniscono una verifica automatica e accurata per compiti simbolici. Utilizzando questo approccio, sintetizziamo un dataset di addestramento con etichette di errore sulle risposte degli LLM per compiti di logica formale e dimostrazione di teoremi senza annotazioni umane. Sebbene questa sintesi di dati sia fattibile solo per compiti compatibili con la verifica formale, osserviamo che i PRM basati su LLM addestrati sul nostro dataset mostrano una generalizzazione cross-task, migliorando la verifica su vari compiti di ragionamento. In particolare, i PRM addestrati con FoVer superano significativamente i PRM di base basati sugli LLM originali e raggiungono risultati competitivi o superiori rispetto ai PRM all'avanguardia addestrati su etichette annotate da umani o modelli più forti, come misurato dalla verifica a livello di passo su ProcessBench e dalle prestazioni Best-of-K su 12 benchmark di ragionamento, tra cui MATH, AIME, ANLI, MMLU e BBH. I dataset, i modelli e il codice sono disponibili su 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.