연구진은 형식적 증명 분야에서 보상 모델을 평가하기 위한 첫 번째 벤치마크인 'FormalRewardBench'를 공개했습니다. 이 벤치마크는 Lean 4를 기반으로 하며, 250개의 선호도 쌍으로 구성되어 있습니다.
전문가들이 직접 제작한 5가지 오류 주입 전략을 통해 올바른 증명과 잘못된 변형을 결합하여 모델의 평가 능력을 측정합니다.
연구 결과, 최첨단 LLM은 가장 높은 성능을 보였으며, 전문적인 증명 모델은 가장 낮은 성능을 기록했습니다. FormalRewardBench는 연구자들이 형식 수학 분야의 보상 모델 개발을 촉진하는 데 기여할 것으로 기대됩니다.