형식 검증 도구를 활용한 훈련 단계 수준 추론 검증기 학습

초록

프로세스 보상 모델(PRMs)은 대형 언어 모델(LLMs)이 생성한 추론 과정에 대해 단계별 피드백을 제공하는 모델로, 최근 주목받고 있습니다. 그러나 두 가지 주요 연구 격차가 남아 있습니다: 정확한 단계별 오류 레이블을 수집하기 위해서는 일반적으로 비용이 많이 드는 인간 주석이 필요하며, 기존 PRMs는 수학적 추론 문제에만 제한되어 있습니다. 이러한 격차에 대응하기 위해, 본 논문은 자동 데이터셋 생성의 어려움과 PRMs의 다양한 추론 작업으로의 일반화 문제를 해결하고자 합니다. 이를 위해 우리는 FoVer를 제안합니다. FoVer는 Z3(형식 논리)와 Isabelle(정리 증명)과 같은 형식 검증 도구를 통해 자동으로 주석 처리된 단계별 오류 레이블을 사용하여 PRMs를 훈련하는 접근 방식입니다. 이러한 도구들은 기호 작업에 대해 자동적이고 정확한 검증을 제공합니다. 이 접근 방식을 사용하여, 우리는 인간 주석 없이 형식 논리와 정리 증명 작업에 대한 LLM 응답의 오류 레이블이 포함된 훈련 데이터셋을 합성합니다. 이 데이터 합성은 형식 검증과 호환되는 작업에만 가능하지만, 우리는 이 데이터셋으로 훈련된 LLM 기반 PRMs가 다양한 추론 작업에서 교차 작업 일반화를 보이며 검증 성능이 향상됨을 관찰했습니다. 구체적으로, FoVer로 훈련된 PRMs는 원본 LLMs를 기반으로 한 기준 PRMs를 크게 능가하며, 인간이나 더 강력한 모델에 의해 주석 처리된 레이블로 훈련된 최첨단 PRMs와 비교하여 경쟁력 있거나 우수한 결과를 달성했습니다. 이는 ProcessBench의 단계별 검증과 MATH, AIME, ANLI, MMLU, BBH를 포함한 12개의 추론 벤치마크에서의 Best-of-K 성능을 통해 측정되었습니다. 데이터셋, 모델, 코드는 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.

형식 검증 도구를 활용한 훈련 단계 수준 추론 검증기 학습

Training Step-Level Reasoning Verifiers with Formal Verification Tools

초록

Support