StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion
Created by
Haebom
Category
Empty
저자
Yutong Wu, Di Huang, Ruosi Wan, Yue Peng, Shijie Shang, Chenrui Cao, Lei Qi, Rui Zhang, Zidong Du, Jie Yan, Xing Hu
개요
Autoformalization은 자연어 수학 명제를 형식 언어로 번역하는 것을 목표로 한다. LLM의 발전에도 불구하고 기존 방법은 낮은 정확도를 보인다. 본 논문은 효과적인 자동 형식화를 위한 두 가지 핵심 능력(형식 언어 도메인 지식에 대한 포괄적인 숙달, 자연어 문제 이해 및 비공식-공식 정렬에 대한 추론 능력)을 식별하고, 두 능력을 향상시키는 데이터 합성 및 훈련 파이프라인인 ThinkingF를 제안한다. ThinkingF는 대규모 형식 지식 예제를 선별하고, 전문가가 설계한 템플릿에 따라 비공식-공식 추론 궤적을 생성하는 두 가지 데이터 세트를 구축한다. SFT와 RLVR을 사용하여 두 능력을 통합하고 개선하며, 7B 및 32B 모델을 개발했다. StepFun-Formalizer-32B는 FormalMATH-Lite에서 40.5%, ProverBench에서 26.7%의 SOTA BEq@1 점수를 달성했다.
시사점, 한계점
•
시사점:
◦
ThinkingF 파이프라인은 형식 언어 도메인 지식과 비공식-공식 추론 능력을 모두 향상시킨다.
◦
두 가지 데이터 세트 구축을 통해 모델 훈련 효과를 높였다.
◦
StepFun-Formalizer-32B는 기존 모델보다 뛰어난 성능을 보였다.
•
한계점:
◦
7B 및 32B 모델의 일반화 능력 및 다른 수학 분야로의 확장성에 대한 추가적인 연구가 필요하다.
◦
RLVR (Reinforcement Learning from Value-guided Reward)의 구체적인 구현 방식 및 효과에 대한 설명이 부족하다.
