Обучение верификаторов пошагового рассуждения с использованием инструментов формальной верификации

Training Step-Level Reasoning Verifiers with Formal Verification Tools

May 21, 2025

Авторы: Ryo Kamoi, Yusen Zhang, Nan Zhang, Sarkar Snigdha Sarathi Das, Rui Zhang

cs.AI

Аннотация

Модели пошагового вознаграждения (Process Reward Models, PRMs), которые предоставляют поэтапную обратную связь на рассуждения, генерируемые крупными языковыми моделями (Large Language Models, LLMs), привлекают всё больше внимания. Однако остаются два ключевых пробела в исследованиях: сбор точных меток ошибок на уровне шагов для обучения обычно требует дорогостоящей аннотации человеком, а существующие PRMs ограничены задачами математического рассуждения. В ответ на эти пробелы данная работа направлена на решение проблем автоматического создания наборов данных и обобщения PRMs для разнообразных задач рассуждения. Для достижения этой цели мы предлагаем FoVer — подход для обучения PRMs на метках ошибок уровня шагов, автоматически аннотированных инструментами формальной верификации, такими как Z3 для формальной логики и Isabelle для доказательства теорем, которые обеспечивают автоматическую и точную проверку для символьных задач. Используя этот подход, мы синтезируем обучающий набор данных с метками ошибок на ответах LLM для задач формальной логики и доказательства теорем без участия человека. Хотя такой синтез данных возможен только для задач, совместимых с формальной верификацией, мы наблюдаем, что PRMs на основе LLM, обученные на нашем наборе данных, демонстрируют кросс-задачное обобщение, улучшая проверку в разнообразных задачах рассуждения. В частности, PRMs, обученные с использованием FoVer, значительно превосходят базовые PRMs, основанные на исходных LLM, и достигают конкурентоспособных или превосходящих результатов по сравнению с современными PRMs, обученными на метках, аннотированных человеком или более мощными моделями, что измеряется пошаговой проверкой на ProcessBench и производительностью Best-of-K на 12 тестовых наборах, включая MATH, AIME, ANLI, MMLU и BBH. Наборы данных, модели и код доступны по адресу 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.